Adam Chlipala. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI'07). June 2007.
A compiler for a tiny statically-typed functional programming language, implemented in Coq with a proof of correctness. The main interesting bits are my use of dependently-typed abstract syntax and denotational semantics, along with some engineering tricks for making the task manageable.
Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP'06). September 2006.
I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. I take advantage of Coq's support for programming with dependent types and modules in the structure of my development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it's possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.
Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'06). January 2006.
We propose a new technique in support of the construction of efficient Foundational Proof-Carrying Code systems. Instead of suggesting that pieces of mobile code come with proofs of their safety, we instead suggest that they come with executable verifiers that can attest to their safety, as in our previous work on the Open Verifier. However, in constrast to that previous work, here we do away with any runtime proof generation by these verifiers. Instead, we require that the verifier itself is proved sound. To support this, we present a novel technique for extracting proof obligations about ML programs. Using this approach, we are able to demonstrate the first foundational verification technique for Typed Assembly Language with performance comparable to that of the traditional, uncertified TAL type checker.
Dirk Beyer, Adam J. Chlipala, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar. Generating Tests from Counterexamples. Proceedings of the 26th International Conference on Software Engineering (ICSE'04), IEEE Computer Society Press. May 2004.
We describe how to use the BLAST model checker to generate program test suites that achieve full coverage with respect to a given set of predicates.
Adam Chlipala. Modular Development of Certified Program Verifiers with a Proof Assistant. Journal of Functional Programming (JFP). Cambridge University Press. Accepted pending revision.
Extended version of my ICFP'06 paper
Adam Chlipala. Position Paper: Thoughts on Programming with Proof Assistants. Proceedings of the Programming Languages meets Program Verification Workshop (PLPV'06). August 2006.
Some thoughts on how Coq is actually in pretty good shape to use today for non-trivial programming with dependent types
Adam Chlipala, George C. Necula. Cooperative Integration of an Interactive Proof Assistant and an Automated Prover. Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES'06). August 2006.
We show how to combine the interactive proof assistant Coq and the Nelson-Oppen-style automated first-order theorem prover Kettle in a synergistic way. We do this with a Kettle tactic for Coq that uses theory-specific reasoning to simplify goals based on automatically chosen case analyses, returning to the user as subgoals the cases it couldn't prove automatically. The process can then be repeated recursively, using Coq's tactical language as a very expressive extension of the matching strategies found in provers like Simplify. We also discuss how to encode specialized first-order proofs efficiently in Coq using proof by reflection.
Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. The Open Verifier Framework for Foundational Verifiers. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). January 2005.
We propose a new framework for the construction of trustworthy program verifiers. The Open Verifier architecture can be viewed as an optimized Foundational Proof-Carrying Code toolkit. Instead of proposing that code producers send proofs of safety with all of their programs, we instead suggest that they send re-usable proof-generating verifiers. The proofs are generated in an online fashion via a novel interaction scheme between the untrusted verifier and the trusted core of the system.
Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. Type-Based Verification of Assembly Language for Compiler Debugging. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). January 2005.
A new approach to checking assembly programs in a way similar to that used in the Java Bytecode Verifier. We introduce a novel mixed type/value technique that makes it tractable to deal with some of the "dependent typing" issues that come up. We also present results on using this technique to help students in an undergraduate compilers class debug their class projects.
Adam Chlipala, Leaf Petersen, Robert Harper. Strict Bidirectional Type Checking. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). January 2005.
We present a type system that is useful in saving type annotation space in intermediate language terms expressed in the restricted form called "A-normal form" or "one-half CPS." Our approach imports ideas from strict logic, which is based on the idea of hypotheses that must be used at least once. The resulting system is relevant to the efficiency of type-preserving compilers.
Adam Chlipala. Developing Certified Program Verifiers with a Proof Assistant. Proceedings of the International Workshop on Proof-Carrying Code (PCC'06). August 2006.
A poster about certified program verifiers in Coq
Dirk Beyer, Adam J. Chlipala, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar. The Blast Query Language for Software Verification. Proceedings of the 11th Static Analysis Symposium (SAS'04), Lecture Notes in Computer Science 3148, Springer-Verlag. August 2004.
We describe a system that combines security automaton-based program specification with a facility for relational-style queries about the possible execution paths of a program.
Adam Chlipala. Generic Programming and Proving for Programming Language Metatheory. Technical Report UCB/EECS-2007-147. 2007.
How to do dependently-typed generation of proofs about programming language syntax and semantics
Adam Chlipala. Implementing Certified Programming Language Tools in Dependent Type Theory. Technical Report UCB/EECS-2007-113. 2007.
My PhD dissertation, re-presenting the work on certified program verifiers (from ICFP'06) and certified compilers (from PLDI'07)
Adam Chlipala. Scrap Your Web Application Boilerplate, or Metaprogramming with Row Types. Technical Report UCB/EECS-2006-120. 2006.
An overview of a work-in-progress functional programming language that puts dependent types and theorem proving to work to make it easier to write concise and maintainable web applications
Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. Technical Report UCB/ERL M05/32. UC Berkeley EECS Department. 2005.
This is an extended version of our VMCAI'06 paper, containing a formalization of our model extraction procedure and additional examples.
Adam Chlipala. An Untrusted Verifier for Typed Assembly Language. MS Project Report. Technical Report UCB/ERL M04/41. UC Berkeley EECS Department. 2004.
A summary of my experiences developing a proof-generating TAL type checker within the Open Verifier framework. In the style of Foundational PCC, the soundness of this verifier and the proofs it generates is based on no assumptions about the TAL type system. This was one of the first projects to consider the runtime performance of Foundational PCC-style verification.