Publications by André Platzer (by year)

Table of Contents
  1. List of Publications
    1. Books
    2. Journal Publications
    3. Conference Publications
    4. Short & Tool Publications
    5. Workshop Publications
    6. Invited Papers
    7. Reports
    8. Lecture Notes
    9. Drafts
    10. Theses
Logical Analysis of Hybrid Systems

List of Publications

[DBLP | Google Scholar | ORCID | by year | by area | abstracts | guide]

Also see publications by area and publication reading guide.

Books

  1. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 p. ISBN 978-3-642-14508-7.
    [bib | book | eBook | doi | web]

Logical Analysis of Hybrid Systems

Journal Publications

  1. Khalil Ghorbal, Jean-Baptiste Jeannin, Erik W. Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell.
    Hybrid theorem proving of aerospace systems: Applications and challenges.
    Journal of Aerospace Information Systems, 11, pages 702-713. 2014. © The authors
    [bib | pdf | doi | abstract]

  2. Akshay Rajhans, Ajinkya Bhave, Ivan Ruchkin, Bruce H. Krogh, David Garlan, André Platzer and Bradley Schmerl.
    Supporting heterogeneity in cyber-physical systems architectures.
    IEEE Transactions on Automatic Control. 59(12), pages 3178-3193, 2014.
    Special issue on Control of Cyber-Physical Systems. © IEEE
    [bib | doi | abstract]

  3. Stefan Mitsch, Grant Olney Passmore and André Platzer.
    Collaborative verification-driven engineering of hybrid systems.
    Mathematics in Computer Science, 8(1), pages 71-97, 2014. © Springer-Verlag
    [bib | pdf | doi | arXiv | abstract]

  4. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian statistical model checking with application to Simulink/Stateflow verification.
    Formal Methods in System Design, 43(2), pages 338-367, 2013. © Springer-Verlag
    [bib | pdf | doi | abstract]

  5. André Platzer.
    A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
    Logical Methods in Computer Science, 8(4), pages 1-44, 2012.
    Special issue for selected papers from CSL'10.
    [bib | pdf | doi | eprint | arXiv | CSL'10 | abstract]

  6. André Platzer.
    The structure of differential invariants and differential cut elimination.
    Logical Methods in Computer Science, 8(4), pages 1-38, 2012.
    [bib | pdf | doi | eprint | arXiv | abstract]

  7. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    Formal Methods in System Design, 35(1), pages 98-120, 2009. © Springer-Verlag
    Special issue for selected papers from CAV'08.
    [bib | pdf | doi | study | CAV'08 | abstract]

  8. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation, 20(1), pages 309-352, 2010. © The author Advance Access published on November 18, 2008 by Oxford University Press.
    [bib | pdf | doi | study | abstract]

  9. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning, 41(2), pages 143-189, 2008. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

Conference Publications

  1. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    A hierarchy of proof rules for checking differential invariance of algebraic sets.
    In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015, Proceedings, volume 8931 of LNCS, pages 419-436. Springer, 2015. © Springer-Verlag
    [bib | pdf | abstract]

  2. Stefan Mitsch and André Platzer.
    ModelPlex: Verified runtime validation of verified cyber-physical system models.
    In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of LNCS, pages 199-214. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  3. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    Invariance of conjunctions of polynomial equalities for algebraic differential equations.
    In Markus Müller-Olm and Helmut Seidl, editors, 21st International Static Analysis Symposium, volume 8723 of LNCS, pages 151-167. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | abstract]

  4. Jean-Baptiste Jeannin and André Platzer.
    dTL2: Differential temporal dynamic logic with nested temporalities for hybrid systems.
    In Stéphane Demri, Deepak Kapur and Christoph Weidenbach, editors, Automated Reasoning, 7th International Joint Conference, IJCAR 2014, Vienna, Austria, July 19-22, 2014, Proceedings, volume 8562 of LNCS, pages 292-306. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | slides | abstract]

  5. Stefan Mitsch, Jan-David Quesel and André Platzer.
    Refactoring, refinement, and reasoning: A logical characterization for hybrid systems.
    In Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, editors, 19th International Symposium on Formal Methods, FM, Singapore, Proceedings, volume 8442 of LNCS, pages 481-496. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | slides | abstract]

  6. Khalil Ghorbal and André Platzer.
    Characterizing algebraic invariants by differential radical invariants.
    In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Proceedings, volume 8413 of LNCS, pages 279-294. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | slides | TR | abstract]

  7. Sarah M. Loos, David Witmer, Peter Steenkiste and André Platzer.
    Efficiency analysis of formally verified adaptive cruise controllers.
    In Andreas Hegyi and Bart De Schutter, editors, 16th International IEEE Conference on Intelligent Transportation Systems, ITSC'13, The Hague, Netherlands, Proceedings, 2013. © IEEE
    [bib | pdf | doi | slides | study | abstract]

  8. Stefan Mitsch, Khalil Ghorbal and André Platzer.
    On provably safe obstacle avoidance for autonomous robotic ground vehicles.
    In Paul Newman, Dieter Fox, and David Hsu, editors, Robotics: Science and Systems, 2013.
    [bib | pdf | slides | study | eprint | talk | abstract]

  9. Erik P. Zawadzki, André Platzer and Geoffrey J. Gordon.
    A generalization of SAT and #SAT for policy evaluation.
    In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23nd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 2583-2589, IJCAI/AAAI, 2013.
    [bib | pdf | poster | eprint | TR | abstract]

  10. Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
    Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
    In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pages 263-272. ACM, 2013. © ACM
    [bib | pdf | doi | study | abstract]

  11. Sarah M. Loos, David W. Renshaw and André Platzer.
    Formal verification of distributed aircraft controllers.
    In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pages 125-130. ACM, 2013. © ACM
    [bib | pdf | doi | slides | poster | study | TR | abstract]

  12. David Henriques, João G. Martins, Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Statistical model checking for Markov decision processes.
    In 9th International Conference on Quantitative Evaluation of Systems, QEST 2012, September 17-20, London, UK, pages 84-93. IEEE Computer Society, 2012. © IEEE
    [bib | pdf | doi | slides | study | abstract]

  13. André Platzer.
    A differential operator approach to equational differential invariants.
    In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pages 28-48. Springer, 2012. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | slides | abstract]

  14. Jan-David Quesel and André Platzer.
    Playing hybrid games with KeYmaera.
    In Bernhard Gramlich, Dale Miller and Ulrike Sattler, editors, Automated Reasoning, 6th International Joint Conference, IJCAR'12, Manchester, UK, Proceedings, volume 7364 of LNCS, pages 439-453. Springer, 2012. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

  15. André Platzer.
    Logics of dynamical systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012. © IEEE
    Invited paper.
    [bib | pdf | doi | slides | abstract]

  16. André Platzer.
    The complete proof theory of hybrid systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541-550. IEEE 2012. © IEEE
    [bib | pdf | doi | slides | TR | abstract]

  17. Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
    Using theorem provers to guarantee closed-loop system properties.
    In Dawn Tilbury, editor, American Control Conference, ACC, Montréal, Canada, June 27-29. pages 3573-3580. 2012. © IEEE
    [bib | pdf | eprint | abstract]

  18. Stefan Mitsch, Sarah M. Loos and André Platzer.
    Towards formal verification of freeway traffic control.
    In Chenyang Lu, editor, ACM/IEEE Third International Conference on Cyber-Physical Systems, Beijing, China, April 17-19. pages 171-180, IEEE. 2012. © IEEE
    [bib | pdf | doi | slides | study | abstract]

  19. Akshay Rajhans, Ajinkya Bhave, Sarah M. Loos, Bruce H. Krogh, André Platzer and David Garlan.
    Using parameters in architectural views to support heterogeneous design and verification.
    In 50th IEEE Conference on Decision and Control and European Control Conference. pages 2705-2710, IEEE. 2011. © IEEE
    [bib | pdf | doi | abstract]

  20. Sarah M. Loos and André Platzer.
    Safe intersections: At the crossing of hybrid systems and verification.
    In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pages 1181-1186. 2011. © IEEE
    [bib | pdf | doi | slides | study | abstract]

  21. João G. Martins, André Platzer and João Leite.
    Statistical model checking for distributed probabilistic control hybrid automata with smart grid applications.
    In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pages 131-146. Springer, 2011. © Springer-Verlag
    [bib | pdf | doi | slides | study | abstract]

  22. David W. Renshaw, Sarah M. Loos and André Platzer.
    Distributed theorem proving for distributed hybrid systems.
    In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pages 356-371. Springer, 2011. © Springer-Verlag Errata fixed in author's version
    [bib | pdf | tool | study | abstract]

  23. André Platzer.
    Logic and compositional verification of hybrid systems.
    In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, CAV 2011, Snowbird, UT, USA, Proceedings, volume 6806 of LNCS, pages 28-43. Springer, 2011. © Springer-Verlag
    Invited tutorial.
    [bib | pdf | doi | slides | abstract]

  24. André Platzer.
    Stochastic differential dynamic logic for stochastic hybrid programs.
    In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, International Conference on Automated Deduction, CADE'11, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pages 431-445. Springer, 2011. © Springer-Verlag
    [bib | pdf | doi | slides | TR | abstract]

  25. Sicun Gao, André Platzer and Edmund M. Clarke.
    Quantifier elimination over finite fields with Gröbner bases.
    In Franz Winkler, editor, Algebraic Informatics, Fourth International Conference, CAI 2011, Linz, Austria, June 21-24, 2011, Proceedings, volume 6742 of LNCS, pages 140-157. Springer, 2011. © Springer-Verlag
    [bib | pdf | doi | arXiv | abstract]

  26. Sarah M. Loos, André Platzer and Ligia Nistor.
    Adaptive cruise control: Hybrid, distributed, and now formally verified.
    In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pages 42-56. Springer, 2011. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  27. Erik P. Zawadzki, Geoffrey J. Gordon and André Platzer.
    An Instantiation-Based Theorem Prover for First-Order Programming.
    In 14th International Conference on Artificial Intelligence and Statistics (AISTATS) 2011, Fort Lauderdale, FL, USA, Proceedings, volume 15 of JMLR W&CP, pages 855-863, 2011.
    [bib | pdf | proceedings | abstract]

  28. André Platzer.
    Quantified differential invariants.
    In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, Pages 63-72. ACM, 2011. © ACM
    [bib | pdf | doi | slides | abstract]

  29. André Platzer.
    Quantified differential dynamic logic for distributed hybrid systems.
    In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of LNCS, pages 469-483. Springer, 2010. © Springer-Verlag
    [bib | pdf | doi | slides | TR | LMCS'12 | abstract]

  30. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian statistical model checking with application to Simulink/Stateflow verification.
    In Karl Henrik Johansson and Wang Yi, editors, Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, pages 243-252. ACM, 2010. © ACM
    [bib | pdf | doi | TR | abstract]

  31. André Platzer and Jan-David Quesel.
    European Train Control System: A case study in formal verification.
    In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  32. André Platzer and Edmund M. Clarke.
    Formal verification of curved flight collision avoidance maneuvers: A case study.
    In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pages 547-562. Springer, 2009. © Springer-Verlag
    This paper was awarded the FM Best Paper Award.
    [bib | pdf | doi | slides | study | TR | abstract]

  33. Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
    A Bayesian approach to model checking biological systems.
    In Pierpaolo Degano and Roberto Gorrieri, editors, Computational Methods in Systems Biology, 7th International Conference, CMSB 2009, Bologna, Italy, Proceedings, volume 5688 of LNCS, pages 218-234. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | TR | abstract]

  34. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real world verification.
    In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE'09, Montreal, Canada, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | slides | TR | smtlib | abstract]
    Introduces a decision procedure for universal nonlinear real arithmetic combining Gröbner bases and semidefinite programming for the Real Nullstellensatz. An extended set of real arithmetic benchmarks from KeYmaera is available in smtlib, including the examples from CADE'09 paper and from some other KeYmaera-related papers.

  35. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pages 176-189, Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | FMSD'09 | abstract]

  36. Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken and Boris Wirtz.
    Automating verification of cooperation, control, and design in traffic applications.
    In Cliff Jones, Zhiming Liu and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 115-169. Springer, 2007. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | abstract]

  37. André Platzer.
    Differential dynamic logic for verifying parametric hybrid systems.
    In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pages 216-232. Springer, 2007. © Springer-Verlag
    This paper was awarded the TABLEAUX Best Paper Award.
    [bib | pdf | doi | slides | study | TR | abstract]

  38. André Platzer.
    A temporal dynamic logic for verifying hybrid system invariants.
    In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pages 457-471. Springer, 2007. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  39. André Platzer and Edmund M. Clarke.
    The image computation problem in hybrid systems model checking.
    In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 473-486. Springer, 2007, © Springer-Verlag
    [bib | pdf | doi | slides | tool | abstract]

  40. Bernhard Beckert and André Platzer.
    Dynamic logic with non-rigid functions: A basis for object-oriented program verification.
    In Uli Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of LNCS, pages 266-280. Springer, 2006. © Springer-Verlag
    [bib | doi | slides | abstract]

Short & Tool Publications

  1. André Platzer and Jan-David Quesel.
    KeYmaera: A hybrid theorem prover for hybrid systems.
    In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | slides | tool | abstract]

  2. André Platzer and Jan-David Quesel.
    Logical verification and systematic parametric analysis in train control.
    In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pages 646-649. Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | poster | abstract]

  3. André Platzer.
    Differential logic for reasoning about hybrid systems.
    In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 746-749. Springer, 2007. © Springer-Verlag
    [bib | pdf | doi | poster | abstract]

Workshop Publications

  1. Stefan Mitsch, Jan-David Quesel, and André Platzer.
    From safety to guilty & from liveness to niceness.
    In Calin Belta and Hadas Kress-Gazit, editors, 5th Workshop on Formal Methods for Robotics and Automation, 2014.
    [bib | pdf | abstract]

  2. Erik P. Zawadzki, Geoffrey J. Gordon and André Platzer .
    A projection algorithm for strictly monotone linear complementarity problems.
    In 6th NIPS Workshop on Optimization for Machine Learning, 2013.
    [bib | pdf | eprint | abstract]

  3. André Platzer.
    Teaching CPS foundations with contracts.
    First Workshop on Cyber-Physical Systems Education, pages 7-10. 2013.
    [bib | pdf | slides | poster | eprint | course | abstract]

  4. André Platzer.
    Combining deduction and algebraic constraints for hybrid system analysis.
    In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
    [bib | pdf | slides | eprint | abstract]

  5. Stephanie Kemper and André Platzer.
    SAT-based abstraction refinement for real-time systems.
    In Frank S. de Boer and Vladimir Mencl, editors, Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, Electr. Notes Theor. Comput. Sci., 182:107-122, 2007
    [bib | pdf | doi | slides | tool | abstract]

  6. André Platzer.
    Towards a hybrid dynamic logic for hybrid dynamic systems.
    In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva and Jørgen Villadsen, editors, Proc., International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, Electr. Notes Theor. Comput. Sci. 174(6):63-77, 2007.
    [bib | pdf | doi | slides | abstract]

Invited Papers

  1. André Platzer.
    Analog and hybrid computation: Dynamical systems and programming languages.
    Bulletin of the EATCS, 114, 2014.
    Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
    [bib | pdf | eprint | abstract]

  2. André Platzer.
    Logical analysis of hybrid systems: A complete answer to a complexity challenge.
    Journal of Automata, Languages and Combinatorics, 17(2-4), pages 265-275. 2012.
    Invited Paper
    [bib | pdf | abstract]

  3. André Platzer.
    Logical analysis of hybrid systems: A complete answer to a complexity challenge.
    In Martin Kutrib, Nelma Moreira and Rogério Reis, editors, Descriptional Complexity of Formal Systems, DCFS'12, Braga, Portugal, Proceedings, volume 7386 of LNCS, pages 43-49. Springer, 2012.
    Invited Paper © Springer-Verlag
    [bib | pdf | doi | abstract]

  4. André Platzer.
    A differential operator approach to equational differential invariants.
    In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pages 28-48. Springer, 2012. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | slides | abstract]

  5. André Platzer.
    Logics of dynamical systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012. © IEEE
    Invited paper.
    [bib | pdf | doi | slides | abstract]

  6. Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
    Using theorem provers to guarantee closed-loop system properties.
    In Dawn Tilbury, editor, American Control Conference, ACC, Montréal, Canada, June 27-29. pages 3573-3580. 2012. © IEEE
    [bib | pdf | eprint | abstract]

  7. Sarah M. Loos and André Platzer.
    Safe intersections: At the crossing of hybrid systems and verification.
    In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pages 1181-1186. 2011. © IEEE
    [bib | pdf | doi | slides | study | abstract]

  8. André Platzer.
    Logic and compositional verification of hybrid systems.
    In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, CAV 2011, Snowbird, UT, USA, Proceedings, volume 6806 of LNCS, pages 28-43. Springer, 2011. © Springer-Verlag
    Invited tutorial.
    [bib | pdf | doi | slides | abstract]

  9. André Platzer.
    Differential dynamic logic: Automated theorem proving for hybrid systems.
    Künstliche Intelligenz, 24(1), pages 75-77, 2010. © Springer-Verlag
    Invited paper.
    [bib | doi | abstract]

  10. André Platzer.
    Verification of cyberphysical transportation systems.
    IEEE Intelligent Systems, 24(4), pages 10-13, Jul/Aug, 2009. © IEEE.
    Invited paper.
    [bib | doi | abstract]

  11. Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken and Boris Wirtz.
    Automating verification of cooperation, control, and design in traffic applications.
    In Cliff Jones, Zhiming Liu and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 115-169. Springer, 2007. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | abstract]

Reports

  1. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Garnder, Aurora Schmidt, Erik Zawadzki, and André Platzer.
    A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System.
    School of Computer Science, Carnegie Mellon University, CMU-CS-14-138, 2014.
    [bib | pdf | study | abstract]

  2. Stefan Mitsch and André Platzer.
    ModelPlex: Verified Runtime Validation of Verified Cyber-physical System Models.
    School of Computer Science, Carnegie Mellon University, CMU-CS-14-121, 2014.
    [bib | pdf | study | RV'14 | abstract]

  3. Khalil Ghorbal and André Platzer.
    Characterizing Algebraic Invariants by Differential Radical Invariants.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-129, 2013.
    [bib | pdf | TACAS'14 | abstract]

  4. Erik Zawadzki, André Platzer, and Geoffrey J. Gordon.
    A Generalization of SAT and #SAT for Robust Policy Evaluation.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-107, 2013.
    [bib | pdf | IJCAI'13 | abstract]

  5. Yanni Kouskoulas, André Platzer and Peter Kazanzides.
    Formal Methods for Robotic System Control Software.
    Johns Hopkins APL Technical Digest 32(2), pages 490-498, 2013.
    [bib | pdf | abstract]

  6. André Platzer.
    A Complete Axiomatization of Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-100R, January 2013, extended in revised version from July 2013. Extended version arXiv 1408.1980.
    [bib | pdf | slides | arXiv | abstract]

  7. David Renshaw, Sarah M. Loos and André Platzer.
    Mechanized Safety Proofs for Disc-Constrained Aircraft.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-132, August 2012.
    [bib | pdf | HSCC'13 | abstract]

  8. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv 1205.4788, May 2012.
    [bib | pdf | arXiv | abstract]

  9. André Platzer.
    Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-105, March 2012.
    Also see new results.
    [bib | pdf | abstract]

  10. André Platzer.
    The Complete Proof Theory of Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-144, November 2011.
    [bib | pdf | LICS'12]

  11. David W. Renshaw and André Platzer.
    Differential Invariants and Symbolic Integration for Distributed Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-107, May 2012.
    [bib | pdf]

  12. André Platzer.
    The Structure of Differential Invariants and Differential Cut Elimination.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-112, April 2011.
    [bib | pdf | arXiv | LMCS]

  13. André Platzer.
    Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-111, 2011.
    [bib | pdf | CADE'11]

  14. Sarah M. Loos, André Platzer and Ligia Nistor.
    Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-107, 2011.
    [bib | pdf | FM'10]

  15. André Platzer.
    Quantified differential dynamic logic for distributed hybrid systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-10-126, 2010.
    [bib | pdf | CSL'10]

  16. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian Statistical Model Checking with Application to Simulink/Stateflow Verification.
    School of Computer Science, Carnegie Mellon University, CMU-CS-10-100, 2010.
    [bib | pdf | HSCC'10]

  17. André Platzer and Jan-David Quesel.
    European Train Control System: A Case Study in Formal Verification.
    Reports of SFB/TR 14 AVACS 54, 2009. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | ICFEM'09]

  18. André Platzer and Edmund M. Clarke.
    Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
    School of Computer Science, Carnegie Mellon University, CMU-CS-09-147, 2009.
    [bib | pdf | FM'09]

  19. Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
    A Bayesian Approach to Model Checking Biological Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-09-110, 2009.
    [bib | pdf | CMSB'09]

  20. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real World Verification.
    Reports of SFB/TR 14 AVACS 52, 2009. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | CADE'09]

  21. André Platzer and Edmund M. Clarke.
    Computing Differential Invariants of Hybrid Systems as Fixedpoints.
    School of Computer Science, Carnegie Mellon University, CMU-CS-08-103, Feb, 2008.
    [bib | pdf | CAV'08]

  22. André Platzer.
    Differential Dynamic Logic for Verifying Parametric Hybrid Systems.
    Reports of SFB/TR 14 AVACS 15, May 2007. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | TABLEAUX'07]

  23. André Platzer.
    A Temporal Dynamic Logic for Verifying Hybrid System Invariants.
    Reports of SFB/TR 14 AVACS 12, February 2007. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | LFCS'07]

Lecture Notes

  1. André Platzer.
    Foundations of Cyber-Physical Systems.
    Lecture Notes, Computer Science Department, Carnegie Mellon University. 2013.
    [bib | pdf | course | abstract]

  1. Compiler Design
  2. Modal Logic

Drafts

  1. Sarah M. Loos and André Platzer.
    Teaching Cyber-Physical Systems with Logic.
    Draft, 2014.
    [bib | pdf | course | abstract]

  2. André Platzer.
    A Complete Axiomatization of Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-100R, January 2013, extended in revised version from July 2013. Extended version arXiv 1408.1980.
    [bib | pdf | slides | arXiv | abstract]

  3. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv 1205.4788, May 2012.
    [bib | pdf | arXiv | abstract]

Theses

  1. André Platzer.
    Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems.
    PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
    ACM Doctoral Dissertation Honorable Mention Award in 2009.
    Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
    [bib | pdf | eprint | book | doi | web | abstract | slides]

  2. André Platzer.
    An Object-oriented Dynamic Logic with Updates.
    Master's Thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, September 2004.
    Short version appeared as Dynamic logic with non-rigid functions: A basis for object-oriented program verification at IJCAR 2006.
    [bib | pdf | slides | abstract]

  3. André Platzer.
    Using a Program Verification Calculus for Constructing Specifications from Implementations.
    Minor Thesis (Studienarbeit), University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, February 2004.
    [bib | pdf | slides | abstract]

Copyright of publications is with the publisher as indicated. Author's versions of papers are posted with permission of the publisher for your personal use. Not for redistribution or commercial purpose. Slides are copyright © by the author.