
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
We formalize the univariate fragment of BenOr, Kozen, and Reif's (BKR) ...
read it

Switched Systems as Hybrid Programs
Real world systems of interest often feature interactions between discre...
read it

Deductive Stability Proofs for Ordinary Differential Equations
Stability is required for real world controlled systems as it ensures th...
read it

Pegasus: Sound Continuous Invariant Generation
Continuous invariants are an important component in deductive verificati...
read it

An Axiomatic Approach to Existence and Liveness for Differential Equations
This article presents an axiomatic approach for deductive verification o...
read it

Constructive Game Logic
Game Logic is an excellent setting to study proofsaboutprograms via th...
read it

Refining Constructive Hybrid Games
We extend the constructive differential game logic (CdGL) of hybrid game...
read it

Constructive Hybrid Games
Hybrid games are models which combine discrete, continuous, and adversar...
read it

Overview of Logical Foundations of CyberPhysical Systems
Cyberphysical systems (CPSs) are important whenever computer technology...
read it

Toward Structured Proofs for Dynamic Logics
We present Kaisar, a structured interactive proof language for different...
read it

Differential Equation Invariance Axiomatization
This article proves the completeness of an axiomatization for differenti...
read it

Towards Physical Hybrid Systems
Some hybrid systems models are unsafe for mathematically correct but phy...
read it

An Axiomatic Approach to Liveness for Differential Equations
This paper presents an approach for deductive liveness verification for ...
read it

Blackbox EndtoEnd Verification of Ground Robot Safety and Liveness
We formally prove endtoend correctness of a ground robot implemented i...
read it

Uniform Substitution At One Fell Swoop
Uniform substitution of function, predicate, program or game symbols is ...
read it

Uniform Substitution in One Fell Swoop
Uniform substitution of function, predicate, program or game symbols is ...
read it

Verifiably Safe OffModel Reinforcement Learning
The desire to use reinforcement learning in safetycritical settings has...
read it

HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification
Programmable Logic Controllers (PLCs) provide a prominent choice of impl...
read it

Verified Runtime Validation for Partially Observable Hybrid Systems
Formal verification provides strong safety guarantees about models of cy...
read it

Uniform Substitution for Differential Game Logic
This paper presents a uniform substitution calculus for differential gam...
read it

Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
We prove the completeness of an axiomatization for differential equation...
read it
André Platzer
is this you? claim profile