| 2014 | 40 Years of Formal Methods - Some Obstacles and Some Possibilities? Dines Bjørner, Klaus Havelund |
| 2014 | A Graph-Based Transformation Reduction to Reach UPPAAL States Faster. Jonas Rinast, Sibylle Schupp, Dieter Gollmann |
| 2014 | A Modular Theory of Object Orientation in Higher-Order UTP. Frank Zeyda, Thiago L. V. L. Santos, Ana Cavalcanti, Augusto Sampaio |
| 2014 | A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes. Pedro R. G. Antonino, Augusto Sampaio, Jim Woodcock |
| 2014 | A Simplified Z Semantics for Presentation Interaction Models. Judy Bowen, Steve Reeves |
| 2014 | A Symbolic Algorithm for the Analysis of Robust Timed Automata. Piotr Kordy, Rom Langerak, Sjouke Mauw, Jan Willem Polderman |
| 2014 | Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools. Alasdair Armstrong, Victor B. F. Gomes, Georg Struth |
| 2014 | Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic. Morteza Yousef Sanati, Wendy MacCaull, T. S. E. Maibaum |
| 2014 | Automated Real Proving in PVS via MetiTarski. William Denman, César A. Muñoz |
| 2014 | Automatic Compositional Synthesis of Distributed Systems. Werner Damm, Bernd Finkbeiner |
| 2014 | Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis. K. Vasanta Lakshmi, Aravind Acharya, Raghavan Komondoor |
| 2014 | Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. K. Rustan M. Leino, Michal Moskal |
| 2014 | Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning. Shang-Wei Lin, Pao-Ann Hsiung |
| 2014 | Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison. Pierre Roux, Pierre-Loïc Garoche |
| 2014 | Contracts in Practice. H.-Christian Estler, Carlo A. Furia, Martin Nordio, Marco Piccioni, Bertrand Meyer |
| 2014 | Definition, Semantics, and Analysis of Multirate Synchronous AADL. Kyungmin Bae, Peter Csaba Ölveczky, José Meseguer |
| 2014 | Diagnosing Industrial Business Processes: Early Experiences. Suman Roy, A. S. M. Sajeev, Srivibha Sripathy |
| 2014 | Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System. Hendra Gunadi, Alwen Tiu |
| 2014 | Efficient Self-composition for Weakest Precondition Calculi. Christoph Scheben, Peter H. Schmitt |
| 2014 | Efficient Tight Field Bounds Computation Based on Shape Predicates. Pablo Ponzio, Nicolás Rosner, Nazareno Aguirre, Marcelo F. Frias |
| 2014 | Engineering UToPiA - Formal Semantics for CML. Jim Woodcock |
| 2014 | FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings Cliff B. Jones, Pekka Pihlajasaari, Jun Sun |
| 2014 | Flexible Invariants through Semantic Collaboration. Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, Bertrand Meyer |
| 2014 | Formal Verification of Lunar Rover Control Software Using UPPAAL. Lijun Shan, Yuying Wang, Ning Fu, Xingshe Zhou, Lei Zhao, Lijng Wan, Lei Qiao, Jianxin Chen |
| 2014 | Formal Verification of Operational Transformation. Yang Liu, Yi Xu, Shao Jie Zhang, Chengzheng Sun |
| 2014 | Formal Verification of a Descent Guidance Control Program of a Lunar Lander. Hengjun Zhao, Mengfei Yang, Naijun Zhan, Bin Gu, Liang Zou, Yao Chen |
| 2014 | Formalizing and Verifying a Modern Build Language. Maria Christakis, K. Rustan M. Leino, Wolfram Schulte |
| 2014 | Formally Verifying Graphics FPU - An Intel® Experience. Aarti Gupta, V. M. Achutha KiranKumar, Rajnish Ghughal |
| 2014 | Invariants, Well-Founded Statements and Real-Time Program Algebra. Ian J. Hayes, Larissa Meinicke |
| 2014 | Knowledge-Based Automated Repair of Authentication Protocols. Borzoo Bonakdarpour, Reza Hajisheykhi, Sandeep S. Kulkarni |
| 2014 | Log Analysis for Data Protection Accountability. Denis Butin, Daniel Le Métayer |
| 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 | Object Propositions. Ligia Nistor, Jonathan Aldrich, Stephanie Balzer, Hannes Mehnert |
| 2014 | Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs. Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, Subodh Sharma |
| 2014 | Proof Engineering Considered Essential. Gerwin Klein |
| 2014 | Proof Patterns for Formal Methods. Leo Freitas, Iain Whiteside |
| 2014 | Quiescent Consistency: Defining and Verifying Relaxed Linearizability. John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim |
| 2014 | Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems. Stefan Mitsch, Jan-David Quesel, André Platzer |
| 2014 | Revisiting Compatibility of Input-Output Modal Transition Systems. Ivo Krka, Nicolás D'Ippolito, Nenad Medvidovic, Sebastián Uchitel |
| 2014 | SCJ: Memory-Safety Checking without Annotations. Chris Marriott, Ana Cavalcanti |
| 2014 | Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol. Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, César A. Muñoz |
| 2014 | The VerCors Tool for Verification of Concurrent Programs. Stefan Blom, Marieke Huisman |
| 2014 | The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification. Sergio Feo-Arenis, Bernd Westphal, Daniel Dietsch, Marco Muñiz, Ahmad Siyar Andisha |
| 2014 | Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections. Roland Wen, Annabelle McIver, Carroll Morgan |
| 2014 | TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms. Guangdong Bai, Jianan Hao, Jianliang Wu, Yang Liu, Zhenkai Liang, Andrew P. Martin |
| 2014 | Validity Checking of Putback Transformations in Bidirectional Programming. Zhenjiang Hu, Hugo Pacheco, Sebastian Fischer |
| 2014 | Verification of a Transactional Memory Manager under Hardware Failures and Restarts. Ognjen Maric, Christoph Sprenger |
| 2014 | When Equivalence and Bisimulation Join Forces in Probabilistic Automata. Yuan Feng, Lijun Zhang |
| 2014 | iscasMc: A Web-Based Probabilistic Model Checker. Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, Lijun Zhang |