-
Article
Synthesis of circular compositional program proofs via abduction
This paper presents a new technique for synthesizing circular compositional proofs of program correctness. Our technique uses abductive inference to decompose the proof into small lemmas (i.e., compositionalit...
-
Chapter and Conference Paper
Bottom-Up Context-Sensitive Pointer Analysis for Java
This paper describes a new bottom-up, subset-based, and context-sensitive pointer analysis for Java. The main novelty of our technique is the constraint-based handling of virtual method calls and instantiation...
-
Chapter and Conference Paper
Optimal Guard Synthesis for Memory Safety
This paper presents a new synthesis-based approach for writing low-level memory-safe code. Given a partial program with missing guards, our algorithm synthesizes concrete predicates to plug in for the missing ...
-
Chapter and Conference Paper
Explain: A Tool for Performing Abductive Inference
This paper describes a tool called Explain for performing abductive inference. Logical abduction is the problem of finding a simple explanatory hypothesis that explains observed facts. Specifically, given a set o...
-
Chapter and Conference Paper
Automated Inference of Library Specifications for Source-Sink Property Verification
Many safety properties in program analysis, such as many memory safety and information flow problems, can be formulated as source-sink problems. While there are many existing techniques for checking source-sink p...
-
Chapter and Conference Paper
Synthesis of Circular Compositional Program Proofs via Abduction
This paper presents a technique for synthesizing circular compositional proofs of program correctness. Our technique uses abductive inference to decompose the proof into small lemmas, which are represented as ...
-
Chapter and Conference Paper
Minimum Satisfying Assignments for SMT
A minimum satisfying assignment of a formula is a minimum-cost partial assignment of values to the variables in the formula that guarantees the formula is true. Minimum satisfying assignments have applications in...
-
Article
Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
We propose a novel, sound, and complete Simplex-based algorithm for solving linear inequalities over integers. Our algorithm, which can be viewed as a semantic generalization of the branch-and-bound technique, sy...
-
Chapter and Conference Paper
Simplifying Loop Invariant Generation Using Splitter Predicates
We present a novel static analysis technique that substantially improves the quality of invariants inferred by standard loop invariant generation techniques. Our technique decomposes multi-phase loops, which requ...
-
Chapter and Conference Paper
Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis
Static analysis techniques that represent program states as formulas typically generate a large number of redundant formulas that are incrementally constructed from previous formulas. In addition to querying s...
-
Chapter and Conference Paper
Fluid Updates: Beyond Strong vs. Weak Updates
We describe a symbolic heap abstraction that unifies reasoning about arrays, pointers, and scalars, and we define a fluid update operation on this symbolic heap that relaxes the dichotomy between strong and weak ...
-
Chapter and Conference Paper
Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
We propose a novel, sound, and complete Simplex-based algorithm for solving linear inequalities over integers. Our algorithm, which can be viewed as a semantic generalization of the branch-and-bound technique, sy...
