Dipl.-Inform. André Platzer

E-Mail: Andre.Platzer

 

Curriculum Vitae

10/2007	Forschungsaufenthalt bei Prof. Edmund M. Clarke an der Carnegie Mellon University
04/2006-09/2006	Forschungsaufenthalt bei Prof. Edmund M. Clarke an der Carnegie Mellon University
seit 12/2005	Kollegiat im DFG-Graduiertenkolleg TrustSoft.
seit 10/2004	Wissenschaftlicher Mitarbeiter in der Abteilung Entwicklung korrekter Systeme
9/2004	Informatik-Diplom an der Universität Karlsruhe (TH)

Projekte

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

Auf der privaten Homepage finden Sie weitere Details.

Werkzeuge

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

Publikationen

[Pla08a]

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

[Pla08b]

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

Abschlussarbeiten

[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 ]