98 citations · 647 across the 44 of their papers we have counts for
44 papers
A Usage-Aware Sequent Calculus for Differential Dynamic Logic
Myra Dotzel, Stefan Mitsch, André Platzer
Ensuring that safety-critical applications behave as intended is an important yet challenging task. Modeling languages like differential dynamic logic (dL) have proof calculi capab…
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…
Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems
William Simmons, André Platzer
Invariant sets are a key ingredient for verifying safety and other properties of cyber-physical systems that mix discrete and continuous dynamics. We adapt the elimination-theoreti…
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…
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis
Jonathan Laurent, André Platzer
We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministi…
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…