research
∙
05/15/2023
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
Technology advances give us the hope of driving without human error, red...
share
research
∙
03/30/2023
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
This paper introduces a uniform substitution calculus for dℒ_CHP, the dy...
research
∙
02/28/2023
Dynamic Logic of Communicating Hybrid Programs
This paper presents a dynamic logic dℒ_CHP for compositional deductive v...
research
∙
03/02/2022
Implicit Definitions with Differential Equations for KeYmaera X (System Description)
Definition packages in theorem provers provide users with means of defin...
research
∙
11/02/2021
Verifying Switched System Stability With Logic
Switched systems are known to exhibit subtle (in)stability behaviors req...
research
∙
08/06/2021
Implicit and Explicit Proof Management in KeYmaera X
Hybrid systems theorem proving provides strong correctness guarantees ab...
research
∙
06/03/2021
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
The design of aircraft collision avoidance algorithms is a subtle but im...
research
∙
05/29/2021
Verified Quadratic Virtual Substitution for Real Arithmetic
This paper presents a formally verified quantifier elimination (QE) algo...
research
∙
06/22/2020
Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned Systems
Machine learning becomes increasingly important to tune or even synthesi...
research
∙
05/19/2020
Pegasus: Sound Continuous Invariant Generation
Continuous invariants are an important component in deductive verificati...
research
∙
07/05/2019
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
Computer-Controlled Systems (CCS) are a subclass of hybrid systems where...
research
∙
06/13/2019
Modeling and Verifying Cyber-Physical Systems with Hybrid Active Objects
Formal modeling of cyber-physical systems (CPS) is hard, because they po...
research
∙
03/12/2019
Blackbox End-to-End Verification of Ground Robot Safety and Liveness
We formally prove end-to-end correctness of a ground robot implemented i...
research
∙
02/14/2019
HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification
Programmable Logic Controllers (PLCs) provide a prominent choice of impl...
research
∙
11/15/2018