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...
share
research
∙
02/28/2023
Dynamic Logic of Communicating Hybrid Programs
This paper presents a dynamic logic dℒ_CHP for compositional deductive v...
research
∙
01/26/2023
Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems
Invariant sets are a key ingredient for verifying safety and other prope...
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...
research
∙
05/27/2022
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies
We propose a new approach to automated theorem proving and deductive pro...
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
∙
01/25/2022
First-Order Game Logic and Modal Mu-Calculus
This paper investigates first-order game logic and first-order modal mu-...
research
∙
11/02/2021
Verifying Switched System Stability With Logic
Switched systems are known to exhibit subtle (in)stability behaviors req...
research
∙
07/19/2021
Structured Proofs for Adversarial Cyber-Physical Systems
Many cyber-physical systems (CPS) are safety-critical, so it is importan...
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
∙
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
∙
02/20/2020
Constructive Game Logic
Game Logic is an excellent setting to study proofs-about-programs via th...
research
∙
02/07/2020
Refining Constructive Hybrid Games
We extend the constructive differential game logic (CdGL) of hybrid game...
research
∙
02/06/2020
Constructive Hybrid Games
Hybrid games are models which combine discrete, continuous, and adversar...
research
∙
10/24/2019
Overview of Logical Foundations of Cyber-Physical Systems
Cyber-physical systems (CPSs) are important whenever computer technology...
research
∙
08/15/2019
Toward Structured Proofs for Dynamic Logics
We present Kaisar, a structured interactive proof language for different...
research
∙
05/31/2019
Differential Equation Invariance Axiomatization
This article proves the completeness of an axiomatization for differenti...
research
∙
05/23/2019
Towards Physical Hybrid Systems
Some hybrid systems models are unsafe for mathematically correct but phy...
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/19/2019
Uniform Substitution At One Fell Swoop
Uniform substitution of function, predicate, program or game symbols is ...
research
∙
02/19/2019
Uniform Substitution in One Fell Swoop
Uniform substitution of function, predicate, program or game symbols is ...
research
∙
02/14/2019
Verifiably Safe Off-Model Reinforcement Learning
The desire to use reinforcement learning in safety-critical settings has...
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
Verified Runtime Validation for Partially Observable Hybrid Systems
Formal verification provides strong safety guarantees about models of cy...
research
∙
04/16/2018
Uniform Substitution for Differential Game Logic
This paper presents a uniform substitution calculus for differential gam...
research
∙
02/05/2018
