Google
Google Scholar
Semantic Scholar
MS Academic
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
- 2020
[j28]André Platzer
, Yong Kiam Tan:
Differential Equation Invariance Axiomatization. J. ACM 67(1): 6:1-6:66 (2020)- [c91]Brandon Bohrer, André Platzer:
Constructive Hybrid Games. IJCAR (1) 2020: 454-473 - [c90]Brandon Bohrer, André Platzer:
Constructive Game Logic. ESOP 2020: 84-111 - [c89]Brandon Bohrer, André Platzer:
Refining Constructive Hybrid Games. FSCD 2020: 14:1-14:19 - [p2]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) - [c88]Brandon Bohrer, Manuel Fernández, André Platzer:
dLι: Definite Descriptions in Differential Dynamic Logic. CADE 2019: 94-110 - [c87]Katherine Cordwell, André Platzer:
Towards Physical Hybrid Systems. CADE 2019: 216-232 - [c86]André Platzer:
Uniform Substitution at One Fell Swoop. CADE 2019: 425-441 - [c85]Viren Bajaj, Karim Elmaaroufi, Nathan Fulton, André Platzer:
Verifiably safe SCUBA diving using commodity sensors: work-in-progress. EMSOFT Companion 2019: 8 - [c84]Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer:
Pegasus: A Framework for Sound Continuous Invariant Generation. FM 2019: 138-157 - [c83]Yong Kiam Tan, André Platzer:
An Axiomatic Approach to Liveness for Differential Equations. FM 2019: 371-388 - [c82]Luis Garcia, Stefan Mitsch, André Platzer:
HyPLC: hybrid programmable logic controller program translation for verification. ICCPS 2019: 47-56 - [c81]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 - [c80]André Platzer:
The Logical Path to Autonomous Cyber-Physical Systems. QEST 2019: 25-33 - [c79]João G. Martins, André Platzer, João Leite:
Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems. TABLEAUX 2019: 428-445 - [c78]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) - [c77]Nathan Fulton, André Platzer:
Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning. AAAI 2018: 6485-6492 - [c76]Brandon Bohrer, Adriel Luo, Xue An Chuang, André Platzer:
CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation. ADHS 2018: 55-60 - [c75]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 - [c74]André Platzer:
Uniform Substitution for Differential Game Logic. IJCAR 2018: 211-227 - [c73]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 - [c72]Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer:
Vector Barrier Certificates and Comparison Systems. FM 2018: 418-437 - [c71]Nathan Fulton, André Platzer:
Safe AI for CPS (Invited Paper). ITC 2018: 1-7 - [c70]Brandon Bohrer, André Platzer:
A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow. LICS 2018: 115-124 - [c69]André Platzer, Yong Kiam Tan:
Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. LICS 2018: 819-828 - [c68]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 - [p1]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) - [c67]Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer:
Formally verified differential dynamic logic. CPP 2017: 208-221 - [c66]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 - [c65]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
Change and Delay Contracts for Hybrid System Component Verification. FASE 2017: 134-151 - [c64]Nathan Fulton, Stefan Mitsch, Brandon Bohrer, André Platzer:
Bellerophon: Tactical Theorem Proving for Hybrid Systems. ITP 2017: 207-224 - [c63]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) - [c62]André Platzer:
Logic & Proofs for Cyber-Physical Systems. IJCAR 2016: 15-21 - [c61]Nathan Fulton, André Platzer:
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. CPP 2016: 110-121 - [c60]Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer:
A Component-Based Approach to Hybrid Systems Safety Verification. IFM 2016: 441-456 - [c59]Sarah M. Loos, André Platzer:
Differential Refinement Logic. LICS 2016: 505-514 - [c58]André Platzer:
Keynote talk I: How to prove hybrid systems. MEMOCODE 2016: 1 - [c57]Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer:
A Method for Invariant Generation for Polynomial Continuous Systems. VMCAI 2016: 268-288 - [c56]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) - [c55]André Platzer:
Ernst-Rüdiger Olderog: A Life for Meaning. Correct System Design 2015: 5-9 - [c54]André Platzer:
A Uniform Substitution Calculus for Differential Dynamic Logic. CADE 2015: 467-481 - [c53]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 - [c52]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 - [c51]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 - [c50]André Platzer:
Proving Hybrid Systems. FMCAD 2015: 1 - [c49]Andreas Müller, Stefan Mitsch, André Platzer:
Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems. ITSC 2015: 757-764 - [c48]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 - [c47]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) - [c46]Jean-Baptiste Jeannin, André Platzer:
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. IJCAR 2014: 292-306 - [c45]Stefan Mitsch, Jan-David Quesel, André Platzer:
Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems. FM 2014: 481-496 - [c44]Stefan Mitsch, André Platzer:
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models. RV 2014: 199-214 - [c43]Khalil Ghorbal, Andrew Sogokon, André Platzer:
Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations. SAS 2014: 151-167 - [c42]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) - [c41]Sarah M. Loos, David W. Renshaw, André Platzer:
Formal verification of distributed aircraft controllers. HSCC 2013: 125-130 - [c40]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 - [c39]Erik Peter Zawadzki, André Platzer, Geoffrey J. Gordon:
A Generalization of SAT and #SAT for Robust Policy Evaluation. IJCAI 2013: 2583-2590 - [c38]Sarah M. Loos, David Witmer, Peter Steenkiste, André Platzer:
Efficiency analysis of formally verified adaptive cruise controllers. ITSC 2013: 1565-1570 - [c37]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) - [c36]Nikos Aréchiga, Sarah M. Loos, André Platzer, Bruce H. Krogh:
Using theorem provers to guarantee closed-loop system properties. ACC 2012: 3573-3580 - [c35]Jan-David Quesel, André Platzer:
Playing Hybrid Games with KeYmaera. IJCAR 2012: 439-453 - [c34]André Platzer:
Logical Analysis of Hybrid Systems - A Complete Answer to a Complexity Challenge. DCFS 2012: 43-49 - [c33]Stefan Mitsch, Sarah M. Loos, André Platzer:
Towards Formal Verification of Freeway Traffic Control. ICCPS 2012: 171-180 - [c32]André Platzer:
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). ITP 2012: 28-48 - [c31]André Platzer:
Logics of Dynamical Systems. LICS 2012: 13-24 - [c30]André Platzer:
The Complete Proof Theory of Hybrid Systems. LICS 2012: 541-550 - [c29]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]André Platzer:
The Structure of Differential Invariants and Differential Cut Elimination. Log. Methods Comput. Sci. 8(4) (2011) - [c28]André Platzer:
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs. CADE 2011: 446-460 - [c27]Sicun Gao, André Platzer, Edmund M. Clarke:
Quantifier Elimination over Finite Fields Using Gröbner Bases. CAI 2011: 140-157 - [c26]André Platzer:
Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial). CAV 2011: 28-43 - [c25]Akshay Rajhans, Ajinkya Bhave, Sarah M. Loos, Bruce H. Krogh, André Platzer, David Garlan:
Using parameters in architectural views to support heterogeneous design and verification. CDC-ECE 2011: 2705-2710 - [c24]Sarah M. Loos, André Platzer, Ligia Nistor:
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. FM 2011: 42-56 - [c23]André Platzer:
Quantified differential invariants. HSCC 2011: 63-72 - [c22]João G. Martins, André Platzer, João Leite:
Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications. ICFEM 2011: 131-146 - [c21]David W. Renshaw, Sarah M. Loos, André Platzer:
Distributed Theorem Proving for Distributed Hybrid Systems. ICFEM 2011: 356-371 - [c20]Sarah M. Loos, André Platzer:
Safe intersections: At the crossing of hybrid systems and verification. ITSC 2011: 1181-1186 - [c19]Erik Zawadzki, Geoffrey J. Gordon, André Platzer:
An Instantiation-Based Theorem Prover for First-Order Programming. AISTATS 2011: 855-863 - [i1]Sicun Gao, André Platzer, Edmund M. Clarke:
Quantifier Elimination over Finite Fields Using Gröbner Bases. CoRR abs/1104.0746 (2011) - 2010
- [b2]André Platzer:
Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer 2010, ISBN 978-3-642-14508-7, pp. I-XXX, 1-426 - [j7]André Platzer:
Differential Dynamic Logics. Künstliche Intell. 24(1): 75-77 (2010) - [j6]André Platzer:
Differential-algebraic Dynamic Logic for Differential-algebraic Programs. J. Log. Comput. 20(1): 309-352 (2010) - [c18]André Platzer:
Real Analysis for Complex Systems. VERIFY@IJCAR 2010: 3 - [c17]