Accepted Papers

Authors Title Length
Albert Rizaldi, Fabian Immler and Matthias Althoff A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles Regular
Jean-Christophe Filliâtre and Mário Pereira A Modular Way to Reason About Iteration Regular
Adam Nellis, Pascal Kesseli, Philippa Ryan Conmy, Daniel Kroening, Peter Schrammel and Michael Tautschnig Assisted Coverage Closure Regular
Susmit Jha and Vasumathi Raman Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty Regular
Jeroen Meijer and Jaco van de Pol Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis Regular
Srinivas Pinisetty and Stavros Tripakis Compositional Runtime Enforcement Regular
Josh Newell, Linna Pang, David Tremaine, Alan Wassyng and Mark Lawford Formal Translation from IEC-61131-3 Function Blocks to PVS with Nuclear Application Regular
Julian Brunner and Peter Lammich Formal Verification of an Executable LTL Model Checker with Partial Order Reduction Regular
Jing Janet Liu, John D. Backes, Darren Cofer and Andrew Gacek From Design Contracts to Component Requirements Verification Regular
Andreas Abel and Jan Reineke Gray-box Learning of Serial Compositions of Mealy Machines Regular
Yi-Chin Wu, Vasumathi Raman, Stephane Lafortune and Sanjit A. Seshia Obfuscator Synthesis for Privacy and Utility Regular
John Backes, Michael Whalen, Andrew Gacek and John Komp On Implementing Real-time Specification Patterns Using Observers Regular
Muhammad Usama Sardar, Nida Afaq, Khaza Anuarul Hoque, Osman Hasan and Taylor T. Johnson Probabilistic Formal Verification of SATS Concept of Operation Regular
Michael D. Ernst, Damiano Macedonio, Massimo Merro and Fausto Spoto Semantics for Locking Specifications (extended abstract) Regular
Clément Fumex, Claire Dross, Jens Gerlach and Claude Marché Specification and Proof of High-Level Functional Properties of Bit-Level Programs Regular
Meng Wu, Haibo Zeng and Chao Wang Synthesizing Runtime Enforcer of Safety Specification under Burst Error Regular
Ariane Piel, Jean Bourrely, Stéphanie Lala, Sylvain Bertrand and Romain Kervarc Temporal Logic Framework for Performance Analysis of Architectures of Systems Regular
Shaobo He, Shuvendu Lahiri and Zvonimir Rakamaric Verifying Relative Safety, Accuracy, and Termination for Program Approximations Regular
Gaspard Ferey and Natarajan Shankar Code Generation Using A Formal Model of Reference Counting Regular
Robert P. Goldman, Daniel Bryce, Michael Pelican, David Musliner and Kyungmin Bae A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control Short
Ashlie B. Hocking, Benjamin D. Rodes, John C. Knight, Jack W. Davidson and Clark L. Coleman A Proof Infrastructure for Binary Programs Short
Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar and Wilfried Steiner ARSENAL: Automatic Requirements Specification Extraction from Natural Language Short
Hua Zhong, Lingming Zhang and Sarfraz Khurshid Combinatorial Generation of Structurally Complex Tests For Commercial Software Short
Devesh Bhatt, Arunabh Chattopadhyay, Wenchao Li, David Oglesby, Sam Owre and Natarajan Shankar Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems Short
Néstor Cataño and Victor Rivera EventB2Java: A Code Generator for Event-B (Tool paper) Short
Cesar Munoz and Anthony Narkawicz Formal Analysis of Extended Well-Clear Boundaries for Unmanned Aircraft Short
Sergio Guarro, Umit Ozguner, Tunc Aldemir, Matt Knudson, Arda Kurt, Michael Yau, Mohammad Hejase and Steve Kwon Formal Validation and Verification Framework and Models for Model-Based and Adaptive Control Systems Short
Sidi Mohamed Beillahi, Mohamed Yousri Mahmoud and Sofiene Tahar Hierarchical Verification of Quantum Circuits Short
Hao Ren, Devesh Bhatt and Jan Hvozdovic Improving an Industrial Test Generation Tool using SMT Solver Short