Jan-David Quesel

 

1 Publications (BibTeX Source)

@INPROCEEDINGS{DBLP:conf/cade/PlatzerQ08,
  AUTHOR = {Andr{\'e} Platzer and
               Jan-David Quesel},
  TITLE = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.},
  BOOKTITLE = {Automated Reasoning, Third International Joint Conference,
               IJCAR 2008, Sydney, Australia, Proceedings},
  YEAR = {2008},
  PAGES = {171-178},
  EDITOR = {Alessandro Armando and
               Peter Baumgartner and
               Gilles Dowek},
  PUBLISHER = {Springer},
  SERIES = {LNCS},
  VOLUME = {5195},
  ISBN = {10.1007/978-3-540-71070-7_15},
  ISSN = {0302-9743},
  KEYWORDS = {dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems},
  ABSTRACT = {
      KeYmaera is a hybrid verification tool for hybrid systems that
      combines deductive, real algebraic, and computer algebraic
      prover technologies.  It is an automated and interactive theorem
      prover for a natural specification and verification logic for
      hybrid systems.  KeYmaera supports differential dynamic logic,
      which is a real-valued first-order dynamic logic for hybrid
      programs, a program notation for hybrid automata.  For
      automating the verification process, KeYmaera implements a
      generalized free-variable sequent calculus and automatic proof
      strategies that decompose the hybrid system specification
      symbolically.  To overcome the complexity of real arithmetic, we
      integrate real quantifier elimination following an iterative
      background closure strategy.  Our tool is particularly suitable
      for verifying parametric hybrid systems and has been used
      successfully for verifying collision avoidance in case studies
      from train control and air traffic management.},
  NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-71070-7_15}{(c)
Springer-Verlag}},
  URL = {http://www.functologic.com/pub/KeYmaera.pdf}
}


@INPROCEEDINGS{DBLP:conf/hybrid/PlatzerQ08,
  AUTHOR = {Andr{\'e} Platzer and
               Jan-David Quesel},
  TITLE = {Logical Verification and Systematic Parametric Analysis in
Train Control.},
  YEAR = {2008},
  PAGES = {646-649},
  DOI = {10.1007/978-3-540-78929-1_55},
  EDITOR = {Magnus Egerstedt and
               Bud Mishra},
  BOOKTITLE = {Hybrid Systems: Computation and Control, 10th International
               Conference, HSCC 2008, St. Louis, USA, Proceedings},
  PUBLISHER = {Springer},
  SERIES = {LNCS},
  VOLUME = {4981},
  ISBN = {},
  KEYWORDS = {parametric verification, logic for hybrid systems, symbolic
decomposition},
  ABSTRACT = {
      We formally verify hybrid safety properties of cooperation
      protocols in a fully parametric version of the European Train
      Control System (ETCS). We present a formal model using hybrid
      programs and verify correctness using our logic-based
      decomposition procedure. This procedure supports free parameters
      and parameter discovery, which is required to determine correct
      design choices for free parameters of ETCS.},
  URL = {http://www.functologic.com/pub/ETCS-short.pdf},
  NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-78929-1_55}{(c)
Springer-Verlag}}
}


@INPROCEEDINGS{QS06,
  AUTHOR = {J.-D. Quesel and A. Sch\"afer},
  TITLE = {Spatio-Temporal Model Checking for Mobile Real-Time  Systems},
  BOOKTITLE = {3rd International Colloquium on Theoretical Aspects 
               of Computing, ICTAC},
  YEAR = {2006},
  EDITOR = {K. Barkaoui and A. Cavalcanti and A. Cerone},
  SERIES = {LNCS},
  PAGES = {347--361},
  ABSTRACT = {
    This paper presents an automatic verification method for combined
    temporal and spatial properties of mobile real-time systems. To
    this end, we provide a translation of the Shape Calculus (SC), a
    spatio-temporal extension of Duration Calculus, into weak second
    order logic of one successor (WS1S).  A prototypical
    implementation facilitates successful verification of
    spatio-temporal properties by translating SC specifications into
    the syntax of the WS1S checker MONA.  For demonstrating the
    formalism and tool usage, we apply it to the benchmark case study
    ``generalised railroad crossing'' (GRC) enriched by requirements
    inexpressible in non-spatial formalisms.
  }
}