Ben Delaware
Home Research My CV Pictures Teaching
  • Publications
    • Product Lines of Theorems
    • Benjamin Delaware, William R. Cook, Don Batory
    • To appear, OOPSLA 2011.
    • Coq Development
    • Show Abstract
    Mechanized proof assistants are powerful verification tools, but proof development can be difficult and time-consuming. When verifying a family of related programs, the effort can be reduced by proof reuse. In this paper, we show how to engineer product lines with theorems and proofs built from feature modules. Each module contains proof fragments which are composed together to build a complete proof of correctness for each product. We consider a product line of programming languages, where each variant includes metatheory proofs verifying the correctness of its semantic definitions. This approach has been realized in the Coq proof assistant, with the proofs of each feature independently certifiable by Coq. These proofs are composed for each language variant, with Coq mechanically verifying that the composite proofs are correct. As validation, we formalize a core calculus for Java in Coq which can be extended with any combination of casts, interfaces, or generics.
    • Fitting The Pieces Together: A Machine-Checked Model of Safe Composition
    • Benjamin Delaware, William R. Cook, Don Batory
    • The 7th joint meeting of the European Software Engineering Conference (ESEC) and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE) 2009.
    • Preliminary version presented at Foundations of Aspect-Oriented Languages (FOAL), 2009.
    • Coq Development of LFJ
    • Show Abstract
    Programs of a software product line can be synthesized by composing features which implement a unit of program functionality. In most product lines, only some combination of features are meaningful; feature models express the high-level domain constraints that govern feature compatibility. Product line developers also face the problem of safe composition- whether every product allowed by a feature model is type-safe when compiled and run. To study the problem of safe composition, we present Lightweight Feature Java (LFJ), an extension of Lightweight Java with support for features. We define a constraint-based type system for LFJ and prove its soundness using a full formalization of LFJ in Coq. In LFJ, soundness means that any composition of features that satisfies the typing constraints will generate a well-formed LJ program. If the constraints of a feature model imply these typing constraints then all programs allowed by the feature model are type-safe.
    • Strategic Programming by Model Interpretation and Partial Evaluation
    • William R. Cook, Benjamin Delaware, Thomas Finsterbusch, Ali Ibrahim, Ben Wiedermann
    • Technical Report TR-09-09, UT Austin Department of Computer Sciences.
    • Show Abstract
    In model-driven development, the use of both model translators and model interpreters is widespread. It is also wellknown that partial evaluation can turn an interpreter into a translator. In this paper we show that a simple online partial evaluator is effective at specializing a model interpreter with respect to a model to create a compiled model interpretation. Data models pose a particular problem, because it is not clear what a data model interpreter would do, given that data is generally considered to be passive. We show how a data model interpreter can be defined in an object-oriented style as a dynamic message-processing function. Partial evaluation can then be applied to this data model interpreter to create a static dispatch function, analogous to a normal static class definition. We also consider the case of user interface model interpreters, and show that partial evaluation and deforestation can produce good specialized code. The user interface interpreter illustrates a solution to integrating two modeling languages. The system described here is bootstrapped from Scheme, although the goal is to build a complete software development environment based on model interpreters.
    • Bagahk: Developing Sound and Complete Decision Procedures in Coq
    • Benjamin Delaware
    • Master's Thesis, Washington University in St. Louis. August, 2007.
    • Show Abstract
    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.