Symbolic Verification in Synchronous Constraint Programming
Christophe MAURAS
Univ. de Nantes IRIN
2, rue de la Houssiniere BP 92208, 44322 Nantes cedex 3, FRANCE

We propose an extension of Timed Default Concurrent Constraint language designed by Saraswat and Gupta. Our proposal is to replace Gentzen constraint system by a mixed constraint system with boolean formulas and linear constraints over rationals. We then propose using model checking like proposed in CLP by Delzanno and Podelski, to verify synchronous programs in Timed Default CC. This allows to deal with properties of numerical variables.

Slides (.pdf)