reports.bib

@techreport{DBLP:conf/cade/QueselP12:TR,
  author = {Jan-David Quesel and Andr{\'e} Platzer},
  title = {Playing Hybrid Games with {KeYmaera}.},
  editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and
                    Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard
                    Wilhelm},
  institution = {SFB/TR 14 AVACS},
  subproject = {H3},
  year = {2012},
  month = {April},
  type = {Reports of SFB/TR 14 AVACS},
  series = {ATR},
  number = 84,
  note = {ISSN: 1860-9821, http://www.avacs.org.},
  abstract = {
  We propose a new logic, called differential dynamic game logic (dDGL), for expressing properties of parametric hybrid games, and develop a theorem prover for it. 
  We give an operational and a modal semantics of dDGL and prove their equivalence.
  To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic(dL). We provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. 
  We have implemented dDGL in the theorem prover KeYmaera and consider a case study in which a robot plays a game against other agents in a factory automation scenario.
      },
  access = {open},
  bibtex = {atr084.bib},
  pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_084.pdf}
}

@techreport{DBLP:conf/cade/PlatzerQR09:TR,
  author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer},
  title = {Real World Verification},
  editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and
                    Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard
                    Wilhelm},
  institution = {SFB/TR 14 AVACS},
  subproject = {H3},
  year = {2009},
  month = {June},
  type = {Reports of SFB/TR 14 AVACS},
  series = {ATR},
  number = 52,
  note = {ISSN: 1860-9821, http://www.avacs.org.},
  access = {open},
  abstract = {Scalable handling of real arithmetic is a crucial part of
			the verification of hybrid systems, mathematical algorithms, and mixed
			analog/digital circuits.  Despite substantial advances in
			verification technology, complexity issues with classical decision
			procedures are still a major obstacle for formal verification of
			real-world applications, e.g., in automotive and avionic
			industries.  To identify strengths and weaknesses, we examine state
			of the art symbolic techniques and implementations for the
			universal fragment of real-closed fields: approaches based on
			quantifier elimination, Gr{\"o}bner Bases, and semidefinite
			programming for the Positivstellensatz.  Within a uniform context
			of the verification tool KeYmaera, we compare these approaches
			qualitatively and quantitatively on verification benchmarks from
			hybrid systems, textbook algorithms, and on geometric problems.
			Finally, we introduce a new decision procedure combining
			Gr{\"o}bner Bases and semidefinite programming for the real
			Nullstellensatz that outperforms the individual approaches on an
			interesting set of problems.},
  bibtex = {atr052.bib},
  pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_052.pdf}
}

@techreport{conf/icfem/PlatzerQ09:TR,
  author = {Andr{\'e} Platzer and Jan-David Quesel},
  title = {European Train Control System: A Case Study in Formal Verification},
  editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and
                    Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard
                    Wilhelm},
  institution = {SFB/TR 14 AVACS},
  subproject = {H3},
  year = {2009},
  month = {Oct},
  type = {Reports of SFB/TR 14 AVACS},
  series = {ATR},
  number = 54,
  note = {ISSN: 1860-9821, http://www.avacs.org.},
  access = {open},
  abstract = {Complex physical systems have several degrees of freedom.
	They only work correctly when their control parameters obey
	corresponding constraints.  Based on the informal specification of
	the European Train Control System (ETCS), we design a controller
	for its cooperation protocol.  For its free parameters, we
	successively identify constraints that are required to ensure
	collision freedom. We formally prove the parameter
	constraints to be sharp by characterizing them equivalently
	in terms of reachability properties of the hybrid system
	dynamics.  Using our deductive verification tool KeYmaera,
	we formally verify controllability, safety, liveness, and
	reactivity properties of the ETCS protocol that entail
	collision freedom.  We prove that the ETCS protocol
	remains correct even in the presence of perturbation by
	disturbances in the dynamics.  Finally we verify that
	safety is preserved when a PI controller is used for
	speed supervision.},
  bibtex = {atr054.bib},
  pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_054.pdf}
}