Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2004: Static Analysis pp 38–52Cite as

Completeness Refinement in Abstract Symbolic Trajectory Evaluation

  • Conference paper

  • 466 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3148))

Abstract

In this paper we study the relation between the lack of completeness in abstract symbolic trajectory evaluation and the structure of the counterexamples that can be derived in case of property failure. We characterize the presence of false negatives as a loss of completeness of the underlying abstraction. We prove how standard completeness refinement in abstract interpretation provides a systematic way for refining abstract symbolic trajectory evaluation in order to gain completeness for the properties of interest.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Chou, C.T.: The mathematical foundation of symbolic trajectory evaluation, pp. 196–207 (1999)

    Google Scholar 

  2. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  3. Clarke, E.M., 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, pp. 154–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL 1977 ), pp. 238–252. ACM Press, New York (1977)

    Chapter  Google Scholar 

  5. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979 ), pp. 269–282. ACM Press, New York (1979)

    Chapter  Google Scholar 

  6. Grumberg, O., Clarke, E.M., Peled, D.A.: Medel Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  7. Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. of the ACM. 47(2), 361–416 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  9. Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst. 20(5), 1067–1109 (1998)

    Article  Google Scholar 

  10. Jain, A.: Formal Hardware Verification by Symbolic Trajectory Evauation. PhD thesis, Carnegie-Mellon University (July 1997)

    Google Scholar 

  11. Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6, 11–44 (1995)

    Article  MATH  Google Scholar 

  12. Lu, Y.: Automatic Abstract in Model Checking. PhD thesis, Department of Electrical and Computer Engineering, Carnegie Institute of Technology, Carnegie Mellon University, Pittsburgh (2000)

    Google Scholar 

  13. Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18–32. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Designs 6(2), 147–189 (1995)

    Article  Google Scholar 

  15. Yang, J., Goel, A.: Gste through a case of study. In: International conference on Computer-Aided Design, pp. 534–541. IEEE/ACM (2002)

    Google Scholar 

  16. Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. In: International conference on Computer Design, pp. 360–365. IEEE, Los Alamitos (2001)

    Google Scholar 

  17. Yang, J., Seger, C.J.H.: Generalized symbolic trajectory evaluation - abstraction in action. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 70–87. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Verona, Strada Le Grazie 15, 37134, Verona, Italy

    Mila Dalla Preda

Authors
  1. Mila Dalla Preda
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Verona, Strada Le Grazie, 15, 37134, Verona, Italy

    Roberto Giacobazzi

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dalla Preda, M. (2004). Completeness Refinement in Abstract Symbolic Trajectory Evaluation. In: Giacobazzi, R. (eds) Static Analysis. SAS 2004. Lecture Notes in Computer Science, vol 3148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27864-1_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27864-1_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22791-5

  • Online ISBN: 978-3-540-27864-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation