Correct System Design

Jan-David Quesel

Address: Jan-David Quesel
University of Oldenburg
Faculty II
Department of Computing Science
D-26111 Oldenburg
Germany
Foto
Room: A3 2-212
Phone: +49 441 798-2376
Fax: +49 441 798-2965
email: Jan-David.Quesel

 


top of page

Curriculum Vitae

since 6/2007 Research Assistant in the Correct System Design Group
4/2007 Diploma degree in Computer Science at the University of Oldenburg


top of page

Research

My research interests are
  • Verifikation of hybrid systems
  • Semantics for hybrid systems
  • Parametric verification
  • Theorem proving
  • real-time systems
  • Model checking

top of page

Tools


top of page

Publications

[QFD11]
J.-D. Quesel, M. Fränzle, and W. Damm. Crossing the bridge between similar games. In Stavros Tripakis and Uli Fahrenberg, editors, Formal Modeling and Analysis of Timed Systems - 9th International Conference (FORMATS), Aalborg, Denmark, 21-23 September, 2011. Proceedings, volume 6919 of LNCS, pages 160-176. Springer, Sep. 2011. The original publication is available at www.springerlink.com.
[ bib | slides | .pdf | Abstract ]

[FLOQ11]
Johannes Faber, Sven Linker, Ernst-Rüdiger Olderog, and Jan-David Quesel. Syspect - modelling, specifying, and verifying real-time systems with rich data. International Journal of Software and Informatics, 5(1-2):117-137, 2011. ISSN 1673-7288.
[ bib | http | Abstract ]

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

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

[QS06]
J.-D. Quesel and A. Schäfer. Spatio-temporal model checking for mobile real-time systems. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, LNCS, pages 347-361, 2006.
[ bib | Abstract ]


top of page

Theses

[JDQ07]
Jan-David Quesel. A Theorem Prover for Differential Dynamic Logic: Deductive Verification of Hybrid Systems, 2007.
[ bib | .pdf ]

[JDQ05]
Jan-David Quesel. MoDiShCa - Model Checking Discrete Shape Calculus, 2005.
[ bib | .pdf ]