39 citations · 158 across the 12 of their papers we have counts for
12 papers
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, André Platzer
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula…
Implicit Definitions with Differential Equations for KeYmaera X (System Description)
James Gallicchio, Yong Kiam Tan, Stefan Mitsch +1
Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the h…
Verifying Switched System Stability With Logic
Yong Kiam Tan, Stefan Mitsch, André Platzer
Switched systems are known to exhibit subtle (in)stability behaviors requiring system designers to carefully analyze the stability of closed-loop systems that arise from their prop…
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…
Deductive Stability Proofs for Ordinary Differential Equations
Yong Kiam Tan, André Platzer
Stability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This pa…
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…
An Axiomatic Approach to Existence and Liveness for Differential Equations
Yong Kiam Tan, André Platzer
This article presents an axiomatic approach for deductive verification of existence and liveness for ordinary differential equations (ODEs) with differential dynamic logic (dL). Th…
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…
A Formal Safety Net for Waypoint Following in Ground Robots
Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch +2
We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for 2D waypoint-following of Dubins-type ground robots with tolerances an…
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…