ESP: path-sensitive program verification in polynomial time

By Manuvir Das, Sorin Lerner, Mark Seigle. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2002

610 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/d15d7fde2bf968249be6a2d1540b07e551347638

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

RELAY: static race detection on millions of lines of code (2007, background): “Finally, while others have designed bottom-up analyses usi ng complete summaries [4, 6], our work, and the notion of parall eliza-”
A few billion lines of code later (2010, background): “A glance through the literature reveals many ways to go about static bug finding.(1,2,4,7,8,11) For us, the central religion was results: If it worked, it was good, and if not, not.”
WYSINWYX: What you see is not what you eXecute (2010, methodology): “ESP: Path-Sensitive program veri.cation in polynomial time.”
The software model checker Blast (2007, background): “Abstraction-based verifiers [12,28,31,62] compute an abstraction of the state space.”
Formal methods: Practice and experience (2009, neutral): “The ESP tool [Das et al. 2002] is similar to SLAM, but trades precision against large-scale tractability for analysing”
Static Analysis in Disjunctive Numerical Domains (2006, methodology): “The design of such strategies can be performed by techniques that annotate data flow objects by partial trace information such as trace partitioning [20,16], and other pathsensitive data-flow analysis techniques that implicitly manage complexity by joining predicates only when the property to be pro”
Synthesizing API usage examples (2012, methodology): “Next, we use symbolic execution [27] to compute intraprocedural path predicates, logical formulae that describe conditions under which each statement can be reached [28], [29] (Figure 3 line 10).”
Javert: fully automatic mining of general temporal properties from dynamic traces (2008, methodology): “Temporal API specifications are useful for a number of reasons: they can shorten development time by guiding the production of correct code; they can be used as input to static analysis tools [6, 10, 13, 31] to find bugs automatically; and they can facilitate software maintenance tasks by aiding pro”
Effective typestate verification in the presence of aliasing (2006, methodology): “Each composable verifier exploits separation[11, 35]: it performs the typestate checking separately for each abstract o bject of the appropriate type in the program.”
Thorough static analysis of device drivers (2006, methodology): “The esp tool checks C code against state machine properties [26] using interprocedural dataﬂow analysis.”
RacerX: effective, static detection of race conditions and deadlocks (2003, methodology): “The basic algorithm is modeled on the analysis frameworks of ESP [ 11 ] and the MC system [20], both of which are based in part on RHS [28].”
Software model checking (2009, positive): “[ Das et al. 2002] shows how a modicum of path information can be regained by combining typestates with symbolic execution, leading to signiﬁcant improvements in precision.”
Using model checking to find serious file system errors (2004, methodology): “…recent work on bug .nding, including both better type systems [DeLine and F¨ ahndrich 2001; Foster et al. 2002; Flanagan and Freund 2000] and static analysis tools [Das et al. 2002; Ball and Rajamani 2001; Coverity http://coverity.com; Bush et al. 2000; Engler et al. 2000; Flanagan et al. 2002].”
Testing static analysis tools using exploitable buffer overflows from open source code (2004, background): “This type of construct, setting flags to capture state, occurs frequently in real programs [13] and is certainly a common one in the model programs we created for this study.”
Securing web application code by static analysis and runtime protection (2004, background): “[19], is representative of this approach; the contribution is distinctive because ESP allows for flow-sensitive verification that scales to large programs.”
Abstractions from proofs (2004, background): “These two features are often mutually exclusive: flow based interprocedural analyses [11, 15] achieve scalability by fixing a small domain of dataflow facts to be tracked, and compute flow functions over the abstract semantics of the program on this fixed set.”