Skip to main content
SpringerLink
Log in

Predicate Abstraction of Programs with Non-linear Computation

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4218))

Abstract

Verification of programs relies on reasoning about the computations they perform. In engineering programs, many of these computations are non-linear. Although predicate abstraction enables model checking of programs with large state spaces, the decision procedures that currently support predicate abstraction are not able to handle such non-linear computations. In this paper, we propose an approach to model checking a class of data-flow properties for engineering programs that contain non-linear products and transcendental functions. The novelty of our approach is the integration of interval constraint solving techniques into the automated predicate discovery/predicate abstraction process, which extends the expressive power of predicate abstraction-based model checking. Using this approach, we construct a prototype model checker for C programs called VISA (Verification of Industrial-Strength Applications). VISA is built on top of Berkeley’s BLAST and University of Nantes’ Realpaver. We successfully apply VISA to scientific computation libraries and avionics applications to verify the absence of certain runtime arithmetic errors.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Neumaier, A.: Interval Methods for System of Equations. Cambridge University Press, Cambridge (1990)

    Google Scholar 

  2. Alefeld, G., Herzberger, J.: Introduction to Interval Computations. Academic Press, London (1983)

    MATH  Google Scholar 

  3. Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Ball, T.: Formalizing counter-example driven predicate refinement with weakest preconditions. Technical Report MSR-TR-2004-134, Microsoft Research (2004)

    Google Scholar 

  5. Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 457–461. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic Predicate Abstraction of C Programs. In: Proceedings of Programming Languages Design and Implementation (PLDI) 2001, pp. 268–283. ACM Press, New York (2001)

    Google Scholar 

  7. Ball, T., Rajamani, S.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Barret, C., Tinelli, C.: Theory and practice of decision procedures for combinations of theories. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, Springer, Heidelberg (2005)

    Google Scholar 

  9. Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The BLAST query language for software verification. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 2–18. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Collins, G.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

  14. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREE analyser. In: Proceedings of The European Symposium on Programming, pp. 21–30 (2005)

    Google Scholar 

  15. Das, S., Dill, D., Park, S.J.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Proceedings of Conference on Formal Methods in Computer-Aided Design, Portland, Oregon (November 2002)

    Google Scholar 

  17. Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking (2003)

    Google Scholar 

  18. Dowek, G., Geser, A., Muñoz, C.: Tactical conflict detection and resolution in a 3-D airspace. In: Proceedings of the 4th USA/Europe Air Traffic Management R&DSeminar, ATM 2001, Santa Fe, New Mexico, 2001. A long version appears as report NASA/CR-2001-210853 ICASE Report No 2001-7

    Google Scholar 

  19. Dwyer, M., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C., Visser, R., Zheng, H.: Tool-supported Program Abstraction for Finite-state Verification

    Google Scholar 

  20. Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246–249. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  21. Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Google Scholar 

  22. Granvilliers, L.: On the combination of interval constraint solvers. Reliable Computing 7(6), 467–483 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  23. Harvey, W., Stuckey, P.J.: Constraint representation for propagation. In: Maher, M.J., Puget, J.-F. (eds.) CP 1998. LNCS, vol. 1520, pp. 235–245. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  24. Hentenryck, P.V., Michel, L., Deville, Y.: Numerica, A Modeling Language for Global Optimization. MIT Press, Cambridge (1997)

    Google Scholar 

  25. Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstraction from Proofs. In: Proceedings of ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages (POPL), pp. 232–244 (2004)

    Google Scholar 

  26. Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-Safety Proofs for Systems Code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  27. Yamamura, K., Kawata, H., Tokue, A.: Interval analysis using linear programming. In: Proceedings of BIT 38, pp. 188–201 (1998)

    Google Scholar 

  28. Granvilliers, L., Benhamou, F.: Realpaver: An interval solver using constraint satisfaction techniques. ACM Transactions on Mathematical Software (accepted for publication)

    Google Scholar 

  29. McMillan, K.L.: Craig interpolation and reachability analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, p. 336. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  30. McPeak, S., Necula, G.C., Rahul, S.P., Weimer, W.: CIL: Intermediate Languages and Tools for C Program Analysis and Transformation. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol. 2304, Springer, Heidelberg (2002)

    Google Scholar 

  31. Moore, R.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966)

    MATH  Google Scholar 

  32. Owre, S., Rushby, J., Shankar, N.: Pvs: A prototype verification system (1992)

    Google Scholar 

  33. Ratschan, S.: Slides, available at http://www.mpi-sb.mpg.de/~ratschan/decproc1.pdf

  34. Ratschan, S.: Continuous first-order constraint satisfaction. In: Proceedings of Artificial Intelligence and Symbolic Computation. LNCS, Springer, Heidelberg (2002)

    Google Scholar 

  35. Rudin, W.: Principles of Mathematical Analysis, 3rd edn., ch. 10. McGraw-Hill, New York (1976)

    MATH  Google Scholar 

  36. Saidi, H., Shankar, N.: Abstract and Model-check While You Prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 443–454. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  37. Schmidt, D.: Data Flow Analysis is Model Checking of Abstract Interpretation. In: Proceedings of SIGPLAN Symposium on Principles of Programming Languages (POPL 1998) (1998)

    Google Scholar 

  38. Tarski, A.: Logic, Semantics, Metamathematics, papers from 1923 to 1938. Hackett Publishing Company (1983) English Version, original in Polish

    Google Scholar 

  39. Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 248–262. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  40. Visser, W., Park, S., Penix, J.: Applying Predicate Abstraction to Model Check Object-oriented Programs. In: Proceedings of the 33rd ACM SIGSOFT Workshop on Formal Methods in Software Practice,

    Google Scholar 

  41. Adams, W., Loustaunau, P.: An Introduction to Gröbner Bases. American Mathematical Society (1994)

    Google Scholar 

  42. Wallace, M., Novello, S., Schimpf, J.: ECLiPSe: A platform for constraint logic programming (1997)

    Google Scholar 

  43. Xia, S., Vito, B.D., Muñoz, C.: Automated test case generations for non-linear engineering programs. In: Proceedings of the Nineenth International Conference on Automated Software Engineering (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NASA Postdoc at NASA Langley Research Center, Hampton, VA

    Songtao Xia

  2. NASA Langley Research Center, Hampton, VA

    Ben Di Vito

  3. National Institute of Aerospace, Hampton, VA

    Cesar Munoz

Authors
  1. Songtao Xia
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ben Di Vito
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cesar Munoz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. VERIMAG, 2 Avenue de Vignate, Centre Equitation, 38610, Grenoble-Gières, France

    Susanne Graf

  2. Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Wenhui Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Xia, S., Di Vito, B., Munoz, C. (2006). Predicate Abstraction of Programs with Non-linear Computation. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_27

Download citation

  • DOI: https://doi.org/10.1007/11901914_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-47237-7

  • Online ISBN: 978-3-540-47238-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation