Thomas Ball
ABSTRACT
The goal of the SLAM project is to check whether or not a program obeys "API usage rules" that specify what it means to be a good client of an API. The SLAM toolkit statically analyzes a C program to determine whether or not it violates given usage rules. The toolkit has two unique aspects: it does not require the programmer to annotate the source program (invariants are inferred); it minimizes noise (false error messages) through a process known as "counterexample-driven refinement". SLAM exploits and extends results from program analysis, model checking and automated deduction. We have successfully applied the SLAM toolkit to Windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.
- 1.G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. In POPL '02. ACM, January 2002.]] Google Scholar
Digital Library
- 2.T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automarie predicate abstraction of C programs. In PLD1 01: Programming Language Design Implementation, pages 203 213. ACM, 2001.]] Google ScholarDigital Library
- 3.T. Ball, T. Millstein, and S. K. Rajamani. Polymorphic predicate abstraction. Technical Igeport MSIg-TI%-2001-10, Microsoft Igesearch, 2001.]]Google Scholar
- 4.T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstractions for model checking C programs. In TAUAS 01: Tools and Algorithms fur Construction and Analysis of System, s, LNCS 2031, pages 268 283. Springer-Verlag, 2001.]] Google ScholarDigital Library
- 5.T. Ball, A. Podelski, and S. K. Rajamani. Oil the relative completeness of abstraction refinement. Technical Report MSR-TR- 2001-106, Microsott Research, 2001.]]Google Scholar
- 6.T. Ball and S. K. Rajamani. Bebop: A symbolic model checker tbr Boolean programs. In SPIN 00: SPIN Workshop, LNCS 1885, pages 113 130. Springer-Verlag, 2000.]] Google ScholarDigital Library
- 7.T. Ball and S. K. Rajamani, Automatically validating temporal safety properties of interfaces. In SPIN 01:SPIN Workshop, LNCS 20557, pages 103 122. Springer-Verlag, 2001.]] Google ScholarDigital Library
- 8.T. Ball and S. K. Rajamani. Bebop: A path-sensitive interprocedural dataflow engine. In PAb'TE 01: Workshop on Program Analysis for Software Tools and Engineering, pages 97 103. ACM, 2001.]] Google ScholarDigital Library
- 9.T. Ball and S. K. Rajamani. SLIC: A specification language tbr interface checking. TechnicM Report MSR-TR-2001-21, Microsoft Research, 2001.]]Google Scholar
- 10.R. Bryant. Graph-based algorithms tbr boolean function manipulation. IEEE Transactions on Cow,parers, C-35(8):677 691, 1986.]] Google ScholarDigital Library
- 11.J. Burch, 19. Clarke, K. McMillan, D. Dill, and L. tiwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142 170, 1992.]] Google ScholarDigital Library
- 12.W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer tbr finding dynamic programming errors, Software-Practice and Experience, 30(7):775 802, June 2000.]] Google ScholarDigital Library
- 13.P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In POPL 77: Principles of Programing Languages, pages 238 252. ACM, 1977.]] Google ScholarDigital Library
- 14.M. Das. Unification-based pointer analysis with directional assignInents. In PLD1 00: Programing Language Design and Implementation, pages 35 46. ACM, 2000.]] Google ScholarDigital Library
- 15.S. Das and D. L. Dill. Successive approximation of abstract trailsition relations. In LIC'S 01: Symposium on Logic in Computer science, 2001.]] Google ScholarDigital Library
- 16.D. L. Detlet, K. E. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report Research Report 159, Compaq Systems Igesearch Center, December 1998.]]Google Scholar
- 17.M. Dwyer, J. tiatcliff, B. Joehanes, S. Laubach, C. Pasareanu, bobby, VV. Visser, and It. Zheng. Tool-supported program abstraction for finite-state verification. In 1USE 01: software Engineering, pages 177 187, 2001.]] Google ScholarDigital Library
- 18.D. Engler, B. Chelf, A. Chou, and S. tiallem. Checking system rules using system-specific, programmer-written compiler extensions. In Oh'D1 00: Operating System Design and lmplementation. Usenix Association, 2000.]] Google ScholarDigital Library
- 19.D. Evans. Static detection of dynamic memory errors. In PLD1 '96, pages 44 53. ACM, May 1996.]] Google ScholarDigital Library
- 20.S. Graf and It. Sa;fdi. Construction of abstract state graphs with PVS. In C'AV P7: Computer Aided Verification, LNCS 1254, pages 72 83. Springer-Verlag, 1997.]] Google ScholarDigital Library
- 21.T. A. Hienzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL '02. ACM, January 2002.]] Google ScholarDigital Library
- 22.G. Holzmann. Logic verification of ANSI-C code with Spin. In SP1N 00: SP1N Workshop, LNCS 1885, pages 131 147. Springer- Verlag, 2000.]] Google ScholarDigital Library
- 23.R. Kurshan. Computer-eided Verification of Coordinating Processes. Princeton University Press, 1994.]] Google ScholarDigital Library
- 24.L. Lamport. Proving the correctness of multiprocess programs. 1EEE Transactions on software Engineering, S19-3(2):125 143, 1977.]]Google Scholar
- 25.G. Necula, S. McPeak, and VV. YVeinler. CCured: Type-safe retrofitting of legacy code. In POPL '02. ACM, January 2002.]] Google ScholarDigital Library
- 26.T. Reps, S. ttorwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL PS: Principles of Programming Languages, pages 49 61. ACM, 1995.]] Google ScholarDigital Library
- 27.V. Rasu and R. Singerman. Oil proving safety properties by integrating static analysis, theorem proving and abstraction. In TAUAS PP: Toools and Algorithms for Construction and Analysis of System, s, LNCS 1579, pages 178 192. Springer-Verlag, 1999.]] Google ScholarDigital Library
- 28.It. Saidi and N. Shanhm Abstract and model check while you prove. In CAV PP: Computer-aided Verification, LNCS 1633, pages 443 454. Springer-Verlag, 1999.]] Google ScholarDigital Library
- 29.F. B. Schneider. Enforceable security policies. ACM :Transactions on lnformation and system security, 3(1):30 50, February 2000.]] Google ScholarDigital Library
- 30.M. Y. Vardi and P. Wolper. An automata theoretic apporach to automatic program verification. In L1US 86: Logic in Computer Science, pages 332 344. I191919 Computer Society Press, 1996.]]Google Scholar
- The SLAM project: debugging system software via static analysis
Recommendations
The SLAM project: debugging system software via static analysis
The goal of the SLAM project is to check whether or not a program obeys "API usage rules" that specify what it means to be a good client of an API. The SLAM toolkit statically analyzes a C program to determine whether or not it violates given usage ...
Comments