98 citations · 647 across the 44 of their papers we have counts for
5 papers · 2 filters
Structured Proofs for Adversarial Cyber-Physical Systems
Rose Bohrer, André Platzer
Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model's correctness specification always holds.…
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
Rachel Cleaveland, Stefan Mitsch, André Platzer
The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivi…
Verified Quadratic Virtual Substitution for Real Arithmetic
Matias Scharager, Katherine Cordwell, Stefan Mitsch +1
This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The…
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
Katherine Cordwell, Yong Kiam Tan, André Platzer
We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR) decision procedure for first-order real arithmetic in Isabelle/HOL. BKR's algorithm has good potential for p…
Switched Systems as Hybrid Programs
Yong Kiam Tan, André Platzer
Real world systems of interest often feature interactions between discrete and continuous dynamics. Various hybrid system formalisms have been used to model and analyze this combin…