André Platzer

is this you? claim profile

0 followers
Carnegie Mellon University

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) ...
02/05/2021 ∙ by Katherine Cordwell, et al. ∙ 0 ∙ share

read it
Switched Systems as Hybrid Programs

Real world systems of interest often feature interactions between discre...
01/15/2021 ∙ by Yong Kiam Tan, et al. ∙ 0 ∙ share

read it
Deductive Stability Proofs for Ordinary Differential Equations

Stability is required for real world controlled systems as it ensures th...
10/25/2020 ∙ by Yong Kiam Tan, et al. ∙ 0 ∙ share

read it
Pegasus: Sound Continuous Invariant Generation

Continuous invariants are an important component in deductive verificati...
05/19/2020 ∙ by Andrew Sogokon, et al. ∙ 0 ∙ share

read it
An Axiomatic Approach to Existence and Liveness for Differential Equations

This article presents an axiomatic approach for deductive verification o...
04/30/2020 ∙ by Yong Kiam Tan, et al. ∙ 0 ∙ share

read it
Constructive Game Logic

Game Logic is an excellent setting to study proofs-about-programs via th...
02/20/2020 ∙ by Brandon Bohrer, et al. ∙ 0 ∙ share

read it
Refining Constructive Hybrid Games

We extend the constructive differential game logic (CdGL) of hybrid game...
02/07/2020 ∙ by Brandon Bohrer, et al. ∙ 0 ∙ share

read it
Constructive Hybrid Games

Hybrid games are models which combine discrete, continuous, and adversar...
02/06/2020 ∙ by Brandon Bohrer, et al. ∙ 0 ∙ share

read it
Overview of Logical Foundations of Cyber-Physical Systems

Cyber-physical systems (CPSs) are important whenever computer technology...
10/24/2019 ∙ by André Platzer, et al. ∙ 0 ∙ share

read it
Toward Structured Proofs for Dynamic Logics

We present Kaisar, a structured interactive proof language for different...
08/15/2019 ∙ by Brandon Bohrer, et al. ∙ 0 ∙ share

read it
Differential Equation Invariance Axiomatization

This article proves the completeness of an axiomatization for differenti...
05/31/2019 ∙ by André Platzer, et al. ∙ 0 ∙ share

read it
Towards Physical Hybrid Systems

Some hybrid systems models are unsafe for mathematically correct but phy...
05/23/2019 ∙ by Katherine Cordwell, et al. ∙ 0 ∙ share

read it
An Axiomatic Approach to Liveness for Differential Equations

This paper presents an approach for deductive liveness verification for ...
04/16/2019 ∙ by Yong Kiam Tan, et al. ∙ 0 ∙ share

read it
Blackbox End-to-End Verification of Ground Robot Safety and Liveness

We formally prove end-to-end correctness of a ground robot implemented i...
03/12/2019 ∙ by Brandon Bohrer, et al. ∙ 0 ∙ share

read it
Uniform Substitution At One Fell Swoop

Uniform substitution of function, predicate, program or game symbols is ...
02/19/2019 ∙ by André Platzer, et al. ∙ 0 ∙ share

read it
Uniform Substitution in One Fell Swoop

Uniform substitution of function, predicate, program or game symbols is ...
02/19/2019 ∙ by André Platzer, et al. ∙ 0 ∙ share

read it
Verifiably Safe Off-Model Reinforcement Learning

The desire to use reinforcement learning in safety-critical settings has...
02/14/2019 ∙ by Nathan Fulton, et al. ∙ 0 ∙ share

read it
HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification

Programmable Logic Controllers (PLCs) provide a prominent choice of impl...
02/14/2019 ∙ by Luis Garcia, et al. ∙ 0 ∙ share

read it
Verified Runtime Validation for Partially Observable Hybrid Systems

Formal verification provides strong safety guarantees about models of cy...
11/15/2018 ∙ by Stefan Mitsch, et al. ∙ 0 ∙ share

read it
Uniform Substitution for Differential Game Logic

This paper presents a uniform substitution calculus for differential gam...
04/16/2018 ∙ by André Platzer, et al. ∙ 0 ∙ share

read it
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts

We prove the completeness of an axiomatization for differential equation...
02/05/2018 ∙ by André Platzer, et al. ∙ 0 ∙ share

read it

André Platzer

Featured Co-authors