André Platzer

231 papers A* 13A 22B 28C 7Misc 3Journal 104Unranked 45
YearRankTypeTitle / Venue / Authors
2026 J jnl
Complete Robust Hybrid Systems Reachability.
CoRR
Noah Abou El Wafa, André Platzer
2026 J jnl
Differential elimination and algebraic invariants of polynomial dynamical systems.
Theor. Comput. Sci.
William Simmons, André Platzer
2026 J jnl
LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game.
CoRR
Aditi Kabra, Jonathan Laurent, Ruben Martins, Stefan Mitsch, André Platzer
2025 A conf
A Real-Analytic Approach to Differential-Algebraic Dynamic Logic.
CADE
Jonathan Hellwig, André Platzer
2025 J jnl
A Real-Analytic Approach to Differential-Algebraic Dynamic Logic.
CoRR
Jonathan Hellwig, André Platzer
2025 J jnl
Adaptive Shielding via Parametric Safety Proofs.
CoRR
Yao Feng, Jun Zhu, André Platzer, Jonathan Laurent
2025 J jnl
Adaptive Shielding via Parametric Safety Proofs.
Proc. ACM Program. Lang.
Yao Feng, Jun Zhu, André Platzer, Jonathan Laurent
2025 J jnl
Approximate Axiomatization for Differentially-Defined Functions.
CoRR
André Platzer, Long Qian
2025 J jnl
Axiomatization of Compact Initial Value Problems: Open Properties.
J. ACM
André Platzer, Long Qian
2025 B conf
Can Large Language Models Autoformalize Kinematics?
FMCAD
Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch, André Platzer
2025 J jnl
Can Large Language Models Autoformalize Kinematics?
CoRR
Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch, André Platzer
2025 J jnl
Complete First-Order Game Logic.
CoRR
Noah Abou El Wafa, André Platzer
2025 — conf
Correct-by-Construction Barrier Certificate Synthesis for Safety Verification of Continuous Dynamical Systems.
CDC
Promit Panja, André Platzer
2025 J jnl
Does Every Computer Scientist Need to Know Formal Methods?
Formal Aspects Comput.
Manfred Broy, Achim D. Brucker, Alessandro Fantechi, Mario Gleirscher, Klaus Havelund, Markus Alexander Kuppe, Alexandra Mendes, André Platzer, Jan Oliver Ringert, Allison Sullivan
2025 — ed.
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I
FM (1)
André Platzer, Kristin Yvonne Rozier, Matteo Pradella, Matteo Rossi
2025 — ed.
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II
FM (2)
André Platzer, Kristin Yvonne Rozier, Matteo Pradella, Matteo Rossi
2025 B conf
From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes.
iFM
Jonathan Hellwig, Lukas Schäfer, Long Qian, André Platzer, Matthias Althoff
2025 J jnl
From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes.
CoRR
Jonathan Hellwig, Lukas Schäfer, Long Qian, André Platzer, Matthias Althoff
2025 J jnl
Heterogeneous Dynamic Logic: Provability Modulo Program Theories.
CoRR
Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert
2025 J jnl
Hybrid Game Control Envelope Synthesis.
CoRR
Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer
2025 J jnl
Hybrid dynamical systems logic and its refinements.
Sci. Comput. Program.
André Platzer
2025 J jnl
Oracular Programming: A Modular Foundation for Building LLM-Enabled Software.
CoRR
Jonathan Laurent, André Platzer
2025 B conf
Safe Temperature Regulation: Formally Verified and Real-World Validated.
iFM
Carlos Isasa, Noah Abou El Wafa, Cláudio Gomes, Peter Gorm Larsen, André Platzer
2025 J jnl
Semi-Competitive Differential Game Logic.
CoRR
Julia Butte, André Platzer
2025 B conf
Semi-competitive Differential Game Logic.
TABLEAUX
Julia Butte, André Platzer
2025 C conf
Verification of Autonomous Neural Car Control with KeYmaera X.
ABZ
Enguerrand Prebet, Samuel Teuber, André Platzer
2025 J jnl
Verification of Autonomous Neural Car Control with KeYmaera X.
CoRR
Enguerrand Prebet, Samuel Teuber, André Platzer
2024 J jnl
Axiomatization of Compact Initial Value Problems: Open Properties.
CoRR
André Platzer, Long Qian
2024 — conf
CESAR: Control Envelope Synthesis via Angelic Refinements.
TACAS (1)
Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer
2024 J jnl
Complete Dynamic Logic of Communicating Hybrid Programs.
CoRR
Marvin Brieger, Stefan Mitsch, André Platzer
2024 A* conf
Complete Game Logic with Sabotage.
LICS
Noah Abou El Wafa, André Platzer
2024 J jnl
Complete Game Logic with Sabotage.
CoRR
Noah Abou El Wafa, André Platzer
2024 — conf
Intersymbolic AI - Interlinking Symbolic AI and Subsymbolic AI.
ISoLA (4)
André Platzer
2024 J jnl
Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI.
CoRR
André Platzer
2024 A* conf
Provably Safe Neural Network Controllers via Differential Dynamic Logic.
NeurIPS
Samuel Teuber, Stefan Mitsch, André Platzer
2024 J jnl
Provably Safe Neural Network Controllers via Differential Dynamic Logic.
CoRR
Samuel Teuber, Stefan Mitsch, André Platzer
2024 — conf
The Significance of Symbolic Logic for Scientific Education.
FMTea
André Platzer
2024 J jnl
The Significance of Symbolic Logic for Scientific Education.
CoRR
André Platzer
2024 — conf
Uniform Substitution for Differential Refinement Logic.
IJCAR (2)
Enguerrand Prebet, André Platzer
2024 J jnl
Uniform Substitution for Differential Refinement Logic.
CoRR
Enguerrand Prebet, André Platzer
2023 B conf
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.
CPP
Katherine Kosaian, Yong Kiam Tan, André Platzer
2023 J jnl
A Usage-Aware Sequent Calculus for Differential Dynamic Logic.
CoRR
Myra Dotzel, Stefan Mitsch, André Platzer
2023 J jnl
CESAR: Control Envelope Synthesis via Angelic Refinements.
CoRR
Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer
2023 J jnl
Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems.
CoRR
William Simmons, André Platzer
2023 J jnl
Dynamic Logic of Communicating Hybrid Programs.
CoRR
Marvin Brieger, Stefan Mitsch, André Platzer
2023 J jnl
Formally Verified Next-generation Airborne Collision Avoidance Games in ACAS X.
ACM Trans. Embed. Comput. Syst.
Rachel Cleaveland, Stefan Mitsch, André Platzer
2023 C conf
Refinements of Hybrid Dynamical Systems Logic.
ABZ
André Platzer
2023 — conf
Theorem Proving and Computer Algebra for Hybrid Systems (Keynote Abstract).
SC-Square@ISSAC
André Platzer
2023 A conf
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs.
CADE
Marvin Brieger, Stefan Mitsch, André Platzer
2023 J jnl
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs.
CoRR
Marvin Brieger, Stefan Mitsch, André Platzer
2022 J jnl
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.
Arch. Formal Proofs
Katherine Cordwell, Yong Kiam Tan, André Platzer
2022 J jnl
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.
CoRR
Katherine Kosaian, Yong Kiam Tan, André Platzer
2022 J jnl
Correction to: Differential Dynamic Logic for Hybrid Systems.
J. Autom. Reason.
André Platzer
2022 J jnl
First-Order Game Logic and Modal Mu-Calculus.
CoRR
Noah Abou El Wafa, André Platzer
2022 J jnl
Implicit Definitions with Differential Equations for KeYmaera X (System Description).
CoRR
James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer
2022 A conf
Implicit Definitions with Differential Equations for KeYmaera X - (System Description).
IJCAR
James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer
2022 J jnl
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies.
CoRR
Jonathan Laurent, André Platzer
2022 A* conf
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis.
NeurIPS
Jonathan Laurent, André Platzer
2022 J jnl
Safe and Resilient Practical Waypoint-Following for Autonomous Vehicles.
IEEE Control. Syst. Lett.
Qin Lin, Stefan Mitsch, André Platzer, John M. Dolan
2022 J jnl
Verified Train Controllers for the Federal Railroad Administration Train Kinematics Model: Balancing Competing Brake and Track Forces.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Aditi Kabra, Stefan Mitsch, André Platzer
2022 — conf
Verifying Switched System Stability With Logic.
HSCC
Yong Kiam Tan, Stefan Mitsch, André Platzer
2021 B conf
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm.
ITP
Katherine Cordwell, Yong Kiam Tan, André Platzer
2021 J jnl
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm.
CoRR
Katherine Cordwell, Yong Kiam Tan, André Platzer
2021 J jnl
An axiomatic approach to existence and liveness for differential equations.
Formal Aspects Comput.
Yong Kiam Tan, André Platzer
2021 A ed.
Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings
CADE
André Platzer, Geoff Sutcliffe
2021 J jnl
Correction to: How to model and prove hybrid systems with KeYmaera: a tutorial on safety.
Int. J. Softw. Tools Technol. Transf.
Jan-David Quesel, Stefan Mitsch, Sarah M. Loos, Nikos Aréchiga, André Platzer
2021 — conf
Deductive Stability Proofs for Ordinary Differential Equations.
TACAS (2)
Yong Kiam Tan, André Platzer
2021 J jnl
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X.
CoRR
Rachel Cleaveland, Stefan Mitsch, André Platzer
2021 J jnl
Pegasus: sound continuous invariant generation.
Formal Methods Syst. Des.
Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer
2021 J jnl
Structured Proofs for Adversarial Cyber-Physical Systems.
CoRR
Rose Bohrer, André Platzer
2021 J jnl
Structured Proofs for Adversarial Cyber-Physical Systems.
ACM Trans. Embed. Comput. Syst.
Rose Bohrer, André Platzer
2021 — conf
Switched Systems as Hybrid Programs.
ADHS
Yong Kiam Tan, André Platzer
2021 J jnl
Switched Systems as Hybrid Programs.
CoRR
Yong Kiam Tan, André Platzer
2021 J jnl
The BKR Decision Procedure for Univariate Real Arithmetic.
Arch. Formal Proofs
Katherine Cordwell, Yong Kiam Tan, André Platzer
2021 B conf
Verified Quadratic Virtual Substitution for Real Arithmetic.
FM
Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer
2021 J jnl
Verified Quadratic Virtual Substitution for Real Arithmetic.
Arch. Formal Proofs
Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer
2021 J jnl
Verified Quadratic Virtual Substitution for Real Arithmetic.
CoRR
Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer
2021 J jnl
Verifying Switched System Stability With Logic.
CoRR
Yong Kiam Tan, Stefan Mitsch, André Platzer
2020 — ch.
A Retrospective on Developing Hybrid System Provers in the KeYmaera Family - A Tale of Three Provers.
20 Years of KeY
Stefan Mitsch, André Platzer
2020 J jnl
An Axiomatic Approach to Existence and Liveness for Differential Equations.
CoRR
Yong Kiam Tan, André Platzer
2020 A conf
Constructive Game Logic.
ESOP
Rose Bohrer, André Platzer
2020 J jnl
Constructive Game Logic.
CoRR
Rose Bohrer, André Platzer
2020 — conf
Constructive Hybrid Games.
IJCAR (1)
Rose Bohrer, André Platzer
2020 J jnl
Constructive Hybrid Games.
CoRR
Rose Bohrer, André Platzer
2020 J jnl
Deductive Stability Proofs for Ordinary Differential Equations.
CoRR
Yong Kiam Tan, André Platzer
2020 J jnl
Differential Equation Invariance Axiomatization.
J. ACM
André Platzer, Yong Kiam Tan
2020 J jnl
Pegasus: Sound Continuous Invariant Generation.
CoRR
Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer
2020 B conf
Refining Constructive Hybrid Games.
FSCD
Rose Bohrer, André Platzer
2020 J jnl
Refining Constructive Hybrid Games.
CoRR
Rose Bohrer, André Platzer
2019 J jnl
A Formal Safety Net for Waypoint Following in Ground Robots.
CoRR
Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer
2019 J jnl
A Formal Safety Net for Waypoint-Following in Ground Robots.
IEEE Robotics Autom. Lett.
Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer
2019 B conf
An Axiomatic Approach to Liveness for Differential Equations.
FM
Yong Kiam Tan, André Platzer
2019 J jnl
An Axiomatic Approach to Liveness for Differential Equations.
CoRR
Yong Kiam Tan, André Platzer
2019 J jnl
Differential Equation Invariance Axiomatization.
CoRR
André Platzer, Yong Kiam Tan
2019 J jnl
Differential Game Logic.
Arch. Formal Proofs
André Platzer
2019 B conf
Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems.
TABLEAUX
João G. Martins, André Platzer, João Leite
2019 J jnl
HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification.
CoRR
Luis Garcia, Stefan Mitsch, André Platzer
2019 — conf
HyPLC: hybrid programmable logic controller program translation for verification.
ICCPS
Luis Garcia, Stefan Mitsch, André Platzer
2019 J jnl
Overview of Logical Foundations of Cyber-Physical Systems.
CoRR
André Platzer
2019 B conf
Pegasus: A Framework for Sound Continuous Invariant Generation.
FM
Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer
2019 — conf
The Logical Path to Autonomous Cyber-Physical Systems.
QEST
André Platzer
2019 J jnl
Toward Structured Proofs for Dynamic Logics.
CoRR
Rose Bohrer, André Platzer
2019 — conf
Toward multi-task support and security analyses in PLC program translation for verification: poster abstract.
ICCPS
Luis Garcia, Stefan Mitsch, André Platzer
2019 A conf
Towards Physical Hybrid Systems.
CADE
Katherine Cordwell, André Platzer
2019 J jnl
Towards Physical Hybrid Systems.
CoRR
Katherine Cordwell, André Platzer
2019 J jnl
Uniform Substitution At One Fell Swoop.
CoRR
André Platzer
2019 A conf
Uniform Substitution at One Fell Swoop.
CADE
André Platzer
2019 — conf
Verifiably Safe Off-Model Reinforcement Learning.
TACAS (1)
Nathan Fulton, André Platzer
2019 J jnl
Verifiably Safe Off-Model Reinforcement Learning.
CoRR
Nathan Fulton, André Platzer
2019 — conf
Verifiably safe SCUBA diving using commodity sensors: work-in-progress.
EMSOFT Companion
Viren Bajaj, Karim Elmaaroufi, Nathan Fulton, André Platzer
2019 A conf
dL
CADE
Rose Bohrer, Manuel Fernández, André Platzer
2018 — conf
A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration).
CyPhy/WESE
Andreas Müller, Stefan Mitsch, Wieland Schwinger, André Platzer
2018 A* conf
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow.
LICS
Rose Bohrer, André Platzer
2018 — conf
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving.
ARCH@ADHS
Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan
2018 — conf
CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation.
ADHS
Rose Bohrer, Adriel Luo, Xue An Chuang, André Platzer
2018 A* conf
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts.
LICS
André Platzer, Yong Kiam Tan
2018 J jnl
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts.
CoRR
André Platzer, Yong Kiam Tan
2018 — book
Logical Foundations of Cyber-Physical Systems
André Platzer
2018 A conf
Safe AI for CPS (Invited Paper).
ITC
Nathan Fulton, André Platzer
2018 A* conf
Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning.
AAAI
Nathan Fulton, André Platzer
2018 J jnl
Tactical contract composition for hybrid system component verification.
Int. J. Softw. Tools Technol. Transf.
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer
2018 A conf
Uniform Substitution for Differential Game Logic.
IJCAR
André Platzer
2018 J jnl
Uniform Substitution for Differential Game Logic.
CoRR
André Platzer
2018 B conf
Vector Barrier Certificates and Comparison Systems.
FM
Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer
2018 A* conf
VeriPhy: verified controller executables from verified cyber-physical system models.
PLDI
Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer
2018 — ch.
Verification of Hybrid Systems.
Handbook of Model Checking
Laurent Doyen, Goran Frehse, George J. Pappas, André Platzer
2018 J jnl
Verified Runtime Validation for Partially Observable Hybrid Systems.
CoRR
Stefan Mitsch, André Platzer
2017 — conf
A Benchmark for Component-based Hybrid Systems Safety Verification.
ARCH@CPSWeek
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer
2017 J jnl
A Complete Uniform Substitution Calculus for Differential Dynamic Logic.
J. Autom. Reason.
André Platzer
2017 J jnl
A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system.
Int. J. Softw. Tools Technol. Transf.
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora C. Schmidt, Ryan W. Gardner, Stefan Mitsch, André Platzer
2017 J jnl
A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets.
Comput. Lang. Syst. Struct.
Khalil Ghorbal, Andrew Sogokon, André Platzer
2017 B conf
Bellerophon: Tactical Theorem Proving for Hybrid Systems.
ITP
Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer
2017 B conf
Change and Delay Contracts for Hybrid System Component Verification.
FASE
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer
2017 J jnl
Differential Hybrid Games.
ACM Trans. Comput. Log.
André Platzer
2017 — conf
Formal Verification of Train Control with Air Pressure Brakes.
RSSRail
Stefan Mitsch, Marco Gario, Christof J. Budnik, Michael Golm, André Platzer
2017 J jnl
Formal verification of obstacle avoidance and navigation of ground robots.
Int. J. Robotics Res.
Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer
2017 B conf
Formally verified differential dynamic logic.
CPP
Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer
2016 J jnl
A Complete Uniform Substitution Calculus for Differential Dynamic Logic.
CoRR
André Platzer
2016 B conf
A Component-Based Approach to Hybrid Systems Safety Verification.
IFM
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer
2016 B conf
A Method for Invariant Generation for Polynomial Continuous Systems.
VMCAI
Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer
2016 B conf
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics.
CPP
Nathan Fulton, André Platzer
2016 A* conf
Differential Refinement Logic.
LICS
Sarah M. Loos, André Platzer
2016 J jnl
Formal Verification of Obstacle Avoidance and Navigation of Ground Robots.
CoRR
Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer
2016 J jnl
How to model and prove hybrid systems with KeYmaera: a tutorial on safety.
Int. J. Softw. Tools Technol. Transf.
Jan-David Quesel, Stefan Mitsch, Sarah M. Loos, Nikos Aréchiga, André Platzer
2016 C conf
Keynote talk I: How to prove hybrid systems.
MEMOCODE
André Platzer
2016 A conf
Logic & Proofs for Cyber-Physical Systems.
IJCAR
André Platzer
2016 J jnl
ModelPlex: verified runtime validation of verified cyber-physical system models.
Formal Methods Syst. Des.
Stefan Mitsch, André Platzer
2016 — conf
The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving.
F-IDE@FM
Stefan Mitsch, André Platzer
2015 A conf
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System.
TACAS
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, André Platzer
2015 B conf
A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets.
VMCAI
Khalil Ghorbal, Andrew Sogokon, André Platzer
2015 A conf
A Uniform Substitution Calculus for Differential Dynamic Logic.
CADE
André Platzer
2015 J jnl
A Uniform Substitution Calculus for Differential Dynamic Logic.
CoRR
André Platzer
2015 — ed.
Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings
Correct System Design
Roland Meyer, André Platzer, Heike Wehrheim
2015 J jnl
Differential Game Logic.
ACM Trans. Comput. Log.
André Platzer
2015 J jnl
Differential Hybrid Games.
CoRR
André Platzer
2015 — conf
Ernst-Rüdiger Olderog: A Life for Meaning.
Correct System Design
André Platzer
2015 Misc conf
Formal verification of ACAS X, an industrial airborne collision avoidance system.
EMSOFT
Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, André Platzer
2015 J jnl
Forward Invariant Cuts to Simplify Proofs of Safety.
CoRR
Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, Bruce H. Krogh
2015 Misc conf
Forward invariant cuts to simplify proofs of safety.
EMSOFT
Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, Bruce H. Krogh
2015 A conf
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems.
CADE
Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer
2015 J jnl
Logic-Based Modeling Approaches for Qualitative and Hybrid Reasoning in Dynamic Spatial Systems.
ACM Comput. Surv.
Stefan Mitsch, André Platzer, Werner Retschitzegger, Wieland Schwinger
2015 B conf
Proving Hybrid Systems.
FMCAD
André Platzer
2015 — conf
Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems.
ITSC
Andreas Müller, Stefan Mitsch, André Platzer
2014 J jnl
Analog and Hybrid Computation: Dynamical Systems and Programming Languages.
Bull. EATCS
André Platzer
2014 A conf
Characterizing Algebraic Invariants by Differential Radical Invariants.
TACAS
Khalil Ghorbal, André Platzer
2014 J jnl
Collaborative Verification-Driven Engineering of Hybrid Systems.
CoRR
Stefan Mitsch, Grant Olney Passmore, André Platzer
2014 J jnl
Collaborative Verification-Driven Engineering of Hybrid Systems.
Math. Comput. Sci.
Stefan Mitsch, Grant Olney Passmore, André Platzer
2014 J jnl
Differential Game Logic.
CoRR
André Platzer
2014 J jnl
Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges.
J. Aerosp. Inf. Syst.
Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, Peter Capell
2014 B conf
Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations.
SAS
Khalil Ghorbal, Andrew Sogokon, André Platzer
2014 B conf
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models.
RV
Stefan Mitsch, André Platzer
2014 — conf
Numerically-aided Deductive Safety Proof for a Powertrain Control System.
NSV
Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, Bruce H. Krogh
2014 B conf
Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems.
FM
Stefan Mitsch, Jan-David Quesel, André Platzer
2014 J jnl
Supporting Heterogeneity in Cyber-Physical Systems Architectures.
IEEE Trans. Autom. Control.
Akshay Rajhans, Ajinkya Bhave, Ivan Ruchkin, Bruce H. Krogh, David Garlan, André Platzer, Bradley R. Schmerl
2014 A conf
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems.
IJCAR
Jean-Baptiste Jeannin, André Platzer
2013 A* conf
A Generalization of SAT and #SAT for Robust Policy Evaluation.
IJCAI
Erik Peter Zawadzki, André Platzer, Geoffrey J. Gordon
2013 J jnl
Bayesian statistical model checking with application to Stateflow/Simulink verification.
Formal Methods Syst. Des.
Paolo Zuliani, André Platzer, Edmund M. Clarke
2013 — conf
Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
HSCC
Yanni Kouskoulas, David W. Renshaw, André Platzer, Peter Kazanzides
2013 — conf
Efficiency analysis of formally verified adaptive cruise controllers.
ITSC
Sarah M. Loos, David Witmer, Peter Steenkiste, André Platzer
2013 — conf
Formal verification of distributed aircraft controllers.
HSCC
Sarah M. Loos, David W. Renshaw, André Platzer
2013 — conf
On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles.
Robotics: Science and Systems
Stefan Mitsch, Khalil Ghorbal, André Platzer
2012 J jnl
A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems
Log. Methods Comput. Sci.
André Platzer
2012 B conf
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper).
ITP
André Platzer
2012 J jnl
Dynamic Logics of Dynamical Systems
CoRR
André Platzer
2012 — conf
Logical Analysis of Hybrid Systems - A Complete Answer to a Complexity Challenge.
DCFS
André Platzer
2012 J jnl
Logical Analysis of Hybrid Systems: A Answer to a Complexity Challenge.
J. Autom. Lang. Comb.
André Platzer
2012 A* conf
Logics of Dynamical Systems.
LICS
André Platzer
2012 A conf
Playing Hybrid Games with KeYmaera.
IJCAR
Jan-David Quesel, André Platzer
2012 — conf
Statistical Model Checking for Markov Decision Processes.
QEST
David Henriques, João G. Martins, Paolo Zuliani, André Platzer, Edmund M. Clarke
2012 A* conf
The Complete Proof Theory of Hybrid Systems.
LICS
André Platzer
2012 — conf
Towards Formal Verification of Freeway Traffic Control.
ICCPS
Stefan Mitsch, Sarah M. Loos, André Platzer
2012 C conf
Using theorem provers to guarantee closed-loop system properties.
ACC
Nikos Aréchiga, Sarah M. Loos, André Platzer, Bruce H. Krogh
2011 B conf
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified.
FM
Sarah M. Loos, André Platzer, Ligia Nistor
2011 A conf
An Instantiation-Based Theorem Prover for First-Order Programming.
AISTATS
Erik Zawadzki, Geoffrey J. Gordon, André Platzer
2011 C conf
Distributed Theorem Proving for Distributed Hybrid Systems.
ICFEM
David W. Renshaw, Sarah M. Loos, André Platzer
2011 A* conf
Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial).
CAV
André Platzer
2011 — conf
Quantified differential invariants.
HSCC
André Platzer
2011 J jnl
Quantifier Elimination over Finite Fields Using Gröbner Bases
CoRR
Sicun Gao, André Platzer, Edmund M. Clarke
2011 — conf
Quantifier Elimination over Finite Fields Using Gröbner Bases.
CAI
Sicun Gao, André Platzer, Edmund M. Clarke
2011 — conf
Safe intersections: At the crossing of hybrid systems and verification.
ITSC
Sarah M. Loos, André Platzer
2011 C conf
Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications.
ICFEM
João G. Martins, André Platzer, João Leite
2011 A conf
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.
CADE
André Platzer
2011 J jnl
The Structure of Differential Invariants and Differential Cut Elimination
Log. Methods Comput. Sci.
André Platzer
2011 — conf
Using parameters in architectural views to support heterogeneous design and verification.
CDC/ECC
Akshay Rajhans, Ajinkya Bhave, Sarah M. Loos, Bruce H. Krogh, André Platzer, David Garlan
2010 — conf
Bayesian statistical model checking with application to Simulink/Stateflow verification.
HSCC
Paolo Zuliani, André Platzer, Edmund M. Clarke
2010 J jnl
Differential Dynamic Logics.
Künstliche Intell.
André Platzer
2010 J jnl
Differential-algebraic Dynamic Logic for Differential-algebraic Programs.
J. Log. Comput.
André Platzer
2010 — book
Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics.
André Platzer
2010 B conf
Quantified Differential Dynamic Logic for Distributed Hybrid Systems.
CSL
André Platzer
2010 — conf
Real Analysis for Complex Systems.
VERIFY@IJCAR
André Platzer
2009 — conf
A Bayesian Approach to Model Checking Biological Systems.
CMSB
Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead, Axel Legay, André Platzer, Paolo Zuliani
2009 J jnl
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods Syst. Des.
André Platzer, Edmund M. Clarke
2009 C conf
European Train Control System: A Case Study in Formal Verification.
ICFEM
André Platzer, Jan-David Quesel
2009 B conf
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
FM
André Platzer, Edmund M. Clarke
2009 A conf
Real World Verification.
CADE
André Platzer, Jan-David Quesel, Philipp Rümmer
2009 J jnl
Verification of Cyberphysical Transportation Systems.
IEEE Intell. Syst.
André Platzer
2008 A* conf
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
CAV
André Platzer, Edmund M. Clarke
2008 J jnl
Differential Dynamic Logic for Hybrid Systems.
J. Autom. Reason.
André Platzer
2008 — —
Differential dynamic logics - automated theorem proving for hybrid systems.
André Platzer
2008 — ch.
Differentielle dynamische Logiken: Automatisches Beweisen für hybride Systeme [Differential Dynamic Logic: Automated Theorem Proving for Hybrid Systems].
Ausgezeichnete Informatikdissertationen
André Platzer
2008 A conf
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).
IJCAR
André Platzer, Jan-David Quesel
2008 — conf
Logical Verification and Systematic Parametric Analysis in Train Control.
HSCC
André Platzer, Jan-David Quesel
2007 Misc conf
A Temporal Dynamic Logic for Verifying Hybrid System Invariants.
LFCS
André Platzer
2007 — conf
Automating Verification of Cooperation, Control, and Design in Traffic Applications.
Formal Methods and Hybrid Real-Time Systems
Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken, Boris Wirtz
2007 — conf
Combining Deduction and Algebraic Constraints for Hybrid System Analysis.
VERIFY
André Platzer
2007 B conf
Differential Dynamic Logic for Verifying Parametric Hybrid Systems.
TABLEAUX
André Platzer
2007 — conf
Differential Logic for Reasoning About Hybrid Systems.
HSCC
André Platzer
2007 — conf
The Image Computation Problem in Hybrid Systems Model Checking.
HSCC
André Platzer, Edmund M. Clarke
2006 A conf
Dynamic Logic with Non-rigid Functions.
IJCAR
Bernhard Beckert, André Platzer
2006 — conf
SAT-based Abstraction Refinement for Real-time Systems.
FACS
Stephanie Kemper, André Platzer
2006 — conf
Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems.
HyLo@FLoC
André Platzer