Density of Reachable States and How to Use it for Safe Autonomous Motion Planning |
Yue Meng, Zeng Qiu, Md Tawhid Bin Waez and Chuchu Fan. |
From Verified Scala to STIX File System Embedded Code using Stainless |
Jad Hamza, Simon Felix, Viktor Kuncak, Ivo Nussbaumer and Filip Schramka. |
Operational annotations: a new method for sequential program verification |
Paul Attie. |
Robust Computation Tree Logic |
Satya Prakash Nayak, Daniel Neider, Rajarshi Roy and Martin Zimmermann. |
Zone extrapolations in parametric timed automata |
Johan Arcile and Étienne André. |
More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme |
James Noble, David Streader, Isaac Oscar Gariano and Miniruwani Samarakoon. |
Towards Refactoring FRETish Requirements |
Marie Farrell, Matt Luckcuck, Oisin Sheridan and Rosemary Monahan. |
Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda |
Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo and Lisandra Silva. |
Assume-Guarantee Reasoning with Scheduled Components |
Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren Cofer and Eric Mercer. |
On-the-Fly Model Checking with Neural MCTS |
Ruiyang Xu and Karl Lieberherr. |
Permutation Invariance of Deep Neural Networks with ReLUs |
Diganta Mukhopadhyay, Kumar Madhukar and Mandayam Srivas. |
On the Termination of Borrow Checking in Featherweight Rust |
Etienne Payet, David J. Pearce and Fausto Spoto. |
The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS |
Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott Smolka and Scott Stoller. |
Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems |
Josefine Graebener, Apurva Badithela and Richard Murray. |
DSV: Disassembly Soundness Validation without Assuming a Ground Truth |
Xiaoxin An, Freek Verbeek and Binoy Ravindran. |
Closed-Loop ACAS Xu NNCS is Unsafe: Quantized State Backreachability for Verification |
Stanley Bak and Hoang Dung Tran. |
Approximate Translation from Floating-Point to Real-Interval Arithmetic |
Daisuke Ishii, Takashi Tomita and Toshiaki Aoki. |
Hierarchical Contract-based Synthesis for Assurance Cases |
Timothy Wang, Zamira Daw, Pierluigi Nuzzo and Alessandro Pinto. |
Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning |
Andrea Pferscher and Bernhard K. Aichernig. |
Quantification of Battery Depletion Risk Made Efficient |
Gilles Nies and Holger Hermanns. |
Configurable Benchmarks for C Model Checkers |
Xaver Fink, Philipp Berger and Joost-Pieter Katoen. |
Timed Automata Learning via SMT Solving |
Martin Tappler, Bernhard K. Aichernig and Florian Lorber. |
Verified Probabilistic Policies for Deep Reinforcement Learning |
Edoardo Bacci and David Parker. |
Asynchronous Composition of Local Interface LTL Properties |
Alberto Bombardelli and Stefano Tonetta. |
Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan and Marielle Stoelinga. |
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees |
Exemplifying parametric timed specifications over signals with bounded behavior |
Étienne André, Masaki Waga, Natsuki Urabe and Ichiro Hasuo. |
Monitorability of Expressive Verdicts |
Felipe Gorostiaga and Cesar Sanchez. |
Requirements-Driven Model Checking and Test Generation for Comprehensive Verification |
Devesh Bhatt, Hao Ren, Anitha Murugesan, Jason Biatek, Srivatsan Varadarajan and Natrajan Shankar. |
Probabilistic Hyperproperties with Rewards |
Lukas Wilke, Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci and Borzoo Bonakdarpour. |
Hypercontracts |
Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli and Sanjit Seshia. |
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry |
Zachary Luppen, Michael Jacks, Nathan Baughman, Muhamed Stilic, Ryan Nasers, Benjamin Hertz, James Cutler, Dae Young Lee and Kristin Yvonne Rozier. |
Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I |
Alexis Aurandt, Phillip Jones and Kristin Yvonne Rozier. |
Incremental Transitive Closure for Zonal Abstract Domain |
Kenny Ballou and Elena Sherman. |
NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing |
Ulices Santa Cruz Leal and Yasser Shoukry. |
The Power of Disjoint Support Decompositions in Decision Diagrams |
Lieuwe Vinkhuijzen and Alfons Laarman. |
Proof Mate: an Interactive Proof Helper for PVS |
Paolo Masci and Aaron Dutle. |
Certified Computation of Nondeterministic Limits |
Michal Konecny, Sewon Park and Holger Thies. |
ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs |
Christopher Strong, Sydney Katz, Anthony Corso and Mykel Kochenderfer. |
Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT |
Baoluo Meng, Arjun Viswanathan, William Smith, Abha Moitra, Kit Siu and Michael Durling. |