2 papers
cs.LO2021
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…
cs.SC2020
Pegasus: Sound Continuous Invariant Generation
Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan +2
Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in d…