Computer Aided Verification
31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I
Page
%P
-
Chapter and Conference Paper
Synthesizing JIT Compilers for In-Kernel DSLs
Modern operating systems allow user-space applications to submit code for kernel execution through the use of in-kernel domain specific languages (DSLs). Applications use these DSLs to customize system policie...
-
Chapter and Conference Paper
Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain
Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. This paper studies the safety and security of smart contracts in the Azure Blockchain Workbench, an enterprise B...
-
Chapter and Conference Paper
Program Synthesis Using Deduction-Guided Reinforcement Learning
In this paper, we present a new program synthesis algorithm based on reinforcement learning. Given an initial policy (i.e. statistical model) trained off-line, our method uses this policy to guide its search a...
-
Book and Conference Proceedings
-
Book and Conference Proceedings
Computer Aided Verification
31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II
-
Book and Conference Proceedings
Verification, Model Checking, and Abstract Interpretation
19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings
-
Chapter and Conference Paper
Learning Abstractions for Program Synthesis
Many example-guided program synthesis techniques use abstractions to prune the search space. While abstraction-based synthesis has proven to be very powerful, a domain expert needs to provide a suitable abstract ...
-
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
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions
In an algorithmic complexity attack, a malicious party takes advantage of the worst-case behavior of an algorithm to cause denial-of-service. A prominent algorithmic complexity attack is regular expression denial...
-
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...
