Skip to main content

Program analysis as constraint solving

Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan

Publisher page dblp BibTeX

Abstract

A constraint-based approach to invariant generation in programs translates a program into constraints that are solved using off-the-shelf constraint solvers to yield desired program invariants.

DOI 10.1145/1375581.1375616

Related papers

Binding-Time Analysis for MetaML via Type Inference and Constraint Solving TACAS 2004
Compact Representation and Interleaved Solving for Scalable Constraint-Based Points-to Analysis CC 2026
JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution) TACAS 2021
Points-To Analysis for Java using Annotated Constraints OOPSLA 2001
Analytic Constraint Solving and Interval Arithmetic POPL 2000
String constraints with concatenation and transducers solved efficiently POPL 2018
Fixpoints for the masses: programming with first-class Datalog constraints OOPSLA 2020
IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications PLDI 2024