| 2014 | A Bounded Model Checker for SPARK Programs. Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto |
| 2014 | A Game-Theoretic Approach to Simulation of Data-Parameterized Systems. Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2014 | A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol. Timothy Bourke, Rob J. van Glabbeek, Peter Höfner |
| 2014 | ACME: Automata with Counters, Monoids and Equivalence. Nathanaël Fijalkow, Denis Kuperberg |
| 2014 | Acceleration of Affine Hybrid Transformations. Bernard Boigelot, Frédéric Herbreteau, Isabelle Mainz |
| 2014 | Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings Franck Cassez, Jean-François Raskin |
| 2014 | Booster: An Acceleration-Based Verification Framework for Array Programs. Francesco Alberti, Silvio Ghilardi, Natasha Sharygina |
| 2014 | Deciding Entailments in Inductive Separation Logic with Tree Automata. Radu Iosif, Adam Rogalewicz, Tomás Vojnar |
| 2014 | Efficiently and Completely Verifying Synchronized Consistency Models. Yi Lv, Luming Sun, Xiaochun Ye, Dongrui Fan, Peng Wu |
| 2014 | Extensional Crisis and Proving Identity. Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov |
| 2014 | Fast Debugging of PRISM Models. Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen |
| 2014 | Formal Safety Assessment via Contract-Based Design. Marco Bozzano, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta |
| 2014 | Formal Verification of Skiplists with Arbitrary Many Levels. Alejandro Sánchez, César Sánchez |
| 2014 | Incremental Encoding and Solving of Cardinality Constraints. Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker |
| 2014 | Liveness Analysis for Parameterised Boolean Equation Systems. Jeroen J. A. Keiren, Wieger Wesselink, Tim A. C. Willemse |
| 2014 | Modelling and Analysis of Markov Reward Automata. Dennis Guck, Mark Timmer, Hassan Hatefi, Enno Ruijters, Mariëlle Stoelinga |
| 2014 | Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters. Guoxin Su, David S. Rosenblum |
| 2014 | On Time with Minimal Expected Cost! Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen, Jakob Haahr Taankvist |
| 2014 | PeCAn: Compositional Verification of Petri Nets Made Easy. Dinh-Thuan Le, Huu-Vu Nguyen, Van-Tinh Nguyen, Phuong-Nam Mai, Bao-Trung Pham-Duy, Thanh-Tho Quan, Étienne André, Laure Petrucci, Yang Liu |
| 2014 | Quantitative Verification of Weighted Kripke Structures. Patricia Bouyer, Patrick Gardy, Nicolas Markey |
| 2014 | Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. Zuzana Komárková, Jan Kretínský |
| 2014 | Statistically Sound Verification and Optimization for Complex Systems. Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi |
| 2014 | Symbolic Memory with Pointers. Marek Trtík, Jan Strejcek |
| 2014 | Symmetry Reduction in Infinite Games with Finite Branching. Nicolas Markey, Steen Vester |
| 2014 | Test Coverage Estimation Using Threshold Accepting. Thao Dang, Noa Shalev |
| 2014 | The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems. Jérôme Leroux, Vincent Penelle, Grégoire Sutre |
| 2014 | Trace Abstraction Refinement for Timed Automata. Weifeng Wang, Li Jiao |
| 2014 | Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom. Divjyot Sethi, Muralidhar Talupur, Sharad Malik |
| 2014 | Verification of Markov Decision Processes Using Learning Algorithms. Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma |
| 2014 | Verifying Communicating Multi-pushdown Systems via Split-Width. C. Aiswarya, Paul Gastin, K. Narayan Kumar |