| 2014 | APTE: An Algorithm for Proving Trace Equivalence. Vincent Cheval |
| 2014 | Alternating Runtime and Size Complexity Analysis of Integer Programs. Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl |
| 2014 | Analyzing the Next Generation Airborne Collision Avoidance System. Christian von Essen, Dimitra Giannakopoulou |
| 2014 | Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata. Ting Wang, Jun Sun, Yang Liu, Xinyu Wang, Shanping Li |
| 2014 | Basic Problems in Multi-View Modeling. Jan Reineke, Stavros Tripakis |
| 2014 | Bounds2: A Tool for Compositional Multi-parametrised Verification. Antti Siirtola |
| 2014 | CBMC - C Bounded Model Checker - (Competition Contribution). Daniel Kroening, Michael Tautschnig |
| 2014 | CIF 3: Model-Based Engineering of Supervisory Controllers. D. A. van Beek, Wan J. Fokkink, Dennis Hendriks, Albert T. Hofkamp, Jasen Markovski, Joanna M. van de Mortel-Fronczak, Michel A. Reniers |
| 2014 | CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution). Stefan Löwe, Mikhail U. Mandrykin, Philipp Wendler |
| 2014 | CPAlien: Shape Analyzer for CPAChecker - (Competition Contribution). Petr Müller, Tomás Vojnar |
| 2014 | Characterizing Algebraic Invariants by Differential Radical Invariants. Khalil Ghorbal, André Platzer |
| 2014 | Compositional Invariant Generation for Timed Systems. Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz |
| 2014 | Computing Conditional Probabilities in Markovian Models Efficiently. Christel Baier, Joachim Klein, Sascha Klüppelholz, Steffen Märcker |
| 2014 | Concurrent Depth-First Search Algorithms. Gavin Lowe |
| 2014 | Decision Procedures for Flat Array Properties. Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2014 | Detecting Unrealizable Specifications of Distributed Systems. Bernd Finkbeiner, Leander Tentrup |
| 2014 | Discounting in LTL. Shaull Almagor, Udi Boker, Orna Kupferman |
| 2014 | EDD: A Declarative Debugger for Sequential Erlang Programs. Rafael Caballero, Enrique Martin-Martin, Adrián Riesco, Salvador Tamarit |
| 2014 | ESBMC 1.22 - (Competition Contribution). Jeremy Morse, Mikhail Ramalho, Lucas C. Cordeiro, Denis A. Nicole, Bernd Fischer |
| 2014 | Environment-Model Based Testing of Control Systems: Case Studies. Erwan Jahier, Simplice Djoko Djoko, Chaouki Maiza, Eric Lafont |
| 2014 | FDR3 - A Modern Refinement Checker for CSP. Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, A. W. Roscoe |
| 2014 | Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic. Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta |
| 2014 | Forward Reachability Computation for Autonomous Max-Plus-Linear Systems. Dieky Adzkiya, Bart De Schutter, Alessandro Abate |
| 2014 | FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). Arie Gurfinkel, Anton Belov |
| 2014 | GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs. Anton Wijs, Dragan Bosnacki |
| 2014 | GRASShopper - Complete Heap Verification with Mixed Specifications. Ruzica Piskac, Thomas Wies, Damien Zufferey |
| 2014 | IC3 Modulo Theories via Implicit Predicate Abstraction. Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2014 | Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution). Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2014 | Learning Regular Languages over Large Alphabets. Oded Maler, Irini-Eleftheria Mens |
| 2014 | MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution). Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2014 | Monitoring Modulo Theories. Normann Decker, Martin Leucker, Daniel Thoma |
| 2014 | On the Correctness of a Branch Displacement Algorithm. Jaap Boender, Claudio Sacerdoti Coen |
| 2014 | PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence. Michael Huth, Jim Huan-Pu Kuo |
| 2014 | Permissive Controller Synthesis for Probabilistic Systems. Klaus Dräger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma |
| 2014 | Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance. Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate |
| 2014 | Predator: A Shape Analyzer Based on Symbolic Memory Graphs - (Competition Contribution). Kamil Dudka, Petr Peringer, Tomás Vojnar |
| 2014 | Proving Nontermination via Safety. Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn |
| 2014 | Quasi-Equal Clock Reduction: More Networks, More Queries. Christian Herrera, Bernd Westphal, Andreas Podelski |
| 2014 | Ranking Templates for Linear Loops. Jan Leike, Matthias Heizmann |
| 2014 | SACO: Static Analyzer for Concurrent Objects. Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, German Puebla, Guillermo Román-Díez |
| 2014 | SATMC: A SAT-Based Model Checker for Security-Critical Systems. Alessandro Armando, Roberto Carbone, Luca Compagna |
| 2014 | SMT-Based Verification of Software Countermeasures against Side-Channel Attacks. Hassan Eldib, Chao Wang, Patrick Schaumont |
| 2014 | Status Report on Software Verification - (Competition Summary SV-COMP 2014). Dirk Beyer |
| 2014 | Symbiotic 2: More Precise Slicing - (Competition Contribution). Jiri Slaby, Jan Strejcek |
| 2014 | Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata. Ala-Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg |
| 2014 | Symbolic Synthesis for Epistemic Specifications with Observational Semantics. Xiaowei Huang, Ron van der Meyden |
| 2014 | Synthesis for Human-in-the-Loop Control Systems. Wenchao Li, Dorsa Sadigh, S. Shankar Sastry, Sanjit A. Seshia |
| 2014 | Synthesizing Safe Bit-Precise Invariants. Arie Gurfinkel, Anton Belov, João Marques-Silva |
| 2014 | Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems. Thomas Reinbacher, Kristin Yvonne Rozier, Johann Schumann |
| 2014 | The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. Arnd Hartmanns, Holger Hermanns |
| 2014 | Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings Erika Ábrahám, Klaus Havelund |
| 2014 | Ultimate Automizer with Unsatisfiable Cores - (Competition Contribution). Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Christian Schilling, Stefan Wissert, Andreas Podelski |
| 2014 | Ultimate Kojak - (Competition Contribution). Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, Andreas Podelski |
| 2014 | Variations on Safety. Orna Kupferman |
| 2014 | VeriMAP: A Tool for Verifying Programs through Transformations. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2014 | Verification of Concurrent Quantum Protocols by Equivalence Checking. Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan |