Verification of Pushdown Systems Using Omega Algebra with Domain

  • Vincent Mathieu
  • Jules Desharnais
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3929)


We present a framework for the verification of pushdown systems. These systems can model the interprocedural control flow of computer programs. The framework is based on an extension of Kleene algebra called omega algebra with domain. This allows to formulate behavioural properties that refer to both actions and states.


Binary Relation Domain Operator Regular Language Atomic Proposition Kripke Frame 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Handbook of Process Algebra, pp. 545–623. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  2. 2.
    Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)zbMATHGoogle Scholar
  4. 4.
    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic (to appear); Preliminary version: Report No. 2003-07, Universität Augsburg, Institut für Informatik (2003)Google Scholar
  5. 5.
    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110, 366–390 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems (TOPLAS) 19, 427–443 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244–259. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  8. 8.
    Mathieu, V.: Vérification des systèmes à pile au moyen des algèbres de Kleene. Forthcoming Master’s thesis, Université Laval, Québec, Canada (2006)Google Scholar
  9. 9.
    Schwoon, S.: Model-Checking Pushdown Systems. Ph.D. thesis, Technische Universität München (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Vincent Mathieu
    • 1
  • Jules Desharnais
    • 1
  1. 1.Département d’informatique et de génie logicielUniversité LavalCanada

Personalised recommendations