| 2015 | A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, André Platzer |
| 2015 | A Method for Improving the Precision and Coverage of Atomicity Violation Predictions. Reng Zeng, Zhuo Sun, Su Liu, Xudong He |
| 2015 | AProVE: Termination and Memory Safety of C Programs - (Competition Contribution). Thomas Ströder, Cornelius Aschermann, Florian Frohn, Jera Hensel, Jürgen Giesl |
| 2015 | An LTL Proof System for Runtime Verification. Clare Cini, Adrian Francalanza |
| 2015 | Analysis of Dynamic Process Networks. Kedar S. Namjoshi, Richard J. Trefler |
| 2015 | Approximate Counting in SMT and Value Estimation for Probabilistic Programs. Dmitry Chistikov, Rayna Dimitrova, Rupak Majumdar |
| 2015 | Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information. Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs, Robert Könighofer |
| 2015 | AutoProof: Auto-Active Functional Verification of Object-Oriented Programs. Julian Tschannen, Carlo A. Furia, Martin Nordio, Nadia Polikarpova |
| 2015 | BINSEC: Binary Code Analysis with Low-Level Regions. Adel Djoudi, Sébastien Bardin |
| 2015 | C2E2: A Verification Tool for Stateflow Models. Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan, Matthew Potok |
| 2015 | CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic - (Competition Contribution). Matthias Dangl, Stefan Löwe, Philipp Wendler |
| 2015 | CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation - (Competition Contribution). Yu-Fang Chen, Chiao Hsieh, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang |
| 2015 | Cascade - (Competition Contribution). Wei Wang, Clark W. Barrett |
| 2015 | Commutativity of Reducers. Yu-Fang Chen, Chih-Duo Hong, Nishant Sinha, Bow-Yaw Wang |
| 2015 | FAUST Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, Alessandro Abate |
| 2015 | Fairness for Infinite-State Systems. Byron Cook, Heidy Khlaaf, Nir Piterman |
| 2015 | Forester: Shape Analysis Using Tree Automata - (Competition Contribution). Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar |
| 2015 | FramewORk for Embedded System verification - (Competition Contribution). Pablo González de Aledo, Pablo Sánchez Espeso |
| 2015 | FuncTion: An Abstract Domain Functor for Termination - (Competition Contribution). Caterina Urban |
| 2015 | GPU Accelerated Strong and Branching Bisimilarity Checking. Anton Wijs |
| 2015 | HyComp: An SMT-Based Model Checker for Hybrid Systems. Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2015 | Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling. Hiroshi Unno, Tachio Terauchi |
| 2015 | Insight: An Open Binary Analysis Framework. Emmanuel Fleury, Olivier Ly, Gérald Point, Aymeric Vincent |
| 2015 | LTSmin: High-Performance Language-Independent Model Checking. Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, Tom van Dijk |
| 2015 | Limit Deterministic and Probabilistic Automata for LTL ∖ GU. Dileep Kini, Mahesh Viswanathan |
| 2015 | Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving. Jeroen Bransen, L. Thomas van Binsbergen, Koen Claessen, Atze Dijkstra |
| 2015 | MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings - (Competition Contribution). Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2015 | MarQ: Monitoring at Runtime with QEA. Giles Reger, Helena Cuenca Cruz, David E. Rydeheard |
| 2015 | Model Checking Gene Regulatory Networks. Mirco Giacobbe, Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Tiago Paixão, Tatjana Petrov |
| 2015 | MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. Tomás Brázdil, Krishnendu Chatterjee, Vojtech Forejt, Antonín Kucera |
| 2015 | Nested Antichains for WS1S. Tomás Fiedor, Lukás Holík, Ondrej Lengál, Tomás Vojnar |
| 2015 | Non-cumulative Resource Analysis. Elvira Albert, Jesús Correas Fernández, Guillermo Román-Díez |
| 2015 | On Parallel Scalable Uniform SAT Witness Generation. Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi |
| 2015 | Parallel Explicit Model Checking for Generalized Büchi Automata. Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2015 | Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis. Rajeev Alur, Salar Moarref, Ufuk Topcu |
| 2015 | Perentie: Modular Trace Refinement and Selective Value Tracking - (Competition Contribution). Franck Cassez, Takashi Matsuoka, Edward Pierzchalski, Nathan Smyth |
| 2015 | Predator Hunting Party (Competition Contribution). Petr Müller, Petr Peringer, Tomás Vojnar |
| 2015 | Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. Roberto Sebastiani, Patrick Trentin |
| 2015 | SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform. Alessandro Armando, Gianluca Bocci, Giantonio Chiarelli, Gabriele Costa, Gabriele De Maglie, Rocco Mammoliti, Alessio Merlo |
| 2015 | SMACK+Corral: A Modular Verifier - (Competition Contribution). Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric |
| 2015 | Saturation-Based Incremental LTL Model Checking with Inductive Proofs. Vince Molnár, Dániel Darvas, András Vörös, Tamás Bartha |
| 2015 | Scalable Timing Analysis with Refinement. Nan Guan, Yue Tang, Jakaria Abdullah, Martin Stigge, Wang Yi |
| 2015 | SeaHorn: A Framework for Verifying C Programs (Competition Contribution). Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas |
| 2015 | Semantic Importance Sampling for Statistical Model Checking. Jeffery P. Hansen, Lutz Wrage, Sagar Chaki, Dionisio de Niz, Mark H. Klein |
| 2015 | Shield Synthesis: - Runtime Enforcement for Reactive Systems. Roderick Bloem, Bettina Könighofer, Robert Könighofer, Chao Wang |
| 2015 | Software Verification and Verifiable Witnesses - (Report on SV-COMP 2015). Dirk Beyer |
| 2015 | Stateless Model Checking for TSO and PSO. Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, Konstantinos Sagonas |
| 2015 | Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. Nicolas Basset, Marta Z. Kwiatkowska, Ufuk Topcu, Clemens Wiltsche |
| 2015 | Sylvan: Multi-Core Decision Diagrams. Tom van Dijk, Jaco van de Pol |
| 2015 | Symbolic Model-Checking Using ITS-Tools. Yann Thierry-Mieg |
| 2015 | Symbolic Quantitative Robustness Analysis of Timed Automata. Ocan Sankur |
| 2015 | Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings Christel Baier, Cesare Tinelli |
| 2015 | ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution). Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed, Andreas Podelski |
| 2015 | Ultimate Automizer with Array Interpolation - (Competition Contribution). Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, Andreas Podelski |
| 2015 | Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches - (Competition Contribution). Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2015 | Uppaal Stratego. Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikucionis, Jakob Haahr Taankvist |
| 2015 | Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip. Abderahman Kriouile, Wendelin Serwe |
| 2015 | Value Slice: A New Slicing Concept for Scalable Property Checking. Shrawan Kumar, Amitabha Sanyal, Uday P. Khedker |
| 2015 | Verified Reachability Analysis of Continuous Systems. Fabian Immler |
| 2015 | Verifying Concurrent Programs by Memory Unwinding. Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2015 | dReach: δ-Reachability Analysis for Hybrid Systems. Soonho Kong, Sicun Gao, Wei Chen, Edmund M. Clarke |
| 2015 | syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications. Ramiro Demasi, Pablo F. Castro, Nicolás Ricci, Thomas Stephen Edward Maibaum, Nazareno Aguirre |
| 2015 | νZ - An Optimizing SMT Solver. Nikolaj S. Bjørner, Anh-Dung Phan, Lars Fleckenstein |