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

research-article

Calysto: scalable and precise extended static checking

Authors:

Alan J. HuAuthors Info & Claims

ICSE '08: Proceedings of the 30th international conference on Software engineering

Pages 211 - 220

https://doi.org/10.1145/1368088.1368118

Published: 10 May 2008 Publication History

Abstract

Automatically detecting bugs in programs has been a long-held goal in software engineering. Many techniques exist, trading-off varying levels of automation, thoroughness of coverage of program behavior, precision of analysis, and scalability to large code bases. This paper presents the Calysto static checker, which achieves an unprecedented combination of precision and scalability in a completely automatic extended static checker. Calysto is interprocedurally path-sensitive, fully context-sensitive, and bit-accurate in modeling data operations --- comparable coverage and precision to very expensive formal analyses --- yet scales comparably to the leading, less precise, static-analysis-based tool for similar properties. Using Calysto, we have discovered dozens of bugs, completely automatically, in hundreds of thousands of lines of production, open-source applications, with a very low rate of false error reports. This paper presents the design decisions, algorithms, and optimizations behind Calysto's performance.

References

[1]

Saturn-discuss mailing list archives, August 2007. https://mailman.stanford.edu/pipermail/saturn-discuss/.

[2]

D. Babic and A. J. Hu. Exploiting Shared Structure in Software Verification Conditions. Third International Haifa Verification Conference, HVC 2007, LNCS vol 4899, pp. 169--184. Springer, 2008.

Digital Library

[3]

D. Babic and A. J. Hu. Structural Abstraction of Software Verification Conditions. Computer Aided Verification (CAV), LNCS vol 4590, pp. 371--383. Springer, 2007.

Digital Library

[4]

D. Babic and M. Musuvathi. Modular Arithmetic Decision Procedure. Technical Report TR-2005-114, Microsoft Research Redmond, 2005.

[5]

T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic Predicate Abstraction of C Programs. Programming Language Design and Implementation (PLDI), pp. 203--213. ACM Press, 2001.

Digital Library

[6]

T. Ball and S. K. Rajamani. The Slam project: debugging system software via static analysis. Principles of Prog Languages (POPL), pp. 1--3. ACM Press, 2002.

Digital Library

[7]

A. R. Bradley, Z. Manna, and H. B. Sipma. What's decidable about arrays? Verification, Model Checking, and Abstract Interpretation: (VMCAI), volume 3855 of LNCS, pp. 427--442. Springer, 2006.

Digital Library

[8]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677--691, 1986.

Digital Library

[9]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), LNCS vol 2988, pp. 168--176. Springer, 2004.

[10]

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. Predicate abstraction of ansi-c programs using sat. Form. Methods Syst. Des., 25(2-3):105--127, 2004.

Digital Library

[11]

E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Workshop on Logics of Programs, pp. 52--71, May 1981. Published 1982 as LNCS Vol 131.

Digital Library

[12]

P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL, pp. 238--252, 1977.

Digital Library

[13]

D. W. Currie, A. J. Hu, S. Rajan, and M. Fujita. Automatic formal verification of DSP software. 37th Design Automation Conference, pp. 130--135. ACM/IEEE, 2000.

Digital Library

[14]

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans. Programming Languages and Systems, 13(4):451--490, October 1991.

Digital Library

[15]

D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report SRC-RR-159, Digital Equipment Corporation, Systems Research Center, 1998. Now available from HP Labs.

[16]

E. W. Dijkstra and C. S. Scholten. Predicate calculus and program semantics. Springer, 1990.

Digital Library

[17]

I. Dillig, T. Dillig, and A. Aiken. Static error detection using semantic inconsistency inference. SIGPLAN Not., 42(6):435--445, 2007.

Digital Library

[18]

D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. Operating Systems Design and Implementation (OSDI), 2000.

Digital Library

[19]

C. Flanagan, K. Leino, M. Lillibridge, G. Nelson, J. Saxe, and R. Stata. Extended static checking for Java. Programming Language Design and Implementation (PLDI), pp. 234--245. ACM Press, 2002.

Digital Library

[20]

D. Heine and M. S. Lam. Static detection of leaks in polymorphic containers. 28th Intl Conf on Software Engineering, pp. 252--261, 2006.

Digital Library

[21]

T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. POPL'2002: Principles of Programming Languages, pp. 58--70. ACM Press, 2002.

Digital Library

[22]

T. Hoare. The verifying compiler: A grand challenge for computing research. J. ACM, 50(1):63--69, 2003.

Digital Library

[23]

G. J. Holzmann. The model checker spin. IEEE Trans. Softw. Eng., 23(5):279--295, 1997.

Digital Library

[24]

F. Hutter, D. Babic, H. H. Hoos, and A. J. Hu. Boosting Verification by Automatic Tuning of Decision Procedures. Formal Methods in Computed Aided Design (FMCAD), pp. 27--34. IEEE Computer Society Press, 2007.

Digital Library

[25]

S. Johnson. Lint, a C program checker. Computer Science Technical Report 65, Bell Laboratories, December 1977.

[26]

J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976.

Digital Library

[27]

A. Kölbl and C. Pixley. Constructing efficient formal models from high-level descriptions using symbolic simulation. Intl J of Parallel Programming, 33(6):645--666, 2005.

Digital Library

[28]

C. Lattner and V. Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. CGO '04: Intl Symp on Code Generation and Optimization, pp. 75--88. IEEE Computer Society, 2004.

Digital Library

[29]

K. R. M. Leino. Efficient weakest preconditions. Inf. Process. Lett., 93(6):281--288, 2005.

Digital Library

[30]

K. R. M. Leino and F. Logozzo. Loop invariants on demand. APLAS, volume 3780 of LNCS, pp. 119--134. Springer, 2005.

Digital Library

[31]

Y. V. Matiyasevich. Hilbert's Tenth Problem. MIT Press, 1993.

Digital Library

[32]

J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. 5th Intl Symp on Programming, pp. 337--351. Springer, 1981. LNCS Vol 137.

Digital Library

[33]

Robby, M. B. Dwyer, and J. Hatcliff. Bogor: an extensible and highly-modular model checking framework. European Software Engineering Conf./Symp. Foundations of Software Engineering (ESEC/FSE), pp. 267--276. ACM Press, 2003.

Digital Library

[34]

G. S. Tseitin. On the complexity of derivation in propositional calculus. Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pp. 466--483. Springer, 1983.

[35]

P. Tu and D. A. Padua. Efficient Building and Placing of Gating Functions. Programming Language Design and Implementation (PLDI), pp. 47--55, 1995.

Digital Library

[36]

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engineering, 10(2):203--232, April 2003.

Digital Library

[37]

J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. Programming Language Design and Implementation (PLDI), pp. 131--144. ACM Press, 2004.

Digital Library

[38]

Y. Xie and A. Aiken. Scalable error detection using boolean satisfiability. Principles of Programming Languages (POPL), pp. 351--363. ACM Press, 2005.

Digital Library

Cited By

Beyer DKettl MLemberger T(2024)Decomposing Software Verification using Distributed Summary SynthesisProceedings of the ACM on Software Engineering10.1145/36607661:FSE(1307-1329)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660766
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
Zheng MShi QLiu XXu XYu LLiu CWei GZhang X(2024)ParDiff: Practical Static Differential Analysis of Network Protocol ParsersProceedings of the ACM on Programming Languages10.1145/36498548:OOPSLA1(1208-1234)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649854
Show More Cited By

Index Terms

Calysto: scalable and precise extended static checking

Recommendations

Abstracting Induction by Extrapolation and Interpolation
VMCAI 2015: Proceedings of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8931

We introduce a unified view of induction performed by automatic verification tools to prove a given program specification This unification is done in the abstract interpretation framework using extrapolation widening/dual-widening and interpolation ...
Model checking of software for microcontrollers

The interest of industries in model checking software for microcontrollers is increasing. However, there are currently no appropriate tools that can be applied by embedded systems developers for the direct verification of software for microcontrollers ...
Precise flow-insensitive may-alias analysis is NP-hard

Determining aliases is one of the foundamental static analysis problems, in part because the precision with which this problem is solved can affect the precision of other analyses such as live variables, available expressions, and constant propagation. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '08: Proceedings of the 30th international conference on Software engineering

May 2008

558 pages

ISBN:9781605580791

DOI:10.1145/1368088

General Chair:
Wilhelm Schäfer
University of Paderborn
,
Program Chairs:
Matthew B. Dwyer
University of Nebraska
,
Volker Gruhn
University of Leipzig

Copyright © 2008 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: 10 May 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSE '08

Sponsor:

ICSE '08: International Conference on Software Engineering

May 10 - 18, 2008

Leipzig, Germany

Acceptance Rates

ICSE '08 Paper Acceptance Rate 56 of 370 submissions, 15%;

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

106
Total Citations
View Citations
880
Total Downloads

Downloads (Last 12 months)23
Downloads (Last 6 weeks)3

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Beyer DKettl MLemberger T(2024)Decomposing Software Verification using Distributed Summary SynthesisProceedings of the ACM on Software Engineering10.1145/36607661:FSE(1307-1329)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660766
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
Zheng MShi QLiu XXu XYu LLiu CWei GZhang X(2024)ParDiff: Practical Static Differential Analysis of Network Protocol ParsersProceedings of the ACM on Programming Languages10.1145/36498548:OOPSLA1(1208-1234)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649854
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
Tang WDong DLi SWang CYao PZhou JZhang C(2024) Octopus: Scaling Value-Flow Analysis via Parallel Collection of Realizable Path ConditionsACM Transactions on Software Engineering and Methodology10.1145/363274333:3(1-33)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632743
Zhang BChen WYao PWang CTang WZhang CTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)SIRO: Empowering Version Compatibility in Intermediate Representations via Program SynthesisProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3620666.3651366(882-899)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620666.3651366
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
Baek SLee S(2024)CaLLi: OCaml library for static analysis of LLVM bitcodeSoftwareX10.1016/j.softx.2024.10181027(101810)Online publication date: Sep-2024
https://doi.org/10.1016/j.softx.2024.101810
Guo YZhou JYao PShi QZhang CDwyer MDamian DZeller A(2022)Precise divide-by-zero detection with affirmative evidenceProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510066(1718-1729)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510066
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