| 2014 | A Logic-Based Framework for Verifying Consensus Algorithms. Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey |
| 2014 | Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes. Lei Song, Lijun Zhang, Jens Chr. Godskesen |
| 2014 | Cascade 2.0. Wei Wang, Clark W. Barrett, Thomas Wies |
| 2014 | Doomsday Equilibria for Omega-Regular Games. Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot, Jean-François Raskin |
| 2014 | Generic Combination of Heap and Value Analyses in Abstract Interpretation. Pietro Ferrara |
| 2014 | Message-Passing Algorithms for the Verification of Distributed Protocols. Loïg Jezequel, Javier Esparza |
| 2014 | Modeling Parsimonious Putative Regulatory Networks: Complexity and Heuristic Approach. Vicente Acuña, Andrés Aravena, Alejandro Maass, Anne Siegel |
| 2014 | Modular Synthesis of Sketches Using Models. Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick, Armando Solar-Lezama |
| 2014 | Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java. Zhoulai Fu |
| 2014 | Monitoring Parametric Temporal Logic. Peter Faymonville, Bernd Finkbeiner, Doron A. Peled |
| 2014 | Parameterized Model Checking of Token-Passing Systems. Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, Sasha Rubin |
| 2014 | Policy Iteration-Based Conditional Termination and Ranking Functions. Damien Massé |
| 2014 | Practical Floating-Point Tests with Integer Code. Anthony Romano |
| 2014 | Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs. Martin D. Schwarz, Helmut Seidl, Vesal Vojdani, Kalmer Apinis |
| 2014 | Precisely Deciding Control State Reachability in Concurrent Traces with Limited Observability. Chao Wang, Kevin Hoang |
| 2014 | Probabilistic Automata for Safety LTL Specifications. Dileep Kini, Mahesh Viswanathan |
| 2014 | Refuting Heap Reachability. Bor-Yuh Evan Chang |
| 2014 | Relational Thread-Modular Static Value Analysis by Abstract Interpretation. Antoine Miné |
| 2014 | SAT-Based Synthesis Methods for Safety Specs. Roderick Bloem, Robert Könighofer, Martina Seidl |
| 2014 | Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops. Marius Bozga, Radu Iosif, Filip Konecný |
| 2014 | Synthesis for Polynomial Lasso Programs. Jan Leike, Ashish Tiwari |
| 2014 | Synthesis with Identifiers. Rüdiger Ehlers, Sanjit A. Seshia, Hadas Kress-Gazit |
| 2014 | Timing Analysis of Parallel Software Using Abstract Execution. Andreas Gustavsson, Jan Gustafsson, Björn Lisper |
| 2014 | Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings Kenneth L. McMillan, Xavier Rival |
| 2014 | Verifying Array Programs by Transforming Verification Conditions. Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti |
| 2014 | Weakest Precondition Synthesis for Compiler Optimizations. Nuno P. Lopes, José Monteiro |
| 2014 | Widening for Control-Flow. Ben Hardekopf, Ben Wiedermann, Berkeley R. Churchill, Vineeth Kashyap |