Article

The SLAM project: debugging system software via static analysis

Authors:

Sriram K. RajamaniAuthors Info & Claims

POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 1 - 3

https://doi.org/10.1145/503272.503274

Published: 01 January 2002 Publication History

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.

References

[1]

G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. In POPL '02. ACM, January 2002.]]

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.]]

Digital Library

[3]

T. Ball, T. Millstein, and S. K. Rajamani. Polymorphic predicate abstraction. Technical Igeport MSIg-TI%-2001-10, Microsoft Igesearch, 2001.]]

[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.]]

Digital 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.]]

[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.]]

Digital 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.]]

Digital 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.]]

Digital Library

[9]

T. Ball and S. K. Rajamani. SLIC: A specification language tbr interface checking. TechnicM Report MSR-TR-2001-21, Microsoft Research, 2001.]]

[10]

R. Bryant. Graph-based algorithms tbr boolean function manipulation. IEEE Transactions on Cow,parers, C-35(8):677 691, 1986.]]

Digital 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.]]

Digital 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.]]

Digital 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.]]

Digital Library

[14]

M. Das. Unification-based pointer analysis with directional assignInents. In PLD1 00: Programing Language Design and Implementation, pages 35 46. ACM, 2000.]]

Digital 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.]]

Digital 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.]]

[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.]]

Digital 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.]]

Digital Library

[19]

D. Evans. Static detection of dynamic memory errors. In PLD1 '96, pages 44 53. ACM, May 1996.]]

Digital 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.]]

Digital Library

[21]

T. A. Hienzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL '02. ACM, January 2002.]]

Digital 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.]]

Digital Library

[23]

R. Kurshan. Computer-eided Verification of Coordinating Processes. Princeton University Press, 1994.]]

Digital Library

[24]

L. Lamport. Proving the correctness of multiprocess programs. 1EEE Transactions on software Engineering, S19-3(2):125 143, 1977.]]

[25]

G. Necula, S. McPeak, and VV. YVeinler. CCured: Type-safe retrofitting of legacy code. In POPL '02. ACM, January 2002.]]

Digital 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.]]

Digital 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.]]

Digital 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.]]

Digital Library

[29]

F. B. Schneider. Enforceable security policies. ACM :Transactions on lnformation and system security, 3(1):30 50, February 2000.]]

Digital 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.]]

Cited By

Yao PZhou JXiao XShi QWu RZhang C(2024)Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence AnalysisProceedings of the ACM on Programming Languages10.1145/36564008:PLDI(567-592)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656400
Beyer DLee N(2024)The Transformation Game: Joining Forces for VerificationPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75778-5_9(175-205)Online publication date: 18-Nov-2024
https://doi.org/10.1007/978-3-031-75778-5_9
Alviano MDodaro CFiorentino SPreviti ARicca F(2023)ASP and subset minimalityArtificial Intelligence10.1016/j.artint.2023.103931320:COnline publication date: 5-Jun-2023
https://dl.acm.org/doi/10.1016/j.artint.2023.103931
Show More Cited By

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 ...
Practical EJB Project for Beginners
Contributing to the Eclipse Project: Principles, Plug-ins and Gerrit Code Review

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2002

351 pages

ISBN:1581134509

DOI:10.1145/503272

Conference Chair:
John Launchbury
OGI and Galois Connections
,
Program Chair:
John C. Mitchell
Stanford University

ACM SIGPLAN Notices Volume 37, Issue 1
Jan. 2002
342 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/565816
Issue’s Table of Contents

Copyright © 2002 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL02

Sponsor:

POPL02: The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2002

January 16 - 18, 2002

Oregon, Portland

Acceptance Rates

POPL '02 Paper Acceptance Rate 28 of 128 submissions, 22%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

757
Total Citations
View Citations
3,477
Total Downloads

Downloads (Last 12 months)89
Downloads (Last 6 weeks)8

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yao PZhou JXiao XShi QWu RZhang C(2024)Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence AnalysisProceedings of the ACM on Programming Languages10.1145/36564008:PLDI(567-592)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656400
Beyer DLee N(2024)The Transformation Game: Joining Forces for VerificationPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75778-5_9(175-205)Online publication date: 18-Nov-2024
https://doi.org/10.1007/978-3-031-75778-5_9
Alviano MDodaro CFiorentino SPreviti ARicca F(2023)ASP and subset minimalityArtificial Intelligence10.1016/j.artint.2023.103931320:COnline publication date: 5-Jun-2023
https://dl.acm.org/doi/10.1016/j.artint.2023.103931
Su TZhang CYan YFan LLiu YFu ZSu Z(2023)Towards Efficient Data-Flow Test Data GenerationTheories of Programming and Formal Methods10.1007/978-3-031-40436-8_10(257-293)Online publication date: 8-Sep-2023
https://doi.org/10.1007/978-3-031-40436-8_10
Beyer DChien PLee N(2023)Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C TranslatorTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_12(152-172)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30820-8_12
Kovács L(2023)Symbolic Computation in Automated Program ReasoningFormal Methods10.1007/978-3-031-27481-7_1(3-9)Online publication date: 3-Mar-2023
https://doi.org/10.1007/978-3-031-27481-7_1
Beyer DArtho CÖlveczky P(2022)Cooperative Verification: Towards Reliable Safety-Critical Systems (Invited Talk)Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems10.1145/3563822.3572548(1-2)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563822.3572548
Murali APeña LBlanchard ELöding CMadhusudan P(2022)Model-guided synthesis of inductive lemmas for FOL with least fixpointsProceedings of the ACM on Programming Languages10.1145/35633546:OOPSLA2(1873-1902)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563354
Tsukada TUnno H(2022)Software model-checking as cyclic-proof searchProceedings of the ACM on Programming Languages10.1145/34987256:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498725
Beyer DDangl MDietsch DHeizmann MLemberger TTautschnig M(2022)Verification WitnessesACM Transactions on Software Engineering and Methodology10.1145/347757931:4(1-69)Online publication date: 8-Sep-2022
https://dl.acm.org/doi/10.1145/3477579
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents