A decade of software model checking with SLAM

Abstract

SLAM is a program-analysis engine used to check if clients of an API follow the API's stateful usage rules.

References

1. Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., and Hawkins, P. An overview of the Saturn project. In Proceedings of the 2007 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (San Diego, June 13--14). ACM Press, New York, 2007, 43--48.
2. Ball, T., Majumdar, R., Millstein, T., and Rajamani, S.K. Automatic predicate abstraction of C programs. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (Snowbird, UT, June 20--22). ACM Press, New York, 2001, 203--213.
3. Ball, T., Millstein, T.D., and Rajamani, S.K. Polymorphic predicate abstraction. ACM Transactions on Programming Languages and Systems 27, 2 (Mar. 2005), 314--343.
4. Ball, T., Podelski, A., and Rajamani, S.K. Boolean and Cartesian abstractions for model checking C programs. In Proceedings of the Seventh International Conference on Tools and Algorithms for Construction and Analysis of Systems (Genova, Italy, Apr. 2--6). Springer, 2001, 268--283.
5. Ball, T. and Rajamani, S.K. Bebop: A symbolic model checker for Boolean programs. In Proceedings of the Seventh International SPIN Workshop on Model Checking and Software Verification (Stanford, CA, Aug. 30--Sept. 1). Springer, 2000, 113--130.
6. Ball, T. and Rajamani, S.K. Boolean Programs: A Model and Process for Software Analysis. Technical Report MSR-TR-2000-14. Microsoft Research, Redmond, WA, Feb. 2000.
7. Ball, T. and Rajamani, S.K. Automatically validating temporal safety properties of interfaces. In Proceedings of the Eighth International SPIN Workshop on Model Checking of Software Verification (Toronto, May 19--20). Springer, 2001, 103--122.
8. Ball, T. and Rajamani, S.K. The SLAM project: Debugging system software via static analysis. In Proceedings of the 29 ^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, OR, Jan. 16--18). ACM Press, New York, Jan. 2002, 1--3.
9. Ball, T. and Rajamani, S.K. SLIC: A Specification Language for Interface Checking. Technical Report MSR-TR-2001-21. Microsoft Research, Redmond, WA, 2001.
10. Beyer, D., Henzinger, T.A., Théoduloz, G., and Zufferey, D. Shape refinement through explicit heap analysis. In Proceedings of the 13 ^th International Conference on Fundamental Approaches to Software Engineering (Paphos, Cyprus, Mar. 20--28). Springer, 2010, 263--277.
11. Bryant, R. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35, 8 (Aug. 1986), 677--691.
12. Bush, W.R., Pincus, J.D., and Siela, D.J. A Static analyzer for finding dynamic programming errors. Software-Practice and Experience 30, 7 (June 2000), 775--802.
13. Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H. Modular verification of software components in C. In Proceedings of the 25 ^th International Conference on Software Engineering (Portland, OR, May 3--10). IEEE Computer Society, 2003, 385--395.
14. Clarke, E., Grumberg, O., and Peled, D. Model Checking. MIT Press, Cambridge, MA, 1999.
15. Clarke, E.M. and Emerson, E.A. Synthesis of synchronization skeletons for branching time temporal logic. In Proceedings of the Workshop on Logic of Programs (Yorktown Heights, NY, May 1981). Springer, 1982, 52--71.
16. Clarke, E.M., Emerson, E.A., and Sifakis, J. Model checking: Algorithmic verification and debugging. Commun. ACM 52, 11 (Nov. 2009), 74--84.
17. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. Counterexample-guided abstraction refinement. In Proceedings of the 12 International Conference on Computer-Aided Verification (Chicago, July 15--19). Springer, 2000, 154--169.
18. Clarke, E.M., Kroening, D., and Lerda, F. A tool for checking ANSI-C programs. In Proceedings of the 10 ^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Barcelona, Mar. 29--Apr. 2). Springer, 2004, 168--176.
19. Cook, B., Podelski, A., and Rybalchenko, A. Abstraction refinement for termination. In Proceedings of the 12 ^th International Static Analysis Symposium (London, Sept. 7--9). Springer, 2005, 87--101.
20. Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., and Zheng, H. Bandera: Extracting finite-state models from Java source code. In Proceedings of the 22 ^nd International Conference on Software Engineering (Limerick, Ireland, June 4--11). ACM Press, New York, 2000, 439--448.
21. Cousot, P. and Cousot, R. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth ACM Symposium on Principles of Programming Languages (Los angeles, Jan.). ACM Press, New York, 1977, 238--252.
22. de Moura, L. and Bjørner, N. Z3: an efficient SMT solver. In Proceedings of the 14 ^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Mar. 29--Apr. 6). Springer, 2008, 337--340.
23. Detlefs, D., Nelson, G., and Saxe, J.B. Simplify: A theorem prover for program checking. Journal of the ACM 52, 3 (May 2005), 365--473.
24. Engler, D., Chelf, B., Chou, A., and Hallem, S. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Fourth Symposium on Operating System Design and Implementation (San Diego, Oct. 23--25). Usenix Association, 2000, 1--16.
25. Esparza, J. and Schwoon, S. A BDD-based model checker for recursive programs. In Proceedings of the 13 ^th International Conference on Computer Aided Verification (Paris, July 18--22). Springer, 2001, 324--336.
26. Foster, J.S., Terauchi, T., and Aiken, A. Flow-sensitive type qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, June 17--19). ACM Press, New York, 2002, 1--12.
27. Godefroid, P., Levin, O.Y., and Molnar, D.A. Automated whitebox fuzz testing. In Proceedings of the Network and Distributed System Security Symposium (San Diego, CA, Feb. 10--13). The Internet society, 2008.
28. Godefroid, P., Nori, A.V., Rajamani, S.K., and Tetali, S.D. Compositional may-must program analysis: Unleashing the power of alternation. In Proceedings of the 37 ^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Madrid, Jan. 17--23). ACM Press, New York, 2010, 43--56.
29. Graf, S. and Saïdi, H. Construction of abstract state graphs with PVS. In Proceedings of the Ninth International Conference on Computer-Aided Verification (Haifa, June 22--25). Springer, 72--83.
30. Henzinger, T.A., Jhala, R., Majumdar, R., and McMillan, K.L. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Venice, Jan. 14--16). ACM Press, New York, 2004, 232--244.
31. Henzinger, T.A., Jhala, R., Majumdar, R., and Sutre, G. Lazy abstraction. In Proceedings of the 29 ^th ACM SIGPLAN-SIGACT Symposium Principles of Programming Languages (Portland, OR, Jan. 16--18). ACM Press, New York, 2002, 58--70.
32. Holzmann, G. The SPIN model checker. IEEE Transactions on Software Engineering 23, 5 (May 1997), 279--295.
33. Holzmann, G. Logic verification of ANSI-C code with SPIN. In Proceedings of the Seventh International SPIN Workshop on Model Checking and Software Verification (Stanford, CA, Aug. 30--Sept. 1). Springer, 2000, 131--147.
34. Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., and Ashar, P. Efficient SAT-based bounded model checking for software verification. Theoretical Computer Science 404, 3 (Sept. 2008), 256--274.
35. Kurshan, R. Computer-aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.
36. La Torre, S., Parthasarathy, M., and Parlato, G. Analyzing recursive programs using a fixed-point calculus. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (Dublin, June 15--21). ACM Press, New York, 2009, 211--222.
37. Larus, J.R., Ball, T., Das, M., DeLine, R., Fähndrich, M., Pincus, J., Rajamani, S.K., and Venkatapathy, R. Righting software. IEEE Software 21, 3 (May/June 2004), 92--100.
38. McMillan, K. Symbolic Model Checking: An Approach to the State-Explosion Problem. Kluwer Academic Publishers, 1993.
39. McMillan, K.L. Interpolation and SAT-based model checking. In Proceedings of the 15th International Conference on Computer-Aided Verification (Boulder, CO, July 8--12). Springer, 2003, 1--13.
40. Qadeer, S. and Wu, D. KISS: Keep it simple and sequential. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation (Washington, D.C., June 9--12). ACM Press, New York, 2004, 14--24.
41. Queille, J. and Sifakis, J. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium on Programming (Torino, Italy, Apr. 6--8). Springer, 1982, 337--350.
42. Reps, T., Horwitz, S., and Sagiv, M. Precise interprocedural data flow analysis via graph reachability. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, Jan. 23--25). ACM Press, New York, 1995, 49--61.
43. Sharir, M. and Pnueli, A. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, N.D. Jones and S.S. Muchnick, eds. Prentice-Hall, 1981, 189--233.
44. Vardi, M.Y. and Wolper, P. An automata theoretic approach to automatic program verification. In Proceedings of the Symposium Logic in Computer Science (Cambridge, MA, June 16--18). IEEE Computer Society Press, 1986, 332--344.

Index Terms

• Computer systems organization

  • Dependable and fault-tolerant systems and networks

• General and reference

  • Cross-computing tools and techniques

    • Performance

    • Verification

• Networks

  • Network performance evaluation

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software development techniques

    • Software verification and validation

      • Formal software verification

      • Software defect analysis

        • Software testing and debugging

  • Software notations and tools

  • Software organization and properties

    • Contextual software domains

      • Operating systems

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification