Google
Google Scholar
Semantic Scholar
IA Scholar
CiteSeerX
ORCIDAndré Platzer
Person information
- 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
- 2022
[j33]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)- [j32]André Platzer:
Correction to: Differential Dynamic Logic for Hybrid Systems. J. Autom. Reason. 66(1): 173 (2022) - 2021
- [d3]Katherine Cordwell, Yong Kiam Tan, André Platzer:
The BKR Decision Procedure for Univariate Real Arithmetic. Arch. Formal Proofs 2021 (2021) - [d2]Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer:
Verified Quadratic Virtual Substitution for Real Arithmetic. Arch. Formal Proofs 2021 (2021) - [j31]Yong Kiam Tan, André Platzer:
An axiomatic approach to existence and liveness for differential equations. Formal Aspects Comput. 33(4-5): 461-518 (2021) - [j30]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) - [j29]Brandon Bohrer, André Platzer:
Structured Proofs for Adversarial Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. 20(5s): 93:1-93:26 (2021) - [c94]Yong Kiam Tan, André Platzer:
Switched Systems as Hybrid Programs. ADHS 2021: 247-252 - [c93]Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer:
Verified Quadratic Virtual Substitution for Real Arithmetic. FM 2021: 200-217 - [c92]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 - [c91]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]Brandon 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
- [j28]André Platzer, Yong Kiam Tan:
Differential Equation Invariance Axiomatization. J. ACM 67(1): 6:1-6:66 (2020) - [c90]Brandon Bohrer, André Platzer:
Constructive Hybrid Games. IJCAR (1) 2020: 454-473 - [c89]Brandon Bohrer, André Platzer:
Constructive Game Logic. ESOP 2020: 84-111 - [c88]Brandon 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]Brandon Bohrer, André Platzer:
Constructive Hybrid Games. CoRR abs/2002.02536 (2020) - [i26]Brandon Bohrer, André Platzer:
Refining Constructive Hybrid Games. CoRR abs/2002.02576 (2020) - [i25]Brandon 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
- [d1]André Platzer:
Differential Game Logic. Arch. Formal Proofs 2019 (2019) - [j27]Brandon 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) - [c87]Brandon Bohrer, Manuel Fernández, André Platzer:
dLι: Definite Descriptions in Differential Dynamic Logic. CADE 2019: 94-110 - [c86]Katherine Cordwell, André Platzer:
Towards Physical Hybrid Systems. CADE 2019: 216-232 - [c85]André Platzer:
Uniform Substitution at One Fell Swoop. CADE 2019: 425-441 - [c84]Viren Bajaj, Karim Elmaaroufi, Nathan Fulton, André Platzer:
Verifiably safe SCUBA diving using commodity sensors: work-in-progress. EMSOFT Companion 2019: 8 - [c83]Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer:
Pegasus: A Framework for Sound Continuous Invariant Generation. FM 2019: 138-157 - [c82]Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Liveness for Differential Equations. FM 2019: 371-388 - [c81]Luis Garcia, Stefan Mitsch, André Platzer:
HyPLC: hybrid programmable logic controller program translation for verification. ICCPS 2019: 47-56 - [c80]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 - [c79]André Platzer:
The Logical Path to Autonomous Cyber-Physical Systems. QEST 2019: 25-33 - [c78]João G. Martins, André Platzer, João Leite:
Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems. TABLEAUX 2019: 428-445 - [c77]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]Brandon 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]Brandon 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 - [j26]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) - [c76]Nathan Fulton, André Platzer:
Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning. AAAI 2018: 6485-6492 - [c75]Brandon Bohrer, Adriel Luo, Xue An Chuang, André Platzer:
CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation. ADHS 2018: 55-60 - [c74]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 - [c73]André Platzer:
Uniform Substitution for Differential Game Logic. IJCAR 2018: 211-227 - [c72]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 - [c71]Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer:
Vector Barrier Certificates and Comparison Systems. FM 2018: 418-437 - [c70]Nathan Fulton, André Platzer:
Safe AI for CPS (Invited Paper). ITC 2018: 1-7 - [c69]Brandon Bohrer, André Platzer:
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow. LICS 2018: 115-124 - [c68]André Platzer, Yong Kiam Tan:
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. LICS 2018: 819-828 - [c67]Brandon 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
- [j25]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) - [j24]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) - [j23]André Platzer:
A Complete Uniform Substitution Calculus for Differential Dynamic Logic. J. Autom. Reason. 59(2): 219-265 (2017) - [j22]Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora 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) - [j21]André Platzer:
Differential Hybrid Games. ACM Trans. Comput. Log. 18(3): 19:1-19:44 (2017) - [c66]Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer:
Formally verified differential dynamic logic. CPP 2017: 208-221 - [c65]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 - [c64]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
Change and Delay Contracts for Hybrid System Component Verification. FASE 2017: 134-151 - [c63]Nathan Fulton, Stefan Mitsch, Brandon Bohrer, André Platzer:
Bellerophon: Tactical Theorem Proving for Hybrid Systems. ITP 2017: 207-224 - [c62]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
- [j20]Stefan Mitsch, André Platzer:
ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1-2): 33-74 (2016) - [j19]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) - [c61]André Platzer:
Logic & Proofs for Cyber-Physical Systems. IJCAR 2016: 15-21 - [c60]Nathan Fulton, André Platzer:
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. CPP 2016: 110-121 - [c59]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
A Component-Based Approach to Hybrid Systems Safety Verification. IFM 2016: 441-456 - [c58]Sarah M. Loos, André Platzer:
Differential Refinement Logic. LICS 2016: 505-514 - [c57]André Platzer:
Keynote talk I: How to prove hybrid systems. MEMOCODE 2016: 1 - [c56]Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer:
A Method for Invariant Generation for Polynomial Continuous Systems. VMCAI 2016: 268-288 - [c55]Stefan Mitsch, André Platzer:
The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving. F-IDE@FM 2016: 67-81 - [i9]André Platzer:
A Complete Uniform Substitution Calculus for Differential Dynamic Logic. CoRR abs/1601.06183 (2016) - [i8]Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, André Platzer:
Formal Verification of Obstacle Avoidance and Navigation of Ground Robots. CoRR abs/1605.00604 (2016) - 2015
- [j18]Stefan Mitsch, André Platzer, Werner Retschitzegger, Wieland Schwinger:
Logic-Based Modeling Approaches for Qualitative and Hybrid Reasoning in Dynamic Spatial Systems. ACM Comput. Surv. 48(1): 3:1-3:40 (2015) - [j17]Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, Bruce H. Krogh:
Numerically-aided Deductive Safety Proof for a Powertrain Control System. Electron. Notes Theor. Comput. Sci. 317: 19-25 (2015) - [j16]André Platzer:
Differential Game Logic. ACM Trans. Comput. Log. 17(1): 1:1-1:51 (2015) - [c54]André Platzer:
Ernst-Rüdiger Olderog: A Life for Meaning. Correct System Design 2015: 5-9 - [c53]André Platzer:
A Uniform Substitution Calculus for Differential Dynamic Logic. CADE 2015: 467-481 - [c52]Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer:
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. CADE 2015: 527-538 - [c51]Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora Schmidt, Erik Zawadzki, André Platzer:
Formal verification of ACAS X, an industrial airborne collision avoidance system. EMSOFT 2015: 127-136 - [c50]Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, Bruce H. Krogh:
Forward invariant cuts to simplify proofs of safety. EMSOFT 2015: 227-236 - [c49]André Platzer:
Proving Hybrid Systems. FMCAD 2015: 1 - [c48]Andreas Müller, Stefan Mitsch, André Platzer:
Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems. ITSC 2015: 757-764 - [c47]Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora Schmidt, Erik Zawadzki, André Platzer:
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System. TACAS 2015: 21-36 - [c46]Khalil Ghorbal, Andrew Sogokon, André Platzer:
A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets. VMCAI 2015: 431-448 - [e1]Roland Meyer, André Platzer, Heike Wehrheim:
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. Lecture Notes in Computer Science 9360, Springer 2015, ISBN 978-3-319-23505-9 [contents] - [i7]André Platzer:
A Uniform Substitution Calculus for Differential Dynamic Logic. CoRR abs/1503.01981 (2015) - [i6]André Platzer:
Differential Hybrid Games. CoRR abs/1507.04943 (2015) - [i5]Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, Bruce H. Krogh:
Forward Invariant Cuts to Simplify Proofs of Safety. CoRR abs/1507.05133 (2015) - 2014
- [j15]André Platzer:
Analog and Hybrid Computation: Dynamical Systems and Programming Languages. Bull. EATCS 114 (2014) - [j14]Khalil Ghorbal, Jean-Baptiste Jeannin, Erik Zawadzki, André Platzer, Geoffrey J. Gordon, Peter Capell:
Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges. J. Aerosp. Inf. Syst. 11(10): 702-713 (2014) - [j13]Stefan Mitsch, Grant Olney Passmore, André Platzer:
Collaborative Verification-Driven Engineering of Hybrid Systems. Math. Comput. Sci. 8(1): 71-97 (2014) - [j12]Akshay Rajhans, Ajinkya Bhave, Ivan Ruchkin, Bruce H. Krogh, David Garlan, André Platzer, Bradley R. Schmerl:
Supporting Heterogeneity in Cyber-Physical Systems Architectures. IEEE Trans. Autom. Control. 59(12): 3178-3193 (2014) - [c45]Jean-Baptiste Jeannin, André Platzer:
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. IJCAR 2014: 292-306 - [c44]Stefan Mitsch, Jan-David Quesel, André Platzer:
Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems. FM 2014: 481-496 - [c43]Stefan Mitsch, André Platzer:
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models. RV 2014: 199-214 - [c42]Khalil Ghorbal, Andrew Sogokon, André Platzer:
Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations. SAS 2014: 151-167 - [c41]Khalil Ghorbal, André Platzer:
Characterizing Algebraic Invariants by Differential Radical Invariants. TACAS 2014: 279-294 - [i4]Stefan Mitsch, Grant Olney Passmore, André Platzer:
Collaborative Verification-Driven Engineering of Hybrid Systems. CoRR abs/1403.6085 (2014) - [i3]André Platzer:
Differential Game Logic. CoRR abs/1408.1980 (2014) - 2013
- [j11]Paolo Zuliani, André Platzer, Edmund M. Clarke:
Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods Syst. Des. 43(2): 338-367 (2013) - [c40]Sarah M. Loos, David W. Renshaw, André Platzer:
Formal verification of distributed aircraft controllers. HSCC 2013: 125-130 - [c39]Yanni Kouskoulas, David W. Renshaw, André Platzer, Peter Kazanzides:
Certifying the safe design of a virtual fixture control algorithm for a surgical robot. HSCC 2013: 263-272 - [c38]Erik Peter Zawadzki, André Platzer, Geoffrey J. Gordon:
A Generalization of SAT and #SAT for Robust Policy Evaluation. IJCAI 2013: 2583-2590 - [c37]Sarah M. Loos, David Witmer, Peter Steenkiste, André Platzer:
Efficiency analysis of formally verified adaptive cruise controllers. ITSC 2013: 1565-1570 - [c36]Stefan Mitsch, Khalil Ghorbal, André Platzer:
On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. Robotics: Science and Systems 2013 - 2012
- [j10]André Platzer:
A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems. Log. Methods Comput. Sci. 8(4) (2012) - [j9]André Platzer:
Logical Analysis of Hybrid Systems: A Answer to a Complexity Challenge. J. Autom. Lang. Comb. 17(2-4): 265-275 (2012) - [c35]Nikos Aréchiga, Sarah M. Loos, André Platzer, Bruce H. Krogh:
Using theorem provers to guarantee closed-loop system properties. ACC 2012: 3573-3580 - [c34]Jan-David Quesel, André Platzer:
Playing Hybrid Games with KeYmaera. IJCAR 2012: 439-453 - [c33]André Platzer:
Logical Analysis of Hybrid Systems - A Complete Answer to a Complexity Challenge. DCFS 2012: 43-49 - [c32]Stefan Mitsch, Sarah M. Loos, André Platzer:
Towards Formal Verification of Freeway Traffic Control. ICCPS 2012: 171-180 - [c31]André Platzer:
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). ITP 2012: 28-48 - [c30]André Platzer:
Logics of Dynamical Systems. LICS 2012: 13-24 - [c29]André Platzer:
The Complete Proof Theory of Hybrid Systems. LICS 2012: 541-550 - [c28]David Henriques, João G. Martins, Paolo Zuliani, André Platzer, Edmund M. Clarke:
Statistical Model Checking for Markov Decision Processes. QEST 2012: 84-93 - [i2]André Platzer:
Dynamic Logics of Dynamical Systems. CoRR abs/1205.4788 (2012) - 2011
- [j8]