| 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 |
