Advertisement

Abstract

Based on constraint database techniques, we present a new approach to software verification. This new approach has some similarity to abstract interpretation that uses various widening operators; therefore, we call the new approach l-u widening. We show that our l-u widening leads to a more precise over-approximation of the invariants in a program than comparable previously proposed widening operators based on difference-bound matrices, although l-u widening can be computed as efficiently as the other widening operators. We show that constraint database techniques can compute non-convex program invariants too. Finally, we give a compact representation of addition-bound matrices, which generalize difference-bound matrices.

Keywords

Model Check Widening Operator Abstract Interpretation Program Variable Constraint Logic Programming 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., et al.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Anderson, S., Revesz, P.: Verifying the incorrectness of programs and automata. In: Zucker, J.-D., Saitta, L. (eds.) SARA 2005. LNCS (LNAI), vol. 3607, pp. 1–13. Springer, Heidelberg (2005)Google Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  4. 4.
    Colmerauer, A.: Note sur Prolog III. In: Proc. Séminaire Programmation en Logique, pp. 159–174 (1986)Google Scholar
  5. 5.
    Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 17–19. Springer, Heidelberg (2005)Google Scholar
  6. 6.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. ACM Principles on Programming Languages, ACM Press, New York (1977)Google Scholar
  7. 7.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. ACM Principles on Programming Languages, ACM Press, New York (1978)Google Scholar
  8. 8.
    Delzanno, G., Podelski, A.: Model checking in. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, Springer, Heidelberg (1999)Google Scholar
  9. 9.
    Dincbas, M., Van Hentenryck, P., Simonis, H., Aggoun, A., Graf, T., Berthier, F.: The constraint logic programming language chip. In: Proc. Fifth Generation Computer Systems, Tokyo, Japan, pp. 693–702 (1988)Google Scholar
  10. 10.
    Fribourg, L., Olsén, H.: A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints 2, 3–4 (1997)CrossRefGoogle Scholar
  11. 11.
    Fribourg, L., Richardson, J.D.C.: Symbolic verification with gap-order constraints. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 20–37. Springer, Heidelberg (1997)Google Scholar
  12. 12.
    Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, Springer, Heidelberg (1993)Google Scholar
  14. 14.
    Harvey, W., Stuckey, P.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proc. Australian Computer Science Conference (Australian Computer Science Communications), pp. 102–11 (1997)Google Scholar
  15. 15.
    Jaffar, J., Lassez, J.L.: Constraint logic programming. In: Proc. 14th ACM Symposium on Principles of Programming Languages, pp. 111–119 (1987)Google Scholar
  16. 16.
    Jaffar, J., Maher, M.: Constraint logic programming: A survey. J. Logic Programming 19(20), 503–581 (1994)CrossRefMathSciNetGoogle Scholar
  17. 17.
    Kanellakis, P.C., Kuper, G.M., Revesz, P.: Constraint query languages. In: Proc. ACM Symposium on Principles of Database Systems, pp. 299–313 (1990)Google Scholar
  18. 18.
    Kanellakis, P.C., Kuper, G.M., Revesz, P.: Constraint query languages. Journal of Computer and System Sciences 51(1), 26–52 (1995)CrossRefMathSciNetGoogle Scholar
  19. 19.
    Kerbrat, A.: Reachable state space analysis of lotos specifications. In: Proc. 7th International Conference on Formal Description Techniques, pp. 161–76 (1994)Google Scholar
  20. 20.
    Kuper, G.M., Libkin, L., Paredaens, J. (eds.): Constraint Databases. Springer, Heidelberg (2000)zbMATHGoogle Scholar
  21. 21.
    Marriott, K., Stuckey, P.J.: Programming with Constraints: An Introduction. MIT Press, Cambridge (1998)zbMATHGoogle Scholar
  22. 22.
    McMillan, K.: Symbolic Model Checking. Kluwer, Norwell (1993)zbMATHGoogle Scholar
  23. 23.
    Miné, A.: The octagon abstract domain. In: Proceedings Analysis, Slicing and Transformation, pp. 310–319. IEEE Press, Los Alamitos (2001)Google Scholar
  24. 24.
    Pratt, V.: Two easy theories whose combination is hard. MIT Technical Report (1977)Google Scholar
  25. 25.
    Revesz, P.: A closed-form evaluation for Datalog queries with integer (gap)-order constraints. Theoretical Computer Science 116(1), 117–149 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Revesz, P.: Datalog programs with difference constraints. In: Proc. 12th International Conference on Applications of Prolog. pp. 69–76 (1999)Google Scholar
  27. 27.
    Revesz, P.: Reformulation and approximation in model checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol. 1864, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  28. 28.
    Revesz, P.: Introduction to Constraint Databases. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  29. 29.
    Revesz, P., Chen, R., Kanjamala, P., Li, Y., Liu, Y., Wang, Y.: The MLPQ/GIS constraint database system. In: ACM SIGMOD International Conference on Management of Data (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Peter Revesz
    • 1
  1. 1.Max Planck Institut für Informatik, University of Nebraska-Lincoln 

Personalised recommendations