Towards a generic tool for reasoning on transition systems

Pierre Casteran

LaBRI, Universite Bordeaux-I

Abstract: The CClair project aims at some kind of "generic" tool for reasoning about labeled transition systems (finite or not, temporized or not). We present the main features we would give to this tool, and discuss which of these features are already implemented.
Cllair being written under the form of Isabelle/HOL theories, we shall discuss which features of this system were actually used (mainly on equality and existential variables), and which features of CClair would be easily adaptable to other frameworks as Coq.

Back to schedule.

Marieke Huisman

Last modified: Tue Apr 3 2001