Abstractions from proofs

By Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan. ACM-SIGACT Symposium on Principles of Programming Languages, 2004

465 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/123c4108dcb409121f3b758b26d273699d053fea

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

In Software

Citations in the corpus

Learning a strategy for adapting a program analysis via bayesian optimisation (2015, methodology): “Such analyses commonly adopt counter-example-guided abstraction refinement, and selects a program abstraction based on the feedback from a failed analysis run [1, 4–6, 8, 9, 31, 32].”
Thorough static analysis of device drivers (2006, background): “Work in the BLAST project has shown how to greatly increase the efficiency of the abstract-check-refine loop through the use of incremental analysis [35] and better predicate generation [34].”
Liquid types (2008, methodology): “Predicate abstraction has proven effective for path-sensitive verification of control-dominated properties of first-order imperative programs [3, 16, 11, 4, 29, 17].”
Synthesis of interface specifications for Java classes (2005, background): “Discovering abstraction predicates automatically is an active area of research in software verification (see [6, 20]), and some of these techniques are potentially useful for the purpose of synthesizing interfaces, but this is left for future work.”
A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “In Section IV-E, we survey solvers for BMC formulas, followed by BMC tools in Section IV-F, and conclude this section with a discussion in Section IV-G.”
Lazy Abstraction with Interpolants (2006, methodology): “As in other work using interpolants [6,8], we generate the characteristic formula of a path in static single-assignment (SSA) form.”
An interpolating theorem prover (2005, methodology): “For this purpose, the Blast software model checker uses the interpolating prover in a technique due to Ranjit Jhala [3].”
From program verification to program synthesis (2010, methodology): “We are working on predicate inference techniques—in the style of CEGAR-based model checkers [23]—but for now, we give the tool a candidate set of predicates.”
Automatically generating features for learning program analysis heuristics for C-like languages (2017, methodology): “Addressing these concerns with manually-designed heuristics has been the goal of a large body of research in the program-analysis community [Ball and Rajamani 2002; Clarke et al. 2003; Grebenshchikov et al. 2012; Gulavani et al. 2008; Gupta et al. 2013; Henzinger et al. 2004; Kastrinis and Smaragdak”
The software model checker Blast (2007, background): “At each cut point, the part of the path formula corresponding to the path fragment up to the cut point is φ−, and the part of the formula corresponding to the path fragment after the cut point is φ+ (the cuts are more complicated for function calls; see [45] for details).”