40 citations · 86 across the 4 of their papers we have counts for
11 papers · 1 filter
First-Order Game Logic and Modal Mu-Calculus
Noah Abou El Wafa, André Platzer
This paper investigates first-order game logic and first-order modal mu-calculus, which extend their propositional modal logic counterparts with first-order modalities of interpret…
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…
Overview of Logical Foundations of Cyber-Physical Systems
André Platzer
Cyber-physical systems (CPSs) are important whenever computer technology interfaces with the physical world as it does in self-driving cars or aircraft control support systems. Due…
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…