14 Result(s)
-
Chapter and Conference Paper
Verification as Learning Geometric Concepts
We formalize the problem of program verification as a learning problem, showing that invariants in program verification can be regarded as geometric concepts in machine learning. Safety properties define bad stat...
-
Chapter and Conference Paper
A Data Driven Approach for Algebraic Loop Invariants
We describe a Guess-and-Check algorithm for computing algebraic equation invariants of the form ∧ i f i (x ...
-
Chapter and Conference Paper
Reasoning about Lock Placements
A lock placement describes, for each heap location, which lock guards the location, and under what circumstances. We formalize methods for reasoning about lock placements, making precise the interactions between ...
-
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
Community Epidemic Detection Using Time-Correlated Anomalies
An epidemic is malicious code running on a subset of a community, a homogeneous set of instances of an application. Syzygy is an epidemic detection framework that looks for time-correlated anomalies, i.e., diverg...
-
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
Data Structure Fusion
We consider the problem of specifying data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using re...
-
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...
-
Chapter and Conference Paper
A Capability Calculus for Concurrency and Determinism
We present a capability calculus for checking partial confluence of channel-communicating concurrent processes. Our approach automatically detects more programs to be partially confluent than previous approach...
-
Chapter and Conference Paper
Banshee: A Scalable Constraint-Based Analysis Toolkit
We introduce Banshee, a toolkit for constructing constraint-based analyses. Banshee’s novel features include a code generator for creating customized constraint resolution engines, incremental analysis based on b...
-
Chapter and Conference Paper
Secure Information Flow as a Safety Problem
The termination insensitive secure information flow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, D’Argenio, and Rezk coined the term “self-composition” to des...
-
Chapter and Conference Paper
Type Systems for Distributed Data Sharing
Parallel programming languages that let multiple processors access shared data provide a variety of sharing mechanisms and memory models. Understanding a language’s support for data sharing behavior is critica...
-
Chapter and Conference Paper
Constraint-based program analysis
