20 Result(s)
within
Conference Paper
Alex Aiken
-
Chapter and Conference Paper
Speaking Pygion: Experiences Writing an Exascale Single Particle Imaging Code
The goal of the SpiniFEL project was to write, from scratch, a single particle imaging code for exascale supercomputers. The original vision was to have two versions of the code, one in MPI and one in Pygion, ...
-
Chapter and Conference Paper
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a bread...
-
Chapter and Conference Paper
From Invariant Checking to Invariant Inference Using Randomized Search
We describe a general framework c2i for generating an invariant inference procedure from an invariant checking procedure. Given a checker and a language of possible invariants, c2i generates an inference procedur...
-
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
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...
-
Chapter and Conference Paper
Interpolants as Classifiers
We show how interpolants can be viewed as classifiers in supervised machine learning. This view has several advantages: First, we are able to use off-the-shelf classification techniques, in particular support ...
-
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
Saturn: A SAT-Based Tool for Bug Detection
Saturn is a boolean satisfiability (SAT) based framework for static bug detection. Saturn targets software written in C and is designed to support a wide range of property checkers.
-
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
