Static Analysis of Programs Using Omega Algebra with Tests

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


Recently, Kozen has proposed a framework based on Kleene algebra with tests for verifying that a program satisfies a security policy specified by a security automaton. A security automaton is used for the specification of linear safety properties on finite and infinite runs. This kind of property is very interesting for most common programs. However, it is not possible to specify liveness properties with security automata. In this paper, we use omega algebra with tests and automata on infinite words to extend the field of properties that can be handled by security automata in Kozen’s framework.


Regular Expression Security Policy Liveness Property Trace Model 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.
    Bolduc, C.: Oméga-algèbre — Théorie et application en vérification de programmes. Forthcoming M.Sc. thesis, Université Laval, Québec, Canada (2006)Google Scholar
  2. 2.
    Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    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
  4. 4.
    Cohen, E.: Omega algebra and concurrency control. Presentation made at the 56th meeting of the IFIP Working Group 2.1, Ameland, The Netherlands (2001)Google Scholar
  5. 5.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering, pp. 411–420. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  6. 6.
    Kozen, D.: Some results in dynamic model theory. Science of Computer Programming 51, 3–22 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Kozen, D.: Kleene algebra with tests and the static analysis of programs. Technical report 1915-2003, Computer Science Department, Cornell University (2003)Google Scholar
  8. 8.
    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
  9. 9.
    Möller, B.: Lazy Kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Safra, S.: Complexity of Automata on Infinite Objects. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel (1989)Google Scholar
  11. 11.
    Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and System Security 3, 30–50 (2000)CrossRefGoogle Scholar
  12. 12.
    von Wright, J.: From Kleene algebra to refinement algebra. LNCS, vol. 2385, pp. 233–262. Springer, Heidelberg (2002)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

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

Personalised recommendations