Asst. Prof. André Platzer

email: Andre.Platzer André Platzer wrote his PhD thesis "Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems" in the Department of Computing Science at the University of Oldenburg. Since October 2008, André Platzer is a faculty member at Carnegie Mellon University.

 

Curriculum Vitae

10/2007	Visiting PhD student of Prof. Edmund M. Clarke at Carnegie Mellon University
04/2006-09/2006	Visiting PhD student of Prof. Edmund M. Clarke at Carnegie Mellon University
since 12/2005	PhD student at the DFG-Graduate School TrustSoft.
since 10/2004	Research Assistant in the Correct System Design Group
9/2004	Diploma degree in Informatics at the University of Karlsruhe (TH)

Projects

• AVACS (Automatic Verification and Analysis of Complex Systems)
• TrustSoft (Trustworthy Software Systems)

See the private home page for more information.

Tools

• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems
• AMC: Approximation Refinement Model Checker
• SAAtRe: SAT-based Abstraction Refinement for Real-time Systems
• Orbital library

Publications

[PQR09a]

André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. Reports of SFB/TR 14 AVACS 52, SFB/TR 14 AVACS, June 2009. ISSN: 1860-9821, http://www.avacs.org. [ bib | .pdf | Abstract ]

[PQR09b]

André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. In Renate A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[PQ09a]

André Platzer and Jan-David Quesel. European train control system: A case study in formal verification. In Ana Cavalcanti and Karin Breitman, editors, Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 9-12, 2009, Proceedings, volume 5885 of LNCS, pages 246-265, Heidelberg, 2009. Springer. (c) Springer-Verlag. [ bib | .pdf | Abstract ]

[PQ09b]

André Platzer and Jan-David Quesel. European train control system: A case study in formal verification. Reports of SFB/TR 14 AVACS 54, SFB/TR 14 AVACS, Oct 2009. ISSN: 1860-9821, http://www.avacs.org. [ bib | .pdf | Abstract ]

[Pla08a]

André Platzer. Differential-algebraic dynamic logic for differential-algebraic programs. Journal of Logic and Computation, 2008. Accepted for publication. [ bib | DOI | .pdf | Abstract ]

[Pla08b]

André Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2):143-189, 2008. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[PQ08a]

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, Third International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[PC08a]

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. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[PQ08b]

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, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pages 646-649. Springer, 2008. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[PC08b]

André Platzer and Edmund M. Clarke. Computing differential invariants of hybrid systems as fixedpoints. Technical Report CMU-CS-08-103, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 2008. [ bib | .pdf | Abstract ]

[Pla07a]

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, volume 259, pages 164-178. CEUR-WS.org, 2007. CEUR Workshop Proceedings. [ bib | .pdf | Abstract ]

[DMO⁺07]

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-Verlag, 2007. (c) Springer-Verlag. [ bib | DOI | Abstract ]

[Pla07b]

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-Verlag, 2007. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[Pla07d]

André Platzer. A temporal dynamic logic for verifying hybrid system invariants. Reports of SFB/TR 14 AVACS 12, February 2007. ISSN: 1860-9821, http://www.avacs.org. [ bib | .pdf ]

[Pla07e]

André Platzer. A temporal dynamic logic for verifying hybrid system invariants. In S. Artemov and A. Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pages 457-471. Springer, 2007. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[Pla07c]

André Platzer. Differential logic for reasoning about hybrid systems. In A. Bemporad, A. Bicchi, and G. Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 746-749. Springer-Verlag, 2007. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[PC07]

André Platzer and Edmund M. Clarke. The image computation problem in hybrid systems model checking. In A. Bemporad, A. Bicchi, and G. Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 473-486. Springer-Verlag, 2007. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[KP07]

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, volume 182 of ENTCS, pages 107-122, 2007. [ bib | DOI | .pdf | Abstract ]

[Pla07f]

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., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, volume 174 of ENTCS, pages 63-77, Jun 2007. [ bib | DOI | .pdf | Abstract ]

[BP06]

Bernhard Beckert and André Platzer. Dynamic logic with non-rigid functions: A basis for object-oriented program verification. In U. Furbach and N. 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-Verlag, 2006. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

Theses

[Pla08]

André Platzer. Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems. PhD thesis, Department of Computing Science, University of Oldenburg, 2008.
[ bib ]

[Pla04a]

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.
[ bib | .pdf | Abstract ]

[Pla04b]

André Platzer. Using a program verification calculus for constructing specifications from implementations. Minor Thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, February 2004.
[ bib | .pdf | Abstract ]