Lazy abstraction

By Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, G. Sutre. 2002

1,248 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

How researchers see this paper

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

In Computational Theory and Mathematics

In Software

Citations in the corpus

Formal Security Analysis of Neural Networks using Symbolic Intervals (2018, methodology): “We term this optimization iterative interval refinement because it is in spirit similar to abstraction refinement [4, 13].”
WYSINWYX: What you see is not what you eXecute (2010, methodology): “Over the last seven years, we have developed static-analysis methods to recover a good approximation to the variables and dynamically allocated memory objects of a stripped executable, and to track the .ow of values through them.”
Transition invariants (2004, background): “The realization of the analogous potential for transition invariants is not in the scope of this paper; see, however, [16].”
CPAchecker: A Tool for Configurable Software Verification (2009, background): “The predicate abstraction is based on Cartesian abstraction and lazy abstraction [6].”
Software Verification with BLAST (2003, methodology): “Blast short-circuits the loop from abstraction to verification to refinement, integrating the three steps tightly through “lazy abstraction” [5].”
Lazy Abstraction with Interpolants (2006, methodology): “For comparison to predicate abstraction approach, we use the Blast software model checker [7].”
A new representation and associated algorithms for generalized planning (2011, methodology): “This is a broad and well-studied problem in the model checking literature, with two categories of approaches: (1) the addition of new defined, or instrumentation predicates whose update formulas can be computed automatically [27], and (2) dynamically refining the abstraction by adding new predicates”
Thorough static analysis of device drivers (2006, background): “This harness leads to fewer false errors being reported but results in increased analysis times.”
DART: directed automated random testing (2005, methodology): “We now discuss how to implement the algorithms presented in the previous section for testing programs written in the C programming language.”
Dynamic partial-order reduction for model checking software (2005, background): “This approach is based on initially exploring an arbitrary interleaving of the various concurrent processes/threads, and dynamically tracking interactions between these to identify backtracking points where alternative paths in the state space need to be explored.”
A static analyzer for large safety-critical software (2003, methodology): “In order to allow for the reuse of boolean model checkers, the conjunction of true atomic predicates is usually encoded as a boolean vector over boolean variables associated to each predicate [19] (the disjunctive completion [9] of this abstract domain can also be used to get more precision [2, 21],”
DieHard: probabilistic memory safety for unsafe languages (2006, methodology): “This heap semantics is the same as that assumed by the SLAM toolkit [4] and the BLAST software model checker [19].”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “If the syntactic analysis fails, an iterative algorithm can be applied.”
Modular verification of software components in C (2003, methodology): “The abstraction method used in SLAM and BLAST is closest to ours.”
Secure Information Flow as a Safety Problem (2005, methodology): “However, a state-of-the-art safety analysis tool BLAST [6] fails to terminate given this query; more precisely, BLAST endlessly keeps discovering more and more predicates getting closer and closer to the answer but never actually converging.”
Abstract Regular Model Checking (2004, background): “Indeed, this is the way large (or infinite) state spaces are being successfully handled outside the domain of regular model checking using the so-called abstract-check-refine paradigm [20, 26, 14, 16] implemented, e.”