| 2014 | Flexible Invariants through Semantic Collaboration. | Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, Bertrand Meyer |
| 2014 | Object Propositions. | Ligia Nistor, Jonathan Aldrich, Stephanie Balzer, Hannes Mehnert |
| 2014 | Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems. | Stefan Mitsch, Jan-David Quesel, Andr Platzer |
| 2014 | SCJ: Memory-Safety Checking without Annotations. | Chris Marriott, Ana Cavalcanti |
| 2014 | Verification of a Transactional Memory Manager under Hardware Failures and Restarts. | Ognjen Maric, Christoph Sprenger |
| 2014 | Formal Verification of Operational Transformation. | Yang Liu, Yi Xu, Shao Jie Zhang, Chengzheng Sun |
| 2014 | MDP-Based Reliability Analysis of an Ambient Assisted Living System. | Yan Liu, Lin Gui, Yang Liu |
| 2014 | Management of Time Requirements in Component-Based Systems. | Yi Li, Tian Huat Tan, Marsha Chechik |
| 2014 | Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning. | Shang-Wei Lin, Pao-Ann Hsiung |
| 2014 | Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. | K. Rustan M. Leino, Michal Moskal |
| 2014 | Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis. | K. Vasanta Lakshmi, Aravind Acharya, Raghavan Komondoor |
| 2014 | Revisiting Compatibility of Input-Output Modal Transition Systems. | Ivo Krka, Nicols D'Ippolito, Nenad Medvidovic, Sebastin Uchitel |
| 2014 | A Symbolic Algorithm for the Analysis of Robust Timed Automata. | Piotr Kordy, Rom Langerak, Sjouke Mauw, Jan Willem Polderman |
| 2014 | Proof Engineering Considered Essential. | Gerwin Klein |
| 2014 | Validity Checking of Putback Transformations in Bidirectional Programming. | Zhenjiang Hu, Hugo Pacheco, Sebastian Fischer |
| 2014 | Invariants, Well-Founded Statements and Real-Time Program Algebra. | Ian J. Hayes, Larissa Meinicke |
| 2014 | iscasMc: A Web-Based Probabilistic Model Checker. | Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, Lijun Zhang |
| 2014 | Formally Verifying Graphics FPU - An Intel Experience. | Aarti Gupta, V. M. Achutha KiranKumar, Rajnish Ghughal |
| 2014 | Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System. | Hendra Gunadi, Alwen Tiu |
| 2014 | Proof Patterns for Formal Methods. | Leo Freitas, Iain Whiteside |
| 2014 | Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. | Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma |
| 2014 | When Equivalence and Bisimulation Join Forces in Probabilistic Automata. | Yuan Feng, Lijun Zhang |
| 2014 | Contracts in Practice. | H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, Bertrand Meyer |
| 2014 | Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol. | Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, Csar A. Muoz |
| 2014 | Quiescent Consistency: Defining and Verifying Relaxed Linearizability. | John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim |