98 citations · 647 across the 44 of their papers we have counts for
32 papers · 1 filter
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Marvin Brieger, Stefan Mitsch, André Platzer
This paper introduces a uniform substitution calculus for , the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious pr…
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…
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…
Structured Proofs for Adversarial Cyber-Physical Systems
Rose Bohrer, André Platzer
Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model's correctness specification always holds.…
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
Rachel Cleaveland, Stefan Mitsch, André Platzer
The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivi…
Verified Quadratic Virtual Substitution for Real Arithmetic
Matias Scharager, Katherine Cordwell, Stefan Mitsch +1
This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The…
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…
Refining Constructive Hybrid Games
Rose Bohrer, André Platzer
We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. We use this connective to prove a folk theorem…
Constructive Hybrid Games
Rose Bohrer, André Platzer
Hybrid games are models which combine discrete, continuous, and adversarial dynamics. Game logic enables proving (classical) existence of winning strategies. We introduce construct…
Constructive Game Logic
Rose Bohrer, André Platzer
Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective…
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…
Towards Physical Hybrid Systems
Katherine Cordwell, André Platzer
Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set…
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…
Uniform Substitution At One Fell Swoop
André Platzer
Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-crit…
Verified Runtime Validation for Partially Observable Hybrid Systems
Stefan Mitsch, André Platzer
Formal verification provides strong safety guarantees but only for models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physica…
Uniform Substitution for Differential Game Logic
André Platzer
This paper presents a uniform substitution calculus for differential game logic (dGL). Church's uniform substitutions substitute a term or formula for a function or predicate symbo…
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…
The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving
Stefan Mitsch, André Platzer
Hybrid systems verification is quite important for developing correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered…
A Complete Uniform Substitution Calculus for Differential Dynamic Logic
André Platzer
This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a for…