Skip to main content
SpringerLink
Log in

Automatically validating temporal safety properties of interfaces

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2001)

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

Included in the following conference series:

Abstract

We present a process for validating temporal safety properties of software that uses a well-defined interface. The process requires only that the user state the property of interest. It then automatically creates abstractions of C code using iterative refinement, based on the given property. The process is realized in the SLAM toolkit, which consists of a model checker, predicate abstraction tool and predicate discovery tool. We have applied the SLAM toolkit to a number of Windows NT device drivers to validate critical safety properties such as correct locking behavior. We have found that the process converges on a set of predicates powerful enough to validate properties in just a few iterations.

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. T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation (to appear). ACM, 2001.

    Google Scholar 

  2. T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstractions for model checking C programs. In TACAS 01: Tools and Algorithms for Construction and Analysis of Systems(to appear). Springer-Verlag, 2001.

    Google Scholar 

  3. T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: SPIN Workshop, LNCS 1885, pages 113–130. Springer-Verlag, 2000.

    Google Scholar 

  4. D. Blei and et al. Vampyre: A proof generating theorem prover — http://www.eecs.berkeley.edu/ rupak/vampyre.

  5. R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.

    Article  Google Scholar 

  6. W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software-Practice and Experience, 30(7):775–802, June 2000.

    Article  MATH  Google Scholar 

  7. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer Aided Verification, LNCS 1855, pages 154–169. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  8. J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In ICSE 2000: International Conference on Software Engineering, pages 439–448. ACM, 2000.

    Google Scholar 

  9. P. Cousot and R. Cousot. Abstract interpretation: a uni_ed lattice model for the static analysis of programs by construction or approximation of fix points. In POPL 77: Principles of Programming Languages, pages 238–252. ACM, 1977.

    Google Scholar 

  10. P. Cousot and R. Cousot. Temporal abstract interpretation. In POPL 00: Principles of Programming Languages, pages 12–25. ACM, 2000.

    Google Scholar 

  11. M. Das. Unification-based pointer analysis with directional assignments. In PLDI 00: Programming Language Design and Implementation, pages 35–46. ACM, 2000.

    Google Scholar 

  12. R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software In PLDI 01: Programming Language Design and Implementation(to appear). ACM, 2001.

    Google Scholar 

  13. D. Detlefs, G. Nelson, and J. Saxe. Simplify theorem prover — http://research.compaq.com/src/esc/simplify.html.

  14. D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report Research Report 159, Compaq Systems Research Center, December 1998.

    Google Scholar 

  15. E. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

    Google Scholar 

  16. M. Dwyer and L. Clarke. Data flow analysis for verifying properties of concurrent programs. In FSE 94: Foundations of Software Engineering, pages 62–75. ACM, 1994.

    Google Scholar 

  17. M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In ICSE 01: Software Engineering (to appear), 2001.

    Google Scholar 

  18. D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation. Usenix Association, 2000.

    Google Scholar 

  19. C. Flanagan, R. Joshi, and K. R. M. Leino. Annotation inference for modular checkers. Information Processing Letters (to appear), 2001.

    Google Scholar 

  20. S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In CAV 97: Computer Aided Verification, LNCS 1254, pages 72–83. Springer-Verlag, 1997.

    Google Scholar 

  21. G. Holzmann. The Spin model checker. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.

    Article  MathSciNet  Google Scholar 

  22. G. Holzmann. Logic verification of ANSI-C code with Spin. In SPIN 00: SPIN Workshop, LNCS 1885, pages 131–147. Springer-Verlag, 2000.

    Google Scholar 

  23. R. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.

    Google Scholar 

  24. L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, 1977.

    Article  MathSciNet  Google Scholar 

  25. K. R. M. Leino and G. Nelson. An extended static checker for Modula-3. In CC 98: Compiler Construction, LNCS 1383, pages 302–305. Springer-Verlag, 1998.

    Google Scholar 

  26. G. Necula. Proof carrying code. In POPL 97: Principles of Programming Languages, pages 106–119. ACM, 1997.

    Google Scholar 

  27. G. Nelson. Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981.

    Google Scholar 

  28. S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In CAV 96: Computer-Aided Verification, LNCS 1102, pages 411–414. Springer-Verlag, 1996.

    Google Scholar 

  29. J. Pincus. personal communication, October 2000.

    Google Scholar 

  30. W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, August 1992.

    Article  Google Scholar 

  31. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL 95: Principles of Programming Languages, pages 49–61. ACM, 1995.

    Google Scholar 

  32. H. Saidi and N. Shankar. Abstract and model check while you prove. In CAV 99: Computer-aided Verification, LNCS 1633, pages 443–454. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  33. D. Schmidt. Data flow analysis is model checking of abstract interpretation. In POPL 98: Principles of Programming Languages, pages 38–48. ACM, 1998.

    Google Scholar 

  34. M. Sharir and A. Pnueli. Two approaches to interprocedural data dalow analysis. In Program Flow Analysis: Theory and Applications, pages 189–233. Prentice-Hall, 1981.

    Google Scholar 

  35. N. Suzuki and K. Ishihata. Implementation of an array bound checker. In POPL 77: Principles of Programming Languages, pages 132–143. ACM, 1977.

    Google Scholar 

  36. Z. Xu, B. P. Miller, and T. Reps. Safety checking of machine code. In PLDI 00: Programming Language Design and Implementation, pages 70–82. ACM, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Productivity Tools, Microsoft Research, USA

    Thomas Ball & Sriram K. Rajamani

Authors
  1. Thomas Ball
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sriram K. Rajamani
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, Manhattan, KS, 66506-2302, USA

    Matthew Dwyer

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ball, T., Rajamani, S.K. (2001). Automatically validating temporal safety properties of interfaces. In: Dwyer, M. (eds) Model Checking Software. SPIN 2001. Lecture Notes in Computer Science, vol 2057. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45139-0_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-45139-0_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45139-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation