The projects DIXIT and DIXIT' aim at the development of techniques and tools for the specification, refinement, and verification of reactive systems, based on the concept of predicate diagrams representing Boolean abstractions. The tools consist of visual editors, backed up by semantic analysis to generate proof obligations that can be handled by different back-end provers and model checkers.

Contact: Dominique Méry

Duration: DIXIT: 2001/2002, DIXIT': 2003/2004

Support: QSL project on quality and safety of computerized systems

What is Dixit ?

Dixit is an editor for predicate diagrams.

It is developed by project Mosel at LORIA.

How does it work ?

It is simply an editor for predicate diagrams that also generates proof obligations and permits you to check some temporal properties. To prove or check properties, it interacts with external tools such as SPIN and LWAASPIN. To learn more you should read the following publications.


Still not sure yet but we should know soon. By now, you can still download the binary.

Related publications

You can find here some publications at the origin of this software.