CL Group
Publications
Some co-authored and older works can be found here.
Slides from selected talks are on this talks page.
2008
Towards an SMT Proof Format. Aaron Stump and Duckki Oe. In proceedings of
the International Workshop on Satisfiability Modulo Theories (SMT), 2008.
[PDF]
Proof Checking Technology for Satisfiability Modulo Theories. Aaron Stump. In proceedings of
the International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), 2008.
[PDF]
Deciding Joinability Modulo Ground Equations in
Operational Type Theory. Adam Petcher. Master's Thesis, Washington University in
St. Louis, April 2008. [PDF]
2007
Baghak: Developing Sound and Complete Decision Procedures in
Coq. Benjamin Delaware. Master's Thesis, Washington University in
St. Louis, August 2007. [PDF]
Decision procedures are automated theorem proving algorithms which
automatically recognize the theorems of some decidable theory. The
correctness of these algorithms is important, since a design error
could lead to the misidentification of a false statement as a
theorem. In the past, decision procedures have been shown to be
correct by mechanically verifying that they are sound, i.e. they only
identify valid statements. Soundness does not entail correctness,
however, as a decision procedure could still fail to recognize a true
formula from the theory it decides. To rigorously verify that a
decision procedure for a theory T is correct, it must also
be shown to be complete in that it recognize all true propositions
from T.
We have developed a decision procedure called Bagahk for the
validity of formulas modulo the theory of ground equations
T=, which we have proven sound and complete in the proof
assistant Coq. In this thesis, we highlight the important lemmas and
theorems of these proofs. As part of the soundness proof, we embed
Coq-level proof terms into the meta-language of our solver using
reflection. As a result of this, Bagahk can also be used to
assist users in the construction of other proofs. In addition, we
develop a proof system for T= and show that our decision
procedure recognizes all T=-provable propositions,
showing that Bagahk is complete.
A Signature Compiler for the Edinburgh LF. Michael Zeller,
Aaron Stump, and Morgan Deters; International Workshop on Logical
Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007).
[PDF]
This paper describes the Signature Compiler, which can compile an LF
signature to a custom proof checker in either C++ or Java, specialized
for that signature. Empirical results are reported showing
substantial improvements in proof-checking time over existing LF
checkers on benchmarks.
Design and Results of the 2nd Annual Satisfiability Modulo Theories
Competition (SMT-COMP 2006). Clark Barrett, Leonardo de Moura,
and Aaron Stump. Formal Methods in System Design, volume 31, number
3, pages 221-239.
[PDF]
The Satisfiability Modulo Theories Competition
(SMT-COMP) arose from the SMT-LIB initiative to
spur adoption of common, community-designed formats, and
to spark further advances in satisfiability modulo theories (SMT).
The first SMT-COMP was held in 2005 as a satellite event of CAV 2005.
SMT-COMP 2006 was held August 17 - 19, 2006, as a satellite event of
CAV 2006. This paper describes the rules and competition format for
SMT-COMP 2006, the benchmarks used, the participants, and the results.
Directly Reflective Meta-Programming. Aaron Stump. The journal
of Higher Order and Symbolic Computation, to appear [PDF].
Existing meta-programming languages operate on encodings of programs
as data. This paper presents a new meta-programming language, based
on an untyped lambda calculus, in which structurally reflective
programming is supported directly, without any encoding. The language
features call-by-value and call-by-name lambda abstractions, as well
as novel reflective features enabling the intensional manipulation of
arbitrary program terms. The language is scope safe, in the sense
that variables can neither be captured nor escape their scopes. The
expressiveness of the language is demonstrated by showing how to
implement quotation and evaluation operations, as proposed by Wand.
The language's utility for meta-programming is further demonstrated
through additional representative examples. A prototype
implementation is described and evaluated.
2006
Roadmap for Enhanced Languages and Methods to Aid Verification.
Gary T. Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler,
Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale
Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith, and
Aaron Stump. Proceedings of the 5th International Conference on
Generative Programming and Component Engineering, GPCE'06 2006,
Pages 221-236. Also Department of Computer Science, Iowa State
University, TR #06-21, July 2006. [PDF]
This roadmap describes ways that researchers in four areas -- speci-
fication languages, program generation, correctness by construction,
and programming languages -- might help further the goal of verified
software. It also describes what advances the "verified software"
grand challenge might anticipate or demand from work in these
areas. That is, the roadmap is intended to help foster collaboration
between the grand challenge and these research areas. A common goal
for research in these areas is to establish language designs and tool
architectures that would allow multiple annotations and tools to be
used on a single program. In the long term, researchers could try to
unify these annotations and integrate such tools.
Knuth-Bendix Completion with Modern Termination Checking, Ian
Wehrman, Master's Thesis, Washington University in St. Louis, August
2006. Expanded version of RTA 2006 paper below with the same
title. [PDF].
Knuth-Bendix completion is a technique for equational automated
theorem proving based on term rewriting. This classic procedure is
parametrized by an equational theory and a (well-founded) reduction
order used at runtime to ensure termination of intermediate rewriting
systems. Any reduction order can be used in principle, but modern
completion tools typically implement only a few classes of such orders
(e.g., recursive path orders and polynomial orders). Consequently, the
theories for which completion can possibly succeed are limited to
those compatible with an instance of an implemented class of
orders. Finding and specifying a compatible order, even among a small
number of classes, is challenging in practice and crucial to the
success of the method.
In this thesis, a new variant on the Knuth-Bendix completion procedure
is developed in which no order is provided by the user. Modern
termination-checking methods are instead used to verify termination of
rewriting systems. We prove the new method correct and also present an
implementation called Slothrop which obtains solutions for theories
that do not admit typical orders and that have not previously been
solved by a fully automatic tool.
Slothrop: Knuth-Bendix Completion with a Modern Termination
Checker, Ian Wehrman, Aaron Stump, Edwin Westbrook; International
Conference on Rewriting Techniques and Applications (RTA) [PDF].
A Knuth-Bendix completion procedure is parametrized by a reduction
ordering used to ensure termination of intermediate and resulting
rewriting systems. While in principle any reduction ordering can be
used, modern completion tools typically implement only Knuth-Bendix
and path orderings. Consequently, the theories for which completion
can possibly yield a decision procedure are limited to those that can
be oriented with a single path order. In this paper, we present a
variant on the Knuth-Bendix completion procedure in which no ordering
is assumed. Instead we rely on a modern termination checker to verify
termination of rewriting systems. The new method is correct if it
terminates; the resulting rewrite system is convergent and equivalent
to the input theory. Completions are also not just ground-convergent,
but fully convergent. We present an implementation of the new
procedure, Slothrop, which automatically obtains such completions for
theories that do not admit path orderings.
Free Variable Types, Edwin Westbrook;
Trends in Functional
Programming (TFP), April 2006. [PDF]
"Knuth-Bendix Completion of Theories of Commuting Group
Endomorphisms", Aaron Stump and Bernd Loechner, Information
Processing Letters, Volume 98, Issue 5, pages 195-198. [PDF]
Knuth-Bendix completions of the equational theories of k greater than
or equal to 2 commuting group endomorphisms are obtained, using
automated theorem proving and modern termination checking. This
improves on modern implementations of completion, where the orderings
implemented cannot orient the commutation rules. The result has
applications in decision procedures for automated verification.
"POPLmark 1a with Named Bound Variables", Aaron Stump,
presented at an informal workshop on the POPLmark
challenge, January 2006, following POPL. [PDF] [Coq proofs].
"Property Types: Semantic Programming for Java", Aaron Stump
and Ian Wehrman, Foundations and Developments of Object-Oriented
Languages (FOOL/WOOD), January, 2006, affiliated with POPL 2006. [PDF] [BIB]. [Examples from the paper]
Dependent types have been proposed for functional programming
languages as a means of expressing semantically rich properties as
types. In this paper, we consider the problem of bringing semantic
programming based on dependent types to an object-oriented language. A
type-theoretically light extension to Java (with generics) is
proposed, called property types. These are types indexed not by other
types (as in Java with generics) but by immutable expressions. We
consider programming with two examples of property types: a property
type HasFactors< long x, Set a>, expressing that the elements of a
are the multiplicative prime factors of x; and a property type
Sorted< List l>, expressing that l is sorted.
"Design and Results of the 1st Satisfiability Modulo Theories
Competition (SMT-COMP 2005)", Clark Barrett, Leonardo de Moura,
and Aaron Stump; the Journal of Automated Reasoning, Volume 35, pages
373-390 [PDF].
2005
"Programming with Proofs: Language-Based Approaches to Totally
Correct Software", Aaron Stump; invited position paper at IFIP
working group conference on "Verified Software: Theories, Tools,
Experiments" [PDF (slightly revised
May 31, 2006] [BIB].
"A Language-based Approach to Functionally Correct
Imperative Programming", Edwin Westbrook, Aaron Stump, Ian Wehrman;
the 10th ACM SIGPLAN International Conference on Functional
Programming (ICFP) [PDF]
[BIB]
[Tech Report].
In this paper a language-based approach to functionally correct
imperative programming is proposed. The approach is based on a
programming language called RSP1, which combines dependent types,
general recursion, and imperative features in a type-safe way, while
preserving decidability of type checking. The methodology used is
that of internal verification, where programs manipulate
programmer-supplied proofs explicitly as data. The fundamental
technical idea of RSP1 is to identify problematic operations as
impure, and keep them out of dependent types. The resulting language
is powerful enough to verify statically non-trivial properties of
imperative and functional programs. The paper presents the ideas
through the examples of statically verified merge sort, statically
verified imperative binary search trees, and statically verified
directed acyclic graphs.
"Validated Construction of Congruence Closures", Aaron Stump;
the CADE Workshop on Disproving [PDF]
[BIB].
It is by now well known that congruence closure (CC) algorithms can be
viewed as implementing ground completion: given a set of ground
equations, the CC algorithm computes a convergent rewrite system whose
equational theory conservatively extends that of the original set of
equations. We call such a rewrite system a CC for the original set.
This paper describes work in progress to create an implementation of a
CC algorithm which is validated, in the following sense. Any
non-aborting, terminating run of the implementation is guaranteed to
produce a CC for the input set of equations. Note that aborting or
failing to terminate can happen for implementations of CC algorithms
only due to bugs in code; the algorithms themselves are usually proved
terminating and correct. Validation of an implementation of a CC
algorithm is achieved by implementing the algorithm in RSP1, a
dependently typed programming language. Type checking ensures that
proofs of convergence and conservative extension are well-formed.
"Mining Propositional Simplification Proofs for Small Validating
Clauses", Ian Wehrman and Aaron Stump; the 3rd Workshop on
Pragmatics of Decision Procedures in Automated Reasoning [PDF]
[BIB].
The problem of obtaining small conflict clauses in SMT systems has
recently received much attention. This paper reports work in
progress which aims to obtain small subsets of the current partial
assignment that imply the goal formula, in the case when the goal
formula has been propositionally simplified under that assignment to
true. The approach used is algebraic proof mining.
Proofs that the goal is equivalent to true (in the current
assignment) are viewed as first-order terms. An equational theory
between proofs is then defined, which is sound with respect to the
equivalence relation ``proves a theorem in common.'' The theory is
completed to obtain a convergent rewrite system that puts proofs
into a canonical form. While our canonical form does not use the
minimal number of assumptions, it does drop many unnecessary parts
of the proof. These unnecessary pieces correspond to the
simplifications performed, e.g., on one side of a disjunction whose
other side simplifies to true. The paper concludes with
speculation on how to obtain a canonical proof with the minimal
number of assumptions.
"SMT-COMP: Satisfiability Modulo Theories Competition", Clark
Barrett, Leonardo de Moura, Aaron Stump; 17th International Conference
on Computer-Aided Verification (CAV), short paper [PDF] [BIB], short talk at CAV '05 [PDF].
This short paper describes the setup for the Satisfiability Modulo
Theories Competition, held as a satellite event of CAV in 2005. See
also the SMT-COMP '05 webpage.
"Formalizing the Meta-Theory of Q0 in Rogue-Sigma-Pi", Li-Yang
Tan, 17th European Summer School in Logic, Language, and Information
(ESSLLI), student session, 2005 [PDF].
Introduced by Peter Andrews in the 1960's, Q0 is a classical
higher-order logic based on simply-typed lambda calculus. This paper
presents our work in progress on the formalizing of Q0 in a
programming language, Rogue-Sigma-Pi (RSP), with the aim of validating
its meta-theory. The main challenge of this project arises from the
fact that while all logical derivations are carried out in much detail
in Andrews' formalism, many of the syntactic derivations have been
kept implicit. Therefore, most of our work has been devoted to
setting up a framework that allows us to formalize low-level syntactic
notions of Q0, such as variable occurrences, bindings and replacement.
This formalization also includes proving meta-theoretic properties of
these various syntactic notions. Building on the the ability to prove
syntactic derivations assumed in Andrews' formalism, recent progress
has led to the proving of basic meta-theorems of Q0, such as the
equality rules, alpha-equivalence, beta- and eta-conversions, as well
as capture-avoiding substitution. This paper will discuss the
theoretical and engineering challenges faced in our formalizing of Q0
in RSP that is guided by a faithful adherence to Andrews' presentation
on paper.
"What a Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms", Joel Brandt, Master's Thesis, April 2005.
[PDF],
[BIB]
The Edinburgh Logical Framework (LF) has been proposed as a system for
expressing inductively defined sets. I will present an inductive
definition of the set of manifold meshes in LF. This definition takes
into account the topological characterization of meshes, namely their
Euler Characteristic. I will then present a set of dependent data
types based on this inductive definition. These data types are
defined in a programming language based on LF. The language's type
checking guarantees that any typeable expression represents a correct
manifold mesh. Furthermore, any mesh can be represented using these
data types. Hence, the encoding is sound and complete.
"The Algebra of Equality Proofs", Aaron Stump and
Li-Yang Tan, at RTA 2005. [PDF], [BIB]
Proofs of equalities may be built from assumptions using proof rules
for reflexivity, symmetry, and transitivity. Reflexivity is an axiom
proving x=x for any x; symmetry is a 1-premise rule taking a proof of
x=y and returning a proof of y=x; and transitivity is a 2-premise rule
taking proofs of x=y and y=z, and returning a proof of x=z. Define an
equivalence relation to hold between proofs iff they prove a theorem
in common. The main theoretical result of the paper is that if all
assumptions are independent, this equivalence relation is axiomatized
by the standard axioms of group theory: reflexivity is the unit of the
group, symmetry is the inverse, and transitivity is the
multiplication. Using a standard completion of the group axioms, we
obtain a rewrite system which puts equality proofs into canonical
form. Proofs in this canonical form use the fewest possible
assumptions, and a proof can be canonized in linear time using a
simple strategy. This result is applied to obtain a simple extension
of the union-find algorithm for ground equational reasoning which
produces minimal proofs. The time complexity of the original
union-find operations is preserved, and minimal proofs are produced in
worst-case time $O(n^{\textit{log}_2 3})$, where $n$ is the number of
expressions being equated. As a second application, the approach is
used to achieve significant performance improvements for the CVC
cooperating decision procedure.
2004
"Logical Semantics for the Rewriting Calculus", Aaron Stump
and Carsten Schuermann, at the 5th International Workshop on
Strategies in Automated Deduction (STRATEGIES
04). [PS (revised January 31,
2005)],[BIB]
The Rewriting Calculus has been proposed as a language for defining
term rewriting strategies. Rules are explicitly represented as terms,
and are applied explicitly to other terms to transform them. Sets of
rules may be applied to (sets of) terms non-deterministically to
obtain sets of results. Strategies are implemented as rules which
accept other rules as arguments and apply them in certain ways. This
paper describes work in progress to strengthen the Rewriting Calculus
by giving it a logical semantics. Such a semantics can provide
crucial guidance for studying the language and increasing its
expressive power. The latter is demonstrated by adding support to the
Rewriting Calculus for what we call \emph{higher-form rewriting},
where rules rewrite other rules. The logical semantics used is based
on ordered linear logic. The paper develops the ideas through several
examples.
"Validated Proof-Producing Decision Procedures", Robert
Klapper and Aaron Stump, at PDPAR 04. [PS], [BIB]
A widely used technique to integrate decision procedures (DPs) with
other systems is to have the DPs emit proofs of the formulas they
report valid. One problem that arises is debugging the
proof-producing code; it is very easy in standard programming
languages to write code which produces an incorrect proof. This paper
demonstrates how proof-producing DPs may be implemented in a
programming language, called Rogue-Sigma-Pi (RSP), whose type system
ensures that proofs are manipulated correctly. RSP combines the Rogue
rewriting language and the Edinburgh Logical Framework (LF).
Type-correct RSP programs are partially correct: essentially, any
putative LF proof object produced by a type-correct RSP program is
guaranteed to type check in LF. The paper describes a simple
proof-producing combination of propositional satisfiability checking
and congruence closure implemented in RSP.
"Imperative LF Meta-Programming", Aaron Stump, at the 4th
International Workshop on Logical Frameworks and Meta-Languages (LFM 04),
2004. [PS], [BIB]
Logical frameworks have enjoyed wide adoption as meta-languages for
describing deductive systems. While the techniques for representing
object languages in logical frameworks are relatively well understood,
languages and techniques for meta-programming with them are much less
so. This paper presents work in progress on a programming language
called Rogue-Sigma-Pi (RSP), in which general programs can be written
for soundly manipulating objects represented in the Edinburgh Logical
Framework (LF). The manipulation is sound in the sense that, in the
absence of runtime errors, any putative LF object produced by a
well-typed RSP program is guaranteed to type check in LF. An
important contribution is an approach for soundly combining imperative
features with higher-order abstract syntax. The focus of the paper is
on demonstrating RSP through representative LF meta-programs.
"From Rogue to MicroRogue", Aaron Stump, Ryan Besand,
James Brodman, Jonathan Hseu, and Bill Kinnersley, 5th International
Workshop on Rewriting Logic and Applications (affiliated with ETAPS),
2004. [PS],
[BIB]
The Rewriting Calculus has been proposed as a foundational system
combining the central ideas of lambda-calculus and term rewriting.
The rewriting is explicit, in the sense that rules must be applied
explicitly to terms to transform them. This paper begins with an
imperative version of the Rewriting Calculus called Rogue. It then
shows how Rogue can itself be conveniently implemented by an even more
foundational system called MicroRogue. MicroRogue rewrites terms
using a global set of first-order rules. Rules can be enabled,
disabled, and dynamically added in scopes, which can be pushed and
popped. MicroRogue also provides mechanisms for specifying evaluation
order. Using these primitives, a Rogue interpreter can be implemented
in less than 40 lines of MicroRogue code.
2003
"Rogue Decision Procedures", Aaron Stump, Arun
Deivanayagam, Spencer Kathol, Dylan Lingelbach, and Daniel Schobel,
1st International Workshop on Pragmatics of Decision Procedures in
Automated Reasoning (PDPAR '03), 2003. [PS], [BIB]
Efficient decision procedures require a substantial
engineering effort to implement in mainstream languages. This paper
proposes a new programming language called Rogue for implementing
decision procedures. Rogue is a rewriting language with backtrackable
mutable expression attributes and an interface to a fast SAT solver.
Work in progress on implementing a Nelson-Oppen style cooperating
validity checker in Rogue is also briefly described.
"Subset Types and Partial Functions", Aaron
Stump, at CADE-19, 2003. This
is an extended version with some corrections, modified 7/24/03. [PS], [PDF], [BIB]
A classical higher-order logic PFsub of partial functions is defined.
The logic extends a version of Farmer's logic PF by enriching the type
system of the logic with subset types and dependent types. Validity
in PFsub is then reduced to validity in PF by a translation.