Isabelle/DC: Proof Assistant for Duration Calculus
Isabelle/DC is a proof assistant for the realtime logic Duration Calculus.
Isabelle/DC is build upon the generic theorem prover Isabelle.
Duration Calculus was originally developed by Zhou, Hoare and Ravn [1].
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 [2]. The development of Isabelle/DC is described in the PhDthesis
of Søren Heilmann [3].
News

1999523: This page constructed.
Software for Isabelle/98
Related links

PC/DC is another proof
assistant for Duration Calculus. It builds on PVS.
References

Zhou Chaochen, C.A.R. Hoare, and Anders P. Ravn, A calculus of durations,
Information Processing Letters, 40(5):269276, 1992.

Michael R. Hansen and Zhou Chaochen, Duration calculus, logical foundations,
Formal
Aspects of Computing, 9:283303, 1997.

Søren T. Heilmann, Proof Support for Duration Calculus, Department
of Information Technology, Technical University of Denmark, PhDthesis,
January 1999. Abstract
, Postscript
Søren Heilmann, email:sth@sth.dk,
last modified:2000117