14 citations · 37 across the 7 of their papers we have counts for
3 papers · 1 filter
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…
Towards Physical Hybrid Systems
Katherine Cordwell, André Platzer
Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set…