enter search term and/or author name
Transition predicate abstraction and fair termination
Andreas Podelski, Andrey Rybalchenko
Article No.: 15
Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a...
Saturn: A scalable framework for error detection using Boolean satisfiability
Yichen Xie, Alex Aiken
Article No.: 16
This article presents Saturn, a general framework for building precise and scalable static error detection systems. Saturn exploits recent advances in Boolean satisfiability (SAT) solvers and is path sensitive, precise down to the bit level, and...
Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem
J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, Alan Schmitt
Article No.: 17
We propose a novel approach to the view-update problem for tree-structured data: a domain-specific programming language in which all expressions denote bidirectional transformations on trees. In one direction, these transformations---dubbed...