default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAndré Platzer
Person information
- affiliation: Karlsruhe Institute of Technology, Germany
- affiliation: Carnegie Mellon University, Computer Science Department, Pittsburgh, PA, USA
- affiliation (PhD 2008): Carl von Ossietzky University, Oldenburg, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2025
[j38]André Platzer
:
Hybrid dynamical systems logic and its refinements. Sci. Comput. Program. 239: 103179 (2025)- [e4]André Platzer, Kristin Yvonne Rozier, Matteo Pradella, Matteo Rossi:
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14933, Springer 2025, ISBN 978-3-031-71161-9 [contents] - [e3]André Platzer, Kristin Yvonne Rozier, Matteo Pradella, Matteo Rossi:
Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II. Lecture Notes in Computer Science 14934, Springer 2025, ISBN 978-3-031-71176-3 [contents] - 2024
- [c109]Enguerrand Prebet, André Platzer:
Uniform Substitution for Differential Refinement Logic. IJCAR (2) 2024: 196-215 - [c108]André Platzer:
Intersymbolic AI - Interlinking Symbolic AI and Subsymbolic AI. ISoLA (4) 2024: 162-180 - [c107]Noah Abou El Wafa, André Platzer:
Complete Game Logic with Sabotage. LICS 2024: 1:1-1:15 - [c106]Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer:
CESAR: Control Envelope Synthesis via Angelic Refinements. TACAS (1) 2024: 144-164 - [c105]André Platzer:
The Significance of Symbolic Logic for Scientific Education. FMTea 2024: 3-22 - [i49]Samuel Teuber, Stefan Mitsch, André Platzer:
Provably Safe Neural Network Controllers via Differential Dynamic Logic. CoRR abs/2402.10998 (2024) - [i48]Noah Abou El Wafa, André Platzer:
Complete Game Logic with Sabotage. CoRR abs/2404.09873 (2024) - [i47]Enguerrand Prebet, André Platzer:
Uniform Substitution for Differential Refinement Logic. CoRR abs/2404.16734 (2024) - [i46]André Platzer:
Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI. CoRR abs/2406.11563 (2024) - [i45]André Platzer:
The Significance of Symbolic Logic for Scientific Education. CoRR abs/2407.09959 (2024) - [i44]Marvin Brieger, Stefan Mitsch, André Platzer:
Complete Dynamic Logic of Communicating Hybrid Programs. CoRR abs/2408.05012 (2024) - [i43]André Platzer, Long Qian:
Axiomatization of Compact Initial Value Problems: Open Properties. CoRR abs/2410.13836 (2024) - 2023
- [j37]Rachel Cleaveland, Stefan Mitsch, André Platzer:
Formally Verified Next-generation Airborne Collision Avoidance Games in ACAS X. ACM Trans. Embed. Comput. Syst. 22(1): 10:1-10:30 (2023) - [c104]Marvin Brieger, Stefan Mitsch, André Platzer:
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. CADE 2023: 96-115 - [c103]Katherine Kosaian, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. CPP 2023: 211-224 - [c102]André Platzer:
Theorem Proving and Computer Algebra for Hybrid Systems (Keynote Abstract). SC-Square@ISSAC 2023: 10 - [c101]André Platzer:
Refinements of Hybrid Dynamical Systems Logic. ABZ 2023: 3-14 - [i42]William Simmons, André Platzer:
Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems. CoRR abs/2301.10935 (2023) - [i41]Marvin Brieger, Stefan Mitsch, André Platzer:
Dynamic Logic of Communicating Hybrid Programs. CoRR abs/2302.14546 (2023) - [i40]Marvin Brieger, Stefan Mitsch, André Platzer:
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. CoRR abs/2303.17333 (2023) - [i39]Myra Dotzel, Stefan Mitsch, André Platzer:
A Usage-Aware Sequent Calculus for Differential Dynamic Logic. CoRR abs/2309.01180 (2023) - [i38]Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer:
CESAR: Control Envelope Synthesis via Angelic Refinements. CoRR abs/2311.02833 (2023) - 2022
- [j36]Katherine Cordwell, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. Arch. Formal Proofs 2022 (2022) - [j35]Qin Lin, Stefan Mitsch, André Platzer, John M. Dolan:
Safe and Resilient Practical Waypoint-Following for Autonomous Vehicles. IEEE Control. Syst. Lett. 6: 1574-1579 (2022) - [j34]André Platzer:
Correction to: Differential Dynamic Logic for Hybrid Systems. J. Autom. Reason. 66(1): 173 (2022) - [j33]Aditi Kabra, Stefan Mitsch, André Platzer:
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. 41(11): 4409-4420 (2022) - [c100]James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer:
Implicit Definitions with Differential Equations for KeYmaera X - (System Description). IJCAR 2022: 723-733 - [c99]Yong Kiam Tan, Stefan Mitsch, André Platzer:
Verifying Switched System Stability With Logic. HSCC 2022: 2:1-2:11 - [c98]Jonathan Laurent, André Platzer:
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis. NeurIPS 2022 - [i37]Noah Abou El Wafa, André Platzer:
First-Order Game Logic and Modal Mu-Calculus. CoRR abs/2201.10012 (2022) - [i36]James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer:
Implicit Definitions with Differential Equations for KeYmaera X (System Description). CoRR abs/2203.01272 (2022) - [i35]Jonathan Laurent, André Platzer:
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies. CoRR abs/2205.14229 (2022) - [i34]Katherine Kosaian, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. CoRR abs/2209.10978 (2022) - 2021
- [j32]Katherine Cordwell, Yong Kiam Tan, André Platzer:
The BKR Decision Procedure for Univariate Real Arithmetic. Arch. Formal Proofs 2021 (2021) - [j31]Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer:
Verified Quadratic Virtual Substitution for Real Arithmetic. Arch. Formal Proofs 2021 (2021) - [j30]Yong Kiam Tan, André Platzer:
An axiomatic approach to existence and liveness for differential equations. Formal Aspects Comput. 33(4-5): 461-518 (2021) - [j29]Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer:
Pegasus: sound continuous invariant generation. Formal Methods Syst. Des. 58(1-2): 5-41 (2021) - [j28]Jan-David Quesel, Stefan Mitsch, Sarah M. Loos, Nikos Aréchiga, André Platzer:
Correction to: How to model and prove hybrid systems with KeYmaera: a tutorial on safety. Int. J. Softw. Tools Technol. Transf. 23(5): 827 (2021) - [j27]Rose Bohrer, André Platzer:
Structured Proofs for Adversarial Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. 20(5s): 93:1-93:26 (2021) - [c97]Yong Kiam Tan, André Platzer:
Switched Systems as Hybrid Programs. ADHS 2021: 247-252 - [c96]Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer:
Verified Quadratic Virtual Substitution for Real Arithmetic. FM 2021: 200-217 - [c95]Katherine Cordwell, Yong Kiam Tan, André Platzer:
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. ITP 2021: 14:1-14:20 - [c94]Yong Kiam Tan, André Platzer:
Deductive Stability Proofs for Ordinary Differential Equations. TACAS (2) 2021: 181-199 - [e2]André Platzer, Geoff Sutcliffe:
Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. Lecture Notes in Computer Science 12699, Springer 2021, ISBN 978-3-030-79875-8 [contents] - [i33]Yong Kiam Tan, André Platzer:
Switched Systems as Hybrid Programs. CoRR abs/2101.06195 (2021) - [i32]Katherine Cordwell, Yong Kiam Tan, André Platzer:
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. CoRR abs/2102.03003 (2021) - [i31]Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer:
Verified Quadratic Virtual Substitution for Real Arithmetic. CoRR abs/2105.14183 (2021) - [i30]Rachel Cleaveland, Stefan Mitsch, André Platzer:
Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X. CoRR abs/2106.02030 (2021) - [i29]Rose Bohrer, André Platzer:
Structured Proofs for Adversarial Cyber-Physical Systems. CoRR abs/2107.08852 (2021) - [i28]Yong Kiam Tan, Stefan Mitsch, André Platzer:
Verifying Switched System Stability With Logic. CoRR abs/2111.01928 (2021) - 2020
- [j26]André Platzer, Yong Kiam Tan:
Differential Equation Invariance Axiomatization. J. ACM 67(1): 6:1-6:66 (2020) - [c93]Rose Bohrer, André Platzer:
Constructive Hybrid Games. IJCAR (1) 2020: 454-473 - [c92]Rose Bohrer, André Platzer:
Constructive Game Logic. ESOP 2020: 84-111 - [c91]Rose Bohrer, André Platzer:
Refining Constructive Hybrid Games. FSCD 2020: 14:1-14:19 - [p3]Stefan Mitsch, André Platzer:
A Retrospective on Developing Hybrid System Provers in the KeYmaera Family - A Tale of Three Provers. 20 Years of KeY 2020: 21-64 - [i27]Rose Bohrer, André Platzer:
Constructive Hybrid Games. CoRR abs/2002.02536 (2020) - [i26]Rose Bohrer, André Platzer:
Refining Constructive Hybrid Games. CoRR abs/2002.02576 (2020) - [i25]Rose Bohrer, André Platzer:
Constructive Game Logic. CoRR abs/2002.08523 (2020) - [i24]Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Existence and Liveness for Differential Equations. CoRR abs/2004.14561 (2020) - [i23]Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer:
Pegasus: Sound Continuous Invariant Generation. CoRR abs/2005.09348 (2020) - [i22]Yong Kiam Tan, André Platzer:
Deductive Stability Proofs for Ordinary Differential Equations. CoRR abs/2010.13096 (2020)
2010 – 2019
- 2019
- [j25]André Platzer:
Differential Game Logic. Arch. Formal Proofs 2019 (2019) - [j24]Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer:
A Formal Safety Net for Waypoint-Following in Ground Robots. IEEE Robotics Autom. Lett. 4(3): 2910-2917 (2019) - [c90]Rose Bohrer, Manuel Fernández, André Platzer:
dLι: Definite Descriptions in Differential Dynamic Logic. CADE 2019: 94-110 - [c89]Katherine Cordwell, André Platzer:
Towards Physical Hybrid Systems. CADE 2019: 216-232 - [c88]André Platzer:
Uniform Substitution at One Fell Swoop. CADE 2019: 425-441 - [c87]Viren Bajaj, Karim Elmaaroufi, Nathan Fulton, André Platzer:
Verifiably safe SCUBA diving using commodity sensors: work-in-progress. EMSOFT Companion 2019: 8 - [c86]Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer:
Pegasus: A Framework for Sound Continuous Invariant Generation. FM 2019: 138-157 - [c85]Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Liveness for Differential Equations. FM 2019: 371-388 - [c84]Luis Garcia, Stefan Mitsch, André Platzer:
HyPLC: hybrid programmable logic controller program translation for verification. ICCPS 2019: 47-56 - [c83]Luis Garcia, Stefan Mitsch, André Platzer:
Toward multi-task support and security analyses in PLC program translation for verification: poster abstract. ICCPS 2019: 348-349 - [c82]André Platzer:
The Logical Path to Autonomous Cyber-Physical Systems. QEST 2019: 25-33 - [c81]João G. Martins, André Platzer, João Leite:
Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems. TABLEAUX 2019: 428-445 - [c80]Nathan Fulton, André Platzer:
Verifiably Safe Off-Model Reinforcement Learning. TACAS (1) 2019: 413-430 - [i21]Luis Garcia, Stefan Mitsch, André Platzer:
HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification. CoRR abs/1902.05205 (2019) - [i20]Nathan Fulton, André Platzer:
Verifiably Safe Off-Model Reinforcement Learning. CoRR abs/1902.05632 (2019) - [i19]André Platzer:
Uniform Substitution At One Fell Swoop. CoRR abs/1902.07230 (2019) - [i18]Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer:
A Formal Safety Net for Waypoint Following in Ground Robots. CoRR abs/1903.05073 (2019) - [i17]Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Liveness for Differential Equations. CoRR abs/1904.07984 (2019) - [i16]Katherine Cordwell, André Platzer:
Towards Physical Hybrid Systems. CoRR abs/1905.09520 (2019) - [i15]André Platzer, Yong Kiam Tan:
Differential Equation Invariance Axiomatization. CoRR abs/1905.13429 (2019) - [i14]Rose Bohrer, André Platzer:
Toward Structured Proofs for Dynamic Logics. CoRR abs/1908.05535 (2019) - [i13]André Platzer:
Overview of Logical Foundations of Cyber-Physical Systems. CoRR abs/1910.11232 (2019) - 2018
- [b3]André Platzer:
Logical Foundations of Cyber-Physical Systems. Springer 2018, ISBN 978-3-319-63587-3, pp. 1-639 - [j23]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
Tactical contract composition for hybrid system component verification. Int. J. Softw. Tools Technol. Transf. 20(6): 615-643 (2018) - [c79]Nathan Fulton, André Platzer:
Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning. AAAI 2018: 6485-6492 - [c78]Rose Bohrer, Adriel Luo, Xue An Chuang, André Platzer:
CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation. ADHS 2018: 55-60 - [c77]Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan:
ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving. ARCH@ADHS 2018: 110-127 - [c76]André Platzer:
Uniform Substitution for Differential Game Logic. IJCAR 2018: 211-227 - [c75]Andreas Müller, Stefan Mitsch, Wieland Schwinger, André Platzer:
A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration). CyPhy/WESE 2018: 91-110 - [c74]Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer:
Vector Barrier Certificates and Comparison Systems. FM 2018: 418-437 - [c73]Nathan Fulton, André Platzer:
Safe AI for CPS (Invited Paper). ITC 2018: 1-7 - [c72]Rose Bohrer, André Platzer:
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow. LICS 2018: 115-124 - [c71]André Platzer, Yong Kiam Tan:
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. LICS 2018: 819-828 - [c70]Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer:
VeriPhy: verified controller executables from verified cyber-physical system models. PLDI 2018: 617-630 - [p2]Laurent Doyen, Goran Frehse, George J. Pappas, André Platzer:
Verification of Hybrid Systems. Handbook of Model Checking 2018: 1047-1110 - [i12]André Platzer, Yong Kiam Tan:
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. CoRR abs/1802.01226 (2018) - [i11]André Platzer:
Uniform Substitution for Differential Game Logic. CoRR abs/1804.05880 (2018) - [i10]Stefan Mitsch, André Platzer:
Verified Runtime Validation for Partially Observable Hybrid Systems. CoRR abs/1811.06502 (2018) - 2017
- [j22]Khalil Ghorbal, Andrew Sogokon, André Platzer:
A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct. 47: 19-43 (2017) - [j21]Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer:
Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robotics Res. 36(12): 1312-1340 (2017) - [j20]André Platzer:
A Complete Uniform Substitution Calculus for Differential Dynamic Logic. J. Autom. Reason. 59(2): 219-265 (2017) - [j19]Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora C. Schmidt, Ryan W. Gardner, Stefan Mitsch, André Platzer:
A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. Int. J. Softw. Tools Technol. Transf. 19(6): 717-741 (2017) - [j18]André Platzer:
Differential Hybrid Games. ACM Trans. Comput. Log. 18(3): 19:1-19:44 (2017) - [c69]Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer:
Formally verified differential dynamic logic. CPP 2017: 208-221 - [c68]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
A Benchmark for Component-based Hybrid Systems Safety Verification. ARCH@CPSWeek 2017: 65-74 - [c67]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
Change and Delay Contracts for Hybrid System Component Verification. FASE 2017: 134-151 - [c66]Nathan Fulton, Stefan Mitsch, Rose Bohrer, André Platzer:
Bellerophon: Tactical Theorem Proving for Hybrid Systems. ITP 2017: 207-224 - [c65]Stefan Mitsch, Marco Gario, Christof J. Budnik, Michael Golm, André Platzer:
Formal Verification of Train Control with Air Pressure Brakes. RSSRail 2017: 173-191 - 2016
- [j17]Stefan Mitsch, André Platzer:
ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1-2): 33-74 (2016) - [j16]Jan-David Quesel, Stefan Mitsch, Sarah M. Loos, Nikos Aréchiga, André Platzer:
How to model and prove hybrid systems with KeYmaera: a tutorial on safety. Int. J. Softw. Tools Technol. Transf. 18(1): 67-91 (2016) - [c64]André Platzer:
Logic & Proofs for Cyber-Physical Systems. IJCAR 2016: 15-21 - [c63]Nathan Fulton, André Platzer:
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. CPP 2016: 110-121 - [c62]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
A Component-Based Approach to Hybrid Systems Safety Verification. IFM 2016: 441-456 - [c61]Sarah M. Loos, André Platzer:
Differential Refinement Logic. LICS 2016: 505-514 - [c60]André Platzer:
Keynote talk I: How to prove hybrid systems. MEMOCODE 2016: 1 - [c59]Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer:
A Method for Invariant Generation for Polynomial Continuous Systems. VMCAI 2016: 268-288 - [c58]Stefan Mitsch, André Platzer:
The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving. F-IDE@FM 2016: 67-81 - [i9]