39 citations · 158 across the 12 of their papers we have counts for
9 papers · 1 filter
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…
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…
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…
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…