| 2015 | A Framework for Correctness Criteria on Weak Memory Models. John Derrick, Graeme Smith |
| 2015 | A Fully Verified Container Library. Nadia Polikarpova, Julian Tschannen, Carlo A. Furia |
| 2015 | A Specification Language for Static and Runtime Verification of Data and Control Properties. Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, Gerardo Schneider |
| 2015 | AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned. Werner Damm |
| 2015 | Abstraction of Elementary Hybrid Systems by Variable Transformation. Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou |
| 2015 | Analyzing the Restart Behavior of Industrial Control Applications. Stefan Hauck-Stattelmann, Sebastian Biallas, Bastian Schlich, Stefan Kowalewski, Raoul Jetley |
| 2015 | Autofunk: An Inference-Based Formal Model Generation Framework for Production Systems. William Durand, Sébastien Salva |
| 2015 | Automated Circular Assume-Guarantee Reasoning. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham |
| 2015 | Automated Verification of RPC Stub Code. Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz |
| 2015 | Axiomatization of Typed First-Order Logic. Peter H. Schmitt, Mattias Ulbrich |
| 2015 | Case Study: Static Security Analysis of the Android Goldfish Kernel. Tao Liu, Ralf Huuck |
| 2015 | Certificates for Parameterized Model Checking. Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi |
| 2015 | Certified Reasoning with Infinity. Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin |
| 2015 | Counterexamples for Expected Rewards. Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker |
| 2015 | Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. Hamid Bagheri, Eunsuk Kang, Sam Malek, Daniel Jackson |
| 2015 | Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems. Andrew Sogokon, Paul B. Jackson |
| 2015 | Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model Checking. Bharti Chimdyalwar, Priyanka Darke, Anooj Chavda, Sagar Vaghani, Avriti Chauhan |
| 2015 | FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings Nikolaj S. Bjørner, Frank S. de Boer |
| 2015 | Formal Virtual Modelling and Data Verification for Supervision Systems. Thierry Lecomte |
| 2015 | Formalizing the Concept Phase of Product Development. Mathijs Schuts, Jozef Hooman |
| 2015 | Model-Based Problem Solving for University Timetable Validation and Improvement. David Schneider, Michael Leuschel, Tobias Witt |
| 2015 | Narrowing Operators on Template Abstract Domains. Gianluca Amato, Simone Di Nardo Di Maio, Maria Chiara Meo, Francesca Scozzari |
| 2015 | Parameter Synthesis Through Temporal Logic Specifications. Thao Dang, Tommaso Dreossi, Carla Piazza |
| 2015 | Practices for Formal Models as Documents: Evolution of VDM Application to "Mobile FeliCa" IC Chip Firmware. Taro Kurita, Fuyuki Ishikawa, Keijiro Araki |
| 2015 | Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System Architectures. Julien Bringer, Hervé Chabanne, Daniel Le Métayer, Roch Lescuyer |
| 2015 | Probabilistic Bisimulation for Realistic Schedulers. Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song, Lijun Zhang |
| 2015 | Property-Driven Fence Insertion Using Reorder Bounded Model Checking. Saurabh Joshi, Daniel Kroening |
| 2015 | Proving Safety with Trace Automata and Bounded Model Checking. Daniel Kroening, Matt Lewis, Georg Weissenbacher |
| 2015 | QPMC: A Model Checker for Quantum Programs and Protocols. Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, Lijun Zhang |
| 2015 | Resource Analysis: From Sequential to Concurrent and Distributed Programs. Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, Guillermo Román-Díez |
| 2015 | Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan |
| 2015 | Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes. Søren Debois, Thomas T. Hildebrandt, Tijs Slaats |
| 2015 | Semantics-Preserving Simplification of Real-World Firewall Rule Sets. Cornelius Diekmann, Lars Hupel, Georg Carle |
| 2015 | Software Development and Authentication for Arms Control Information Barriers. Neil Evans |
| 2015 | Static Differential Program Analysis for Software-Defined Networks. Tim Nelson, Andrew D. Ferguson, Shriram Krishnamurthi |
| 2015 | Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking. Xueyang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang, Wenhui Zhang, Guangquan Zhang |
| 2015 | The Semantics of Cardinality-Based Feature Models via Formal Languages. Aliakbar Safilian, Tom Maibaum, Zinovy Diskin |
| 2015 | Towards Formal Verification of Orchestration Computations Using the 핂 Framework. Musab A. Alturki, Omar Alzuhaibi |
| 2015 | Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL. Xiaoning Du, Yang Liu, Alwen Tiu |
| 2015 | Using Real-Time Maude to Model Check Energy Consumption Behavior. Shin Nakajima |
| 2015 | Using Simulink Design Verifier for Automatic Generation of Requirements-Based Tests. Bruno Miranda, Henrique Masini, Rodrigo Reis |
| 2015 | Verifying Opacity of a Transactional Mutex Lock. John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim |
| 2015 | Verifying Parameterized Timed Security Protocols. Li Li, Jun Sun, Yang Liu, Jin Song Dong |
| 2015 | Verifying the Safety of a Flight-Critical System. Guillaume Brat, David H. Bushnell, Misty D. Davies, Dimitra Giannakopoulou, Falk Howar, Temesghen Kahsai |