| 2026 | IJCAR | A Deductive Refinement Calculus for Differential-Algebraic Programs. | Jonathan Hellwig, Long Qian, Andr Platzer |
| 2026 | IJCAR | Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements. | Enguerrand Prebet, Andr Platzer |
| 2026 | IJCAR | Complete Robust Hybrid Systems Reachability. | Noah Abou El Wafa, Andr Platzer |
| 2025 | CADE | A Real-Analytic Approach to Differential-Algebraic Dynamic Logic. | Jonathan Hellwig, Andr Platzer |
| 2025 | FMCAD | Can Large Language Models Autoformalize Kinematics? | Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch, Andr Platzer |
| 2025 | IFM | From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes. | Jonathan Hellwig, Lukas Schfer, Long Qian, Andr Platzer, Matthias Althoff |
| 2025 | IFM | Safe Temperature Regulation: Formally Verified and Real-World Validated. | Carlos Isasa, Noah Abou El Wafa, Cludio Gomes, Peter Gorm Larsen, Andr Platzer |
| 2025 | TABLEAUX | Semi-competitive Differential Game Logic. | Julia Butte, Andr Platzer |
| 2024 | IJCAR | Uniform Substitution for Differential Refinement Logic. | Enguerrand Prebet, Andr Platzer |
| 2024 | ISoLA | Intersymbolic AI - Interlinking Symbolic AI and Subsymbolic AI. | Andr Platzer |
| 2024 | LICS | Complete Game Logic with Sabotage. | Noah Abou El Wafa, Andr Platzer |
| 2024 | TACAS | CESAR: Control Envelope Synthesis via Angelic Refinements. | Aditi Kabra, Jonathan Laurent, Stefan Mitsch, Andr Platzer |
| 2023 | CADE | Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. | Marvin Brieger, Stefan Mitsch, Andr Platzer |
| 2023 | CPP | A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. | Katherine Kosaian, Yong Kiam Tan, Andr Platzer |
| 2022 | CADE | Implicit Definitions with Differential Equations for KeYmaera X - (System Description). | James Gallicchio, Yong Kiam Tan, Stefan Mitsch, Andr Platzer |
| 2021 | FM | Verified Quadratic Virtual Substitution for Real Arithmetic. | Matias Scharager, Katherine Cordwell, Stefan Mitsch, Andr Platzer |
| 2021 | ITP | A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. | Katherine Cordwell, Yong Kiam Tan, Andr Platzer |
| 2021 | TACAS | Deductive Stability Proofs for Ordinary Differential Equations. | Yong Kiam Tan, Andr Platzer |
| 2020 | CADE | Constructive Hybrid Games. | Rose Bohrer, Andr Platzer |
| 2020 | ESOP | Constructive Game Logic. | Rose Bohrer, Andr Platzer |
| 2020 | FSCD | Refining Constructive Hybrid Games. | Rose Bohrer, Andr Platzer |
| 2019 | CADE | dL | Rose Bohrer, Manuel Fernndez, Andr Platzer |
| 2019 | CADE | Towards Physical Hybrid Systems. | Katherine Cordwell, Andr Platzer |
| 2019 | CADE | Uniform Substitution at One Fell Swoop. | Andr Platzer |
| 2019 | EMSOFT | Verifiably safe SCUBA diving using commodity sensors: work-in-progress. | Viren Bajaj, Karim Elmaaroufi, Nathan Fulton, Andr Platzer |
| 2019 | FM | Pegasus: A Framework for Sound Continuous Invariant Generation. | Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, Andr Platzer |
| 2019 | FM | An Axiomatic Approach to Liveness for Differential Equations. | Yong Kiam Tan, Andr Platzer |
| 2019 | TABLEAUX | Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems. | Joo G. Martins, Andr Platzer, Joo Leite |
| 2019 | TACAS | Verifiably Safe Off-Model Reinforcement Learning. | Nathan Fulton, Andr Platzer |
| 2018 | AAAI | Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning. | Nathan Fulton, Andr Platzer |
| 2018 | CADE | Uniform Substitution for Differential Game Logic. | Andr Platzer |
| 2018 | FM | Vector Barrier Certificates and Comparison Systems. | Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, Andr Platzer |
| 2018 | ITC | Safe AI for CPS (Invited Paper). | Nathan Fulton, Andr Platzer |
| 2018 | LICS | A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow. | Rose Bohrer, Andr Platzer |
| 2018 | LICS | Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. | Andr Platzer, Yong Kiam Tan |
| 2018 | PLDI | VeriPhy: verified controller executables from verified cyber-physical system models. | Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, Andr Platzer |
| 2017 | CPP | Formally verified differential dynamic logic. | Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Vlp, Andr Platzer |
| 2017 | FASE | Change and Delay Contracts for Hybrid System Component Verification. | Andreas Mller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, Andr Platzer |
| 2017 | ITP | Bellerophon: Tactical Theorem Proving for Hybrid Systems. | Nathan Fulton, Stefan Mitsch, Rose Bohrer, Andr Platzer |
| 2016 | CADE | Logic & Proofs for Cyber-Physical Systems. | Andr Platzer |
| 2016 | CPP | A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. | Nathan Fulton, Andr Platzer |
| 2016 | IFM | A Component-Based Approach to Hybrid Systems Safety Verification. | Andreas Mller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, Andr Platzer |
| 2016 | LICS | Differential Refinement Logic. | Sarah M. Loos, Andr Platzer |
| 2016 | MEMOCODE | Keynote talk I: How to prove hybrid systems. | Andr Platzer |
| 2016 | VMCAI | A Method for Invariant Generation for Polynomial Continuous Systems. | Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, Andr Platzer |
| 2015 | CADE | KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. | Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Vlp, Andr Platzer |
| 2015 | CADE | A Uniform Substitution Calculus for Differential Dynamic Logic. | Andr Platzer |
| 2015 | EMSOFT | Forward invariant cuts to simplify proofs of safety. | Nikos Archiga, James Kapinski, Jyotirmoy V. Deshmukh, Andr Platzer, Bruce H. Krogh |
| 2015 | EMSOFT | Formal verification of ACAS X, an industrial airborne collision avoidance system. | Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, Andr Platzer |
| 2015 | FMCAD | Proving Hybrid Systems. | Andr Platzer |
| 2015 | TACAS | A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. | Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, Andr Platzer |
| 2015 | VMCAI | A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets. | Khalil Ghorbal, Andrew Sogokon, Andr Platzer |
| 2014 | CADE | dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. | Jean-Baptiste Jeannin, Andr Platzer |
| 2014 | FM | Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems. | Stefan Mitsch, Jan-David Quesel, Andr Platzer |
| 2014 | RV | ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models. | Stefan Mitsch, Andr Platzer |
| 2014 | SAS | Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations. | Khalil Ghorbal, Andrew Sogokon, Andr Platzer |
| 2014 | TACAS | Characterizing Algebraic Invariants by Differential Radical Invariants. | Khalil Ghorbal, Andr Platzer |
| 2013 | IJCAI | A Generalization of SAT and #SAT for Robust Policy Evaluation. | Erik Peter Zawadzki, Andr Platzer, Geoffrey J. Gordon |
| 2012 | CADE | Playing Hybrid Games with KeYmaera. | Jan-David Quesel, Andr Platzer |
| 2012 | ITP | A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). | Andr Platzer |
| 2012 | LICS | Logics of Dynamical Systems. | Andr Platzer |
| 2012 | LICS | The Complete Proof Theory of Hybrid Systems. | Andr Platzer |
| 2011 | CADE | Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs. | Andr Platzer |
| 2011 | CAV | Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial). | Andr Platzer |
| 2011 | FM | Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. | Sarah M. Loos, Andr Platzer, Ligia Nistor |
| 2011 | ICFEM | Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications. | Joo G. Martins, Andr Platzer, Joo Leite |
| 2011 | ICFEM | Distributed Theorem Proving for Distributed Hybrid Systems. | David W. Renshaw, Sarah M. Loos, Andr Platzer |
| 2010 | CADE | Real Analysis for Complex Systems. | Andr Platzer |
| 2010 | CSL | Quantified Differential Dynamic Logic for Distributed Hybrid Systems. | Andr Platzer |
| 2009 | CADE | Real World Verification. | Andr Platzer, Jan-David Quesel, Philipp Rmmer |
| 2009 | FM | Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. | Andr Platzer, Edmund M. Clarke |
| 2009 | ICFEM | European Train Control System: A Case Study in Formal Verification. | Andr Platzer, Jan-David Quesel |
| 2008 | CADE | KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). | Andr Platzer, Jan-David Quesel |
| 2008 | CAV | Computing Differential Invariants of Hybrid Systems as Fixedpoints. | Andr Platzer, Edmund M. Clarke |
| 2007 | CADE | Combining Deduction and Algebraic Constraints for Hybrid System Analysis. | Andr Platzer |
| 2007 | LFCS | A Temporal Dynamic Logic for Verifying Hybrid System Invariants. | Andr Platzer |
| 2007 | TABLEAUX | Differential Dynamic Logic for Verifying Parametric Hybrid Systems. | Andr Platzer |
| 2006 | CADE | Dynamic Logic with Non-rigid Functions. | Bernhard Beckert, Andr Platzer |