Advertisement

Toupie=μ-calculus+constraints

  • Antoine Rauzy
Session 4: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

This paper presents some of the features of the constraint language Toupie (version 0.26). Toupie is basically a μ-calculus intepreter. Variables takes their values in finite domains, i.e. finite sets of symbolic or numerical constants. Toupie integrates a solver for systems of linear inequations over finite domains and uses an extension of Bryant's binary decision diagrams to encode relations. Combination of μ-calculus expressiveness, efficient coding and manipulation of relations through the use of n-ary decision diagrams and constraint solving technics make Toupie a powerfull tool to perform system of communicating processes analyses.

Keywords

Compact Representation Reachable State Symbolic Execution Finite Domain Finite State Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    A. Arnold and M. Nivat. Comportements de processus. In Colloque AFCET “Les Mathématiques de l'informatique”, 1989.Google Scholar
  2. 2.
    J.P. Billon. Perfect Normal Forms for Discrete Functions. Technical Report DSG/CRG/87014, Centre de Recherche, BULL, 1987.Google Scholar
  3. 3.
    A. Bouali. Études et mises en œ uvre d'outils de vérification basée sur la bisimulation. PhD thesis, Université Paris VII, 03 1993. in french.Google Scholar
  4. 4.
    K. Brace, R. Rudell, and R. Bryant. Efficient Implementation of a BDD Package. In Proceedings of the 27th ACM/IEEE Design Automation Conference. IEEE 0738, 1990.Google Scholar
  5. 5.
    R. Bryant. Graph Based Algorithms for Boolean Fonction Manipulation. IEEE Transactions on Computers, 35:677–691, 8 1986.Google Scholar
  6. 6.
    R. Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams. ACM Computing Surveys, 1992.Google Scholar
  7. 7.
    W. Buettner. Unification in Finite Algebras is Unitary (?). In 9th Conference on Automatic Demonstration, volume 310. LNCS, 1988.Google Scholar
  8. 8.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. IEEE transactions on computers, 1990.Google Scholar
  9. 9.
    M-M. Corsini and A. Rauzy. Symbolic Model Checking and Constraint Logic Programming: a Cross-Fertilization. In Don Sannella, editor, Proceedings of the European Symposium on Programming ESOP'94, volume 788. LNCS, 1994.Google Scholar
  10. 10.
    O. Coudert, C. Berthet, and J-C. Madre. Verification of Synchronous Sequential Machines Based on Symbolic Execution. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, volume 407. LNCS, 1989.Google Scholar
  11. 11.
    R. Enders, T. Filkorn, and D. Taubner. Generating BDDs for Symbolic Model Checking in CCS. Journal of Distributed Computing, 6:155–164, 6 1993.Google Scholar
  12. 12.
    N. Halbwachs. Delay Analysis in Synchronous Programs. In Proceedings of the 5th international conference on Computer Aided Verification CAV'93, volume 697 of LNCS. Springer Verlag, June 1993.Google Scholar
  13. 13.
    M. Henessy and R. Milner. Algebraic laws for non-determinism and concurrency. J. Assoc. Comput. Mach., 32:137–161, 1985.Google Scholar
  14. 14.
    P. Van Hentenryck. Constraint Satisfaction in Logic Programming. Logic Programming Series. MIT Press, 1989.Google Scholar
  15. 15.
    J. Jaffar and J.L. Lassez. Constraint Logic Programming. In Proceedings of Principle of Programming Languages (POPL'87), January 1987.Google Scholar
  16. 16.
    D. Park. Fixpoint Induction and Proofs of Program Properties. Machine Intelligence, 5, 1970.Google Scholar
  17. 17.
    A. Rauzy. Toupie Version 0.25: User's Manual. Technical Report 959-94, LaBRI — URA CNRS 1304 — Université Bordeaux I, 1994.Google Scholar
  18. 18.
    A. Srinivasan, T. Kam, S. Malik, and R.K. Brayton. Algorithms for Discrete Function Manipulation. In Proceedings of International Conference on Computer Aided Design, ICCAD'90, pages 92–95. IEEE, 1990.Google Scholar
  19. 19.
    D.L. Waltz. Generating semantic descriptions for drawings of scenes with shadows. In P.H. Winston, editor, The Psychology of Computer Vision, pages 19–91. Mc Graw Hill, New York, 1975.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Antoine Rauzy
    • 1
  1. 1.LaBRI - CNRS URA 1304Université Bordeaux ITalenceFrance

Personalised recommendations