More Web Proxy on the site http://driver.im/

Article

Scalable error detection using boolean satisfiability

Authors:

Alex AikenAuthors Info & Claims

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 351 - 363

https://doi.org/10.1145/1040305.1040334

Published: 12 January 2005 Publication History

Abstract

We describe a software error-detection tool that exploits recent advances in boolean satisfiability (SAT) solvers. Our analysis is path sensitive, precise down to the bit level, and models pointers and heap data. Our approach is also highly scalable, which we achieve using two techniques. First, for each program function, several optimizations compress the size of the boolean formulas that model the control- and data-flow and the heap locations accessed by a function. Second, summaries in the spirit of type signatures are computed for each function, allowing inter-procedural analysis without a dramatic increase in the size of the boolean constraints to be solved.We demonstrate the effectiveness of our approach by constructing a lock interface inference and checking tool. In an interprocedural analysis of more than 23,000 lock related functions in the latest Linux kernel, the checker generated 300 warnings, of which 179 were unique locking errors, a false positive rate of only 40%.

References

[1]

A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading, Massachusetts, 1986.

Digital Library

[2]

A. Aiken, J. S. Foster, J. Kodumal, and T. Terauchi. Checking and inferring local non-aliasing. In Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 129--140, June 2003.

Digital Library

[3]

T. Ball, B. Cook, V. Levin, and S. Rajamani. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In Proceedings of Fourth International Conference on Integrated Formal Methods. Springer, 2004.

[4]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedings of SPIN 2001 Workshop on Model Checking of Software, pages 103--122, May 2001. LNCS 2057.

Digital Library

[5]

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

Digital Library

[6]

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

Digital Library

[7]

S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of soft are components in C. In Proceedings of the 25th International Conference on Software Engineering (ICSE), pages 385--395, 2003.

Digital Library

[8]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In K. Jensen and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of Lecture Notes in Computer Science, pages 168--176. Springer, 2004.

[9]

M. Das, S. Lerner, and M. Seigle. Path-sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, Berlin, Germany, June 2002.

Digital Library

[10]

D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking systemrules using system-specific, programmer-ritten compiler extensions. In Proceedings of Operating Systems Design and Implementation (OSDI), Sept.2000.

Digital Library

[11]

C. Flanagan and S. Freund. Type inference against races. In Proceedings of 11th Static Analysis Symposium, Verona, Italy, Aug. 2004.

[12]

J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1--12, June 2002.

Digital Library

[13]

S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific, static analyses. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, Berlin, Germany, June 2002.

Digital Library

[14]

T. A. Henzinger, R. Jhala, and R. Majumdar. Lazy abstraction. In Proceedings of the 29th Annual Symposium on Principles of Programming Languages, January 2002.

Digital Library

[15]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Soft are verification with Blast. In Proceedings of the SPIN 2003 Workshop on Model Checking Software, pages 235--239, May 2003. LNCS 2648.

Digital Library

[16]

D. Jackson. Automating first-order relational logic. In Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2000.

Digital Library

[17]

D. Jackson and M. Vaziri. Finding bugs with a constraint solver. In Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis, 2000.

Digital Library

[18]

S. Khurshid, C. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2003.

Digital Library

[19]

D. Kroening, E. Clarke, and K. Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings of DAC 2003, pages 368--371. ACM Press, 2003.

Digital Library

[20]

X. Leroy, D. Doligez, J. Garrigue, and J. Vouillon. The Objective Caml system. Soft are and documentation available on the web, http://caml.inria.fr

[21]

J. Lind-Nielsen. BuDDy, a binary decision diagram package. http://www.itu.dk/research/buddy/.

[22]

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 39th Conference on Design Automation Conference, June 2001.

Digital Library

[23]

G. Necula, S. McPeak, S. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proceedings of the 11th International Conference on Compiler Construction, Mar. 2002.

Digital Library

[24]

Y. Xie and A. Chou. Path sensitive analysis using boolean satisfiability. Technical report, Stanford University, Nov. 2002.

[25]

L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proceedings of International Conference on Computer-Aided Design, SanJose, CA, Nov. 2001.

Digital Library

Cited By

Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Cheng XRen JSui Y(2024)Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point SlicingProceedings of the ACM on Software Engineering10.1145/36437491:FSE(494-516)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643749
Wu RHe YHuang JWang CTang WShi QXiao XZhang CRoychoudhury APaiva AAbreu RStorey M(2024)LibAlchemy: A Two-Layer Persistent Summary Design for Taming Third-Party Libraries in Static Bug-Finding SystemsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639132(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639132
Show More Cited By

Index Terms

Scalable error detection using boolean satisfiability

Recommendations

Saturn: A scalable framework for error detection using Boolean satisfiability
Special issue on POPL 2005

This article presents Saturn, a general framework for building precise and scalable static error detection systems. Saturn exploits recent advances in Boolean satisfiability (SAT) solvers and is path sensitive, precise down to the bit level, and models ...
Scalable error detection using boolean satisfiability
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We describe a software error-detection tool that exploits recent advances in boolean satisfiability (SAT) solvers. Our analysis is path sensitive, precise down to the bit level, and models pointers and heap data. Our approach is also highly scalable, ...
Tracking pointers with path and context sensitivity for bug detection in C programs

This paper proposes a pointer alias analysis for automatic error detection. State-of-the-art pointer alias analyses are either too slow or too imprecise for finding errors in real-life programs. We propose a hybrid pointer analysis that tracks actively ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

402 pages

ISBN:158113830X

DOI:10.1145/1040305

General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

ACM SIGPLAN Notices Volume 40, Issue 1
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
391 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1047659
Issue’s Table of Contents

Copyright © 2005 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: 12 January 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL05

Sponsor:

POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005

January 12 - 14, 2005

California, Long Beach, USA

Acceptance Rates

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

203
Total Citations
View Citations
1,151
Total Downloads

Downloads (Last 12 months)27
Downloads (Last 6 weeks)2

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Cheng XRen JSui Y(2024)Fast Graph Simplification for Path-Sensitive Typestate Analysis through Tempo-Spatial Multi-Point SlicingProceedings of the ACM on Software Engineering10.1145/36437491:FSE(494-516)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643749
Wu RHe YHuang JWang CTang WShi QXiao XZhang CRoychoudhury APaiva AAbreu RStorey M(2024)LibAlchemy: A Two-Layer Persistent Summary Design for Taming Third-Party Libraries in Static Bug-Finding SystemsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639132(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639132
Sun YWang CFan GShi QZhang X(2024)Fast and Precise Static Null Exception Analysis With Synergistic PreprocessingIEEE Transactions on Software Engineering10.1109/TSE.2024.346655150:11(3022-3036)Online publication date: Nov-2024
https://doi.org/10.1109/TSE.2024.3466551
Zhang RCao YLiang RHu PChen K(2024)Optimizing Decompiler Output by Eliminating Redundant Data Flow in Self-Recursive Inlining2024 IEEE International Conference on Software Maintenance and Evolution (ICSME)10.1109/ICSME58944.2024.00015(38-49)Online publication date: 6-Oct-2024
https://doi.org/10.1109/ICSME58944.2024.00015
Orvalho PJanota MManquinho V(2024)cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test CasesFormal Methods10.1007/978-3-031-71162-6_24(463-481)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_24
Shi QXu XZhang XCalandrino JTroncoso C(2023)Extracting protocol format as state machine via controlled static loop analysisProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620630(7019-7036)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620630
Cai YYao PYe CZhang CCalandrino JTroncoso C(2023)Place your locks wellProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620446(3727-3744)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620446
Zhang JWang XZhang HSun HLiu XHu CLiu YJust RFraser G(2023)Detecting Condition-Related Bugs with Control Flow Graph Neural NetworkProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598142(1370-1382)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598142
Madhav C HCheramangalath U(2023)Memory leak detection using Heap Object Flow Graph (HOFG)Proceedings of the 16th Innovations in Software Engineering Conference10.1145/3578527.3578528(1-11)Online publication date: 23-Feb-2023
https://dl.acm.org/doi/10.1145/3578527.3578528
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