Snugglebug
Published 15 June 2009
Satish Chandra, Stephen J. Fink, Manu Sridharan
Citations125
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The results show that the algorithmic techniques were critical for successfully analyzing large Java applications and how integrating an inexpensive, custom logic simplifier with weakest precondition computation dramatically improves performance.
Abstract
Symbolic analysis shows promise as a foundation for bug-finding, specification inference, verification, and test generation. This paper addresses demand-driven symbolic analysis for object-oriented programs and frameworks. Many such codes comprise large, partial programs with highly dynamic behaviors--polymorphism, reflection, and so on--posing significant scalability challenges for any static analysis.
Keywords
Computer Science
Communications of the ACMSymbolic execution and program testing
2,991 Citations1976James C. King
A particular system called EFFIGY which provides symbolic execution for program testing and debugging is described, which interpretively executes programs written in a simple PL/I style programming language.
KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs
2,681 Citations2008Cristian Cadar, Daniel Dunbar +1 more
A new symbolic execution tool, KLEE, capable of automatically generating tests that achieve high coverage on a diverse set of complex and environmentally-intensive programs, and significantly beat the coverage of the developers' own handwritten test suite is presented.
Separation logic: a logic for shared mutable data structures
2,127 Citations2003John Reynolds
An extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure is developed, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures.
CUTE
1,653 Citations2005Koushik Sen, Darko Marinov +1 more
A method to represent and track constraints that capture the behavior of a symbolic execution of a unit with memory graphs as inputs is developed and an efficient constraint solver is proposed to facilitate incremental generation of such test inputs.
DART
1,501 Citations2005Patrice Godefroid, Nils Klarlund +1 more
DART is a new tool for automatically testing software that combines three main techniques, automated extraction of the interface of a program with its external environment using static source-code parsing, and dynamic analysis of how the program behaves under random testing and automatic generation of new test inputs to direct systematically the execution along alternative program paths.
Extended static checking for Java
1,339 Citations2002Cormac Flanagan, K. Rustan M. Leino +4 more
The Extended Static Checker for Java (ESC/Java) is introduced, an experimental compile-time program checker that finds common programming errors and provides programmers with a simple annotation language with which programmer design decisions can be expressed formally.
Lazy abstraction
1,146 Citations2002Thomas A. Henzinger, Ranjit Jhala +2 more
This work presents an algorithm for model checking safety properties using lazy abstraction and describes an implementation of the algorithm applied to C programs and provides sufficient conditions for the termination of the method.
Precise interprocedural dataflow analysis via graph reachability
1,135 Citations1995Thomas Reps, Susan Horwitz +1 more
The paper shows how a large class of interprocedural dataflow-analysis problems can be solved precisely in polynomial time by transforming them into a special kind of graph-reachability problem.
The S <scp>LAM</scp> project
919 Citations2002Thomas Ball, Sriram K. Rajamani
This work has successfully applied the SLAM toolkit to Windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.
Program Analysis and Specialization for the C Programming Language
917 Citations2005Lars Ole Andersen, Peter Lee
This thesis presents an automatic partial evaluator for the Ansi C programming language, and proves that partial evaluation at most can accomplish linear speedup, and develops an automatic speedup analysis.
Lecture notes in computer scienceBoogie: A Modular Reusable Verifier for Object-Oriented Programs
784 Citations2006Mike Barnett, Bor-Yuh Evan Chang +3 more
The architecture of a state-of-the-art program verifier for object-oriented programs for compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user interface are described.
Finding bugs is easy
775 Citations2004David Hovemeyer, William Pugh
It is found that even well tested code written by experts contains a surprising number of obvious bugs and that simple automatic techniques can be effective at countering the impact of both ordinary mistakes and misunderstood language features.
Studies in logic and the foundations of mathematicsA Basis for a Mathematical Theory of Computation )
699 Citations1963John McCarthy
Software Practice and ExperienceA static analyzer for finding dynamic programming errors
508 Citations2000William R. Bush, Jonathan D. Pincus +1 more
A compile‐time analyzer that detects dynamic errors in large, real‐world programs, and provides valuable contextual information to the programmer who needs to understand and repair the defects.
Test input generation with java PathFinder
500 Citations2004Willem Visser, Corina S. Păsăreanu +1 more
The main contribution of this work is to show how efficient white-box test input generation can be done for code manipulating complex data, taking into account complex method preconditions.
Lecture notes in computer scienceHoudini, an Annotation Assistant for ESC/Java
394 Citations2001Cormac Flanagan, K. Rustan M. Leino
Houdini is presented, an annotation assistant for the modular checker ESC/Java, which generates a large number of candidate annotations and uses ESC/ Java to verify or refute each of these annotations.
Compositional dynamic test generation
308 Citations2007Patrice Godefroid
This paper introduces a new algorithm, dubbed SMART for Systematic Modular Automated Random Testing, that extends DART by testing functions in isolation, encoding test results as function summaries expressed using input preconditions and output postconditions, and then re-using those summaries when testing higher-level functions.
ACM Transactions on Programming Languages and SystemsA framework for call graph construction algorithms
252 Citations2001David Grove, Craig Chambers
A general parameterized algorithm is presented that encompasses many well-known and novel call graph construction algorithms and is implemented in the Vortex compiler infrastructure, a mature, multilanguage, optimizing compiler.
SYNERGY
251 Citations2006Bhargav S. Gulavani, Thomas A. Henzinger +3 more
This paper proposes a new algorithm, Synergy, which combines testing and verification, and unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.
Boogie: a modular reusable verifier for object-oriented programs
242 Citations2006Mike Barnett, Bor-Yuh Evan Chang +3 more
Lecture notes in computer scienceDemand-Driven Compositional Symbolic Execution
217 Citations2008Saswat Anand, Patrice Godefroid +1 more
A demand-driven compositional interprocedural symbolic execution is performed entirely using first-order logic formulas solved with an off-the-shelf SMT (Satisfiability-Modulo-Theories) solver - this allows a uniform and elegant way of summarizing procedures at various levels of detail and of composing those using logic formulas.
Finding bugs with a constraint solver
211 Citations2000Daniel Jackson, Mandana Vaziri
A method for finding bugs in code that can analyze millions of executions in seconds, and thus rapidly expose quite subtle flaws.
Lecture notes in computer scienceModular Static Program Analysis
153 Citations2002Patrick Cousot, Radhia Cousot
Four basic methods for compositional separate modular static analysis of programs by abstract interpretation are presented and a fifth category which is essentially obtained by composition of the above separate local analyses together with global analysis methods is presented.
Calysto
146 Citations2008Domagoj Babić, Alan J. Hu
The Calysto static checker achieves an unprecedented combination of precision and scalability in a completely automatic extendedstatic checker, and scales comparably to the leading, less precise, static-analysis-based tool for similar properties.
ACM Transactions on Programming Languages and SystemsSaturn
145 Citations2007Yichen Xie, Alex Aiken
Saturn is a general framework for building precise and scalable static error detection systems that exploits recent advances in Boolean satisfiability (SAT) solvers and is path sensitive, precise down to the bit level, and models pointers and heap data.
ACM Transactions on Software Engineering and MethodologyDSD-Crasher
125 Citations2008Christoph Csallner, Yannis Smaragdakis +1 more
DSD-Crasher is a bug finding tool that follows a three-step approach to program analysis that yields benefits compared to past two-step combinations in the literature, and demonstrates higher precision over tools that lack a dynamic step and higher efficiency over tools That lack a static step.
Proofs from tests
119 Citations2008Nels E. Beckman, Aditya V. Nori +2 more
A new refinement operator WPα is introduced that uses only the alias information obtained by symbolically executing a test to refine abstractions in a sound manner and is implemented in a tool called YOGI that plugs into Microsoft's Static Driver Verifier framework.
PSE
106 Citations2004Roman Manevich, Manu Sridharan +3 more
PSE (Postmortem Symbolic Evaluation), a static analysis algorithm that can be used by programmers to diagnose software failures, is described, which combines a novel dataflow analysis and memory alias analysis in a manner that allows for precise exploration of the program's behavior in polynomial time.
Finding bugs efficiently with a SAT solver
67 Citations2007Julian Dolby, Mandana Vaziri +1 more
A soundness proof for the slicing algorithm and a general condition under which relational formulae may be sliced are presented and a new encoding of the program that effectively slices it at the logical level with respect to the specification is presented.
Automated Software EngineeringInferring specifications to detect errors in code
60 Citations2006Mana Taghdiri, Daniel J. Jackson
A new technique is presented to statically check a given procedure against a user-provided property, which automatically infers a context-dependent specification for each procedure call, so that only as much information about a procedure is used as is needed to analyze its caller.