research
∙
09/22/2022
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
We formalize a multivariate quantifier elimination (QE) algorithm in the...
share
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
∙
02/05/2021
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR) ...
research
∙
01/15/2021
Switched Systems as Hybrid Programs
Real world systems of interest often feature interactions between discre...
research
∙
10/25/2020
Deductive Stability Proofs for Ordinary Differential Equations
Stability is required for real world controlled systems as it ensures th...
research
∙
05/19/2020
Pegasus: Sound Continuous Invariant Generation
Continuous invariants are an important component in deductive verificati...
research
∙
04/30/2020
An Axiomatic Approach to Existence and Liveness for Differential Equations
This article presents an axiomatic approach for deductive verification o...
research
∙
05/31/2019
Differential Equation Invariance Axiomatization
This article proves the completeness of an axiomatization for differenti...
research
∙
04/16/2019
An Axiomatic Approach to Liveness for Differential Equations
This paper presents an approach for deductive liveness verification for ...
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/05/2018
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
We prove the completeness of an axiomatization for differential equation...
research
∙
06/15/2016