| 2015 | GPU Accelerated Strong and Branching Bisimilarity Checking. | Anton Wijs |
| 2015 | Cascade - (Competition Contribution). | Wei Wang, Clark W. Barrett |
| 2015 | FuncTion: An Abstract Domain Functor for Termination - (Competition Contribution). | Caterina Urban |
| 2015 | Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling. | Hiroshi Unno, Tachio Terauchi |
| 2015 | AutoProof: Auto-Active Functional Verification of Object-Oriented Programs. | Julian Tschannen, Carlo A. Furia, Martin Nordio, Nadia Polikarpova |
| 2015 | Verifying Concurrent Programs by Memory Unwinding. | Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 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 | Symbolic Model-Checking Using ITS-Tools. | Yann Thierry-Mieg |
| 2015 | AProVE: Termination and Memory Safety of C Programs - (Competition Contribution). | Thomas Strder, Cornelius Aschermann, Florian Frohn, Jera Hensel, Jrgen Giesl |
| 2015 | FAUST | Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, Alessandro Abate |
| 2015 | Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. | Roberto Sebastiani, Patrick Trentin |
| 2015 | Symbolic Quantitative Robustness Analysis of Timed Automata. | Ocan Sankur |
| 2015 | Parallel Explicit Model Checking for Generalized Bchi Automata. | Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| 2015 | MarQ: Monitoring at Runtime with QEA. | Giles Reger, Helena Cuenca Cruz, David E. Rydeheard |
| 2015 | ULTIMATE KOJAK with Memory Safety Checks - (Competition Contribution). | Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed, 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 | Analysis of Dynamic Process Networks. | Kedar S. Namjoshi, Richard J. Trefler |
| 2015 | Predator Hunting Party (Competition Contribution). | Petr Mller, Petr Peringer, Toms Vojnar |
| 2015 | Saturation-Based Incremental LTL Model Checking with Inductive Proofs. | Vince Molnr, Dniel Darvas, Andrs Vrs, Tams Bartha |
| 2015 | Value Slice: A New Slicing Concept for Scalable Property Checking. | Shrawan Kumar, Amitabha Sanyal, Uday P. Khedker |
| 2015 | Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip. | Abderahman Kriouile, Wendelin Serwe |
| 2015 | dReach: δ-Reachability Analysis for Hybrid Systems. | Soonho Kong, Sicun Gao, Wei Chen, Edmund M. Clarke |
| 2015 | Limit Deterministic and Probabilistic Automata for LTL ∖ GU. | Dileep Kini, Mahesh Viswanathan |
| 2015 | LTSmin: High-Performance Language-Independent Model Checking. | Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, Tom van Dijk |
| 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 |