iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/S10009-009-0100-Y
Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification

  • Introduction
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Reachability analysis asks whether a system can evolve from legitimate initial states to unsafe states. It is thus a fundamental tool in the validation of computational systems—be they software, hardware, or a combination thereof. We recall a standard approach for reachability analysis, which captures the system in a transition system, forms another transition system as an over-approximation, and performs an incremental fixed-point computation on that over-approximation to determine whether unsafe states can be reached. We show this method to be sound for proving the absence of errors, and discuss its limitations for proving the presence of errors, as well as some means of addressing this limitation. We then sketch how program annotations for data integrity constraints and interface specifications—as in Bertrand Meyer’s paradigm of Design by Contract—can facilitate the validation of modular programs, e.g., by obtaining more precise verification conditions for software verification supported by automated theorem proving. Then we recap how the decision problem of satisfiability for formulae of logics with theories—e.g., bit-vector arithmetic—can be used to construct an over-approximating transition system for a program. Programs with data types comprised of bit-vectors of finite width require bespoke decision procedures for satisfiability. Finite-width data types challenge the reduction of that decision problem to one that off-the-shelf tools can solve effectively, e.g., SAT solvers for propositional logic. In that context, we recall the Tseitin encoding which converts formulae from that logic into conjunctive normal form—the standard format for most SAT solvers—with only linear blow-up in the size of the formula, but linear increase in the number of variables. Finally, we discuss the contributions that the three papers in this special section make in the areas that we sketched above.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Conference Record of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1–3, Portland, Oregon, 16–18 January 2002. ACM Press, New York

  2. Barnett, M., Rustan, K., Leino, M., Schulte, W.: The Spec# programming system: an overview. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, vol. 3362, Lecture Notes in Computer Science, Springer, Heidelberg (2005)

  3. Berezin, S., Ganesh, V., Dill, D.: A decision procedure for fixed-width bit-vectors. Technical report, Computer Science Department, Stanford University, April (2005)

  4. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1579, Lecture Notes in Computer Science, pp. 193–207. Springer, Heidelberg (1999)

  5. Bryant R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  6. Burdy L., Cheon Y., Cok D., Ernst M., Kiniry J., Leavens G.T., Rustan K., Leino M., Poll E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212–232 (2005)

    Article  Google Scholar 

  7. Ciardo, G., Luettgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 328–342, Springer, Heidelberg (2001)

  8. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proceedings of the 12th International Conference on Computer Aided Verification, vol. 1855, Lecture Notes in Computer Science, pp. 154–169, Berlin, Germany. Springer, Heidelberg (2000)

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

    Article  Google Scholar 

  10. Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Proceedings of the 12th International Symposium on Static Analysis, vol. 3672, Lecture Notes in Computer Science, pp. 87–101, London, England, 7–9 September. Springer, Heidelberg (2005)

  11. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs. In: Proceedings of the Fourth ACM Symp. On Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)

  12. Dams, D.: Abstract interpretation and partition refinement for model checking. Ph.D Thesis, Technische Universiteit Eindhoven, The Netherlands (1996)

  13. Dams D., Gerth R., Grumberg O.: Abstract interpretation of reactive systems. ACM TOPLAS 19, 253–291 (1997)

    Article  Google Scholar 

  14. Dimovski, A., Ghica, D.R., Lazić, R.: Data-abstraction refinement: a game semantic approach. In: Proceedings of the 12th International Symposium on Static Analysis, vol. 3672, Lecture Notes in Computer Science, pp. 102–117, London, England, 7–9 September. Springer, Heidelberg (2005)

  15. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Proceedings of the 9th International Conference on Computer Aided Verification, vol. 1254, Lecture Notes in Computer Science, pp. 72–83, Haifa, Israel, Springer, Heidelberg (1997)

  16. Jackson D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)

    Google Scholar 

  17. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2008)

  18. Leavens, G.T., Cheon, Y.: Design By Contract with JML. Tutorial paper available at ftp://ftp.cs.iastate.edu/pub/leavens/JML/, 2003.

  19. Meyer B.: Design by contract. In: Meyer, B., Mandrioli, D. (eds.) Proceedings of Advances in Object-Oriented Software Engineering, pp. 1–50, Prentice-Hall, Englewood Cliffs (1991)

  20. Tan R.P., Edwards S.H.: Experiences evaluating the effectiveness of JML—JUnit testing. ACM SIGSOFT Softw. Eng. Notes 29(5), 1–4 (2004)

    Article  Google Scholar 

  21. Tseitin, G.: On the complexity of proofs in propositional logics. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic 1967–1970, vol. 2. Springer, Heidelberg (1983) (originally published in 1970)

Download references

Author information

Authors and Affiliations

  1. Department of Computing, Imperial College London, South Kensington campus, London, SW7 2AZ, UK

    Michael Huth

  2. Computer Science Department, TECHNION, Israel Institute of Technology, 32000, Technion City, Haifa, Israel

    Orna Grumberg

Authors
  1. Michael Huth
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Orna Grumberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Orna Grumberg.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Huth, M., Grumberg, O. Special section on advances in reachability analysis and decision procedures: contributions to abstraction-based system verification. Int J Softw Tools Technol Transfer 11, 85–94 (2009). https://doi.org/10.1007/s10009-009-0100-y

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-009-0100-y

Keywords

Search

Navigation