6 papers
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…
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…
Differential Equation Invariance Axiomatization
André Platzer, Yong Kiam Tan
This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differe…
An Axiomatic Approach to Liveness for Differential Equations
Yong Kiam Tan, André Platzer
This paper presents an approach for deductive liveness verification for ordinary differential equations (ODEs) with differential dynamic logic. Numerous subtleties complicate the g…
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
André Platzer, Yong Kiam Tan
We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete…