Isabelle/DC: Proof Assistant for Duration Calculus
Isabelle/DC is a proof assistant for the real-time logic Duration Calculus.
Isabelle/DC is build upon the generic theorem prover Isabelle.
Duration Calculus was originally developed by Zhou, Hoare and Ravn .
DC is an interval logic where time is modelled by the real numbers and
boolean functions of time are used to capture the state of real time systems.
A concise reference to the foundation, development and properties of the
logic is . The development of Isabelle/DC is described in the PhD-thesis
of Søren Heilmann .
1999-5-23: This page constructed.
Software for Isabelle/98
PC/DC is another proof
assistant for Duration Calculus. It builds on PVS.
Zhou Chaochen, C.A.R. Hoare, and Anders P. Ravn, A calculus of durations,
Information Processing Letters, 40(5):269-276, 1992.
Michael R. Hansen and Zhou Chaochen, Duration calculus, logical foundations,
Aspects of Computing, 9:283-303, 1997.
Søren T. Heilmann, Proof Support for Duration Calculus, Department
of Information Technology, Technical University of Denmark, PhD-thesis,
January 1999. Abstract
Søren Heilmann, e-mail:email@example.com,