Past Projects

Banshee: A toolkit for building constraint-based analyses. Banshee is a toolkit that simplifies the task of building constraint-based program analyses. Program analyses are widely used in compilers and software engineering tools for discovering or verifying specific properties of software systems, such as type safety and opportunities for program optimization. To use Banshee, the analysis designer provides a short specification file describing the kinds of constraints used in the analysis. From this specification, Banshee builds a customized constraint resolution engine which solves those constraints very efficiently. Banshee also builds a customized interface for that engine which is easy to use.
Blast: Berkeley Lazy Abstraction Software Verification Toolkit. Blast verifies and certifies temporal safety properties of C progams by model-checking a lazily-refined conservative abstraction of the program.

[HJMS02]	Lazy Abstraction [ ps ] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre. ACM Symposium on Principles of Programming Languages (POPL 2002).
[HJMGWS02]	Temporal-safety Proofs for Systems Code [ ps ] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George Necula, Westley Weimer, Gregoire Sutre. Proceedings of the 14th Conference on Computer-Aided Verification (CAV 2002).
[HJMQ03]	Thread-modular Abstraction Refinement [ ps/pdf ] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Proceedings of the 15th International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science, Springer-Verlag, 2003.
[HJMM04]	Abstractions from Proofs [ ps/pdf ] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. ACM Principles of Programming Languages (POPL 2004).
[BCHJM04]	Generating Tests from Counterexamples [ ps/pdf ] Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. ACM/IEEE International Conference on Software Engineering (ICSE 2004).
[HJM04]	Race Checking by Context Inference [ ps/pdf ] Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. ACM Programming Language Design and Implementation (PLDI 2004).

Build Interceptor captures the .i files of any project while it is built from source using the gcc toolchain, a necessary first step for most static analyses. No modifications are required to the build process of the project you are trying to capture.
CCured. CCured is a source-to-source translator for C, which instruments the source C code with runtime checks to catch memory safety violations at run time. As a novel enhancement, the system infers when some (or all!) of the checks can be safely omitted.



[NMW02]	CCured: Type-Safe Retrofitting of Legacy Code [ ps ] George C. Necula, Scott McPeak, Westley Weimer. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL02), pp. 128-139, Oregon, January 2002.
[CHMNW03]	CCured In The Real World [ pdf ] Jeremy Condit, Matthew Harren, George C. Necula, Scott McPeak, Westley Weimer. In Proceedings of the Programming Language Design and Implementation(PLDI03), pp. 232-244, California, June 2003.
[NCHMW05]	CCured: Type-Safe Retrofitting of Legacy Software. [ pdf ] George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley Weimer. ACM Transactions on Programming Languages and Systems (TOPLAS). To appear circa 2005.

Certified compilers

[Chl07] A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language [ abstract/ps/pdf ] Adam Chlipala. Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI'07).

Chic. Chic is a modular verifier for behavioral compatibility of software and hardware components. The goal of Chic is to be able to check that the interfaces for software or hardware components provide guarantees that satisfy the assumptions they make about each other. Chic supports a variety of interface property specification formalisms. The algorithms implemented in Chic version 1.0 are described below.

[dAH01a]	Interface automata [ ps | pdf ] Luca de Alfaro and Thomas A. Henzinger. Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE), ACM Press, 2001, pp. 109-120.
[dAH01b]	Interface theories for component-based design [ ps | pdf ] Luca de Alfaro and Thomas A. Henzinger. Proceedings of the First International Workshop on Embedded Software (EMSOFT), Lecture Notes in Computer Science 2211, Springer-Verlag, 2001, pp. 148-165.
[CdAHJM02]	Interface compatibility checking for software module [ ps | pdf ] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, and Freddy Y. C. Mang. Proceedings of the 14th International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 2404, Springer-Verlag, 2002, pp. 428-441.
[CdAHM02]	Synchronous and bidirectional component interfaces [ ps | pdf ] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Freddy Y. C. Mang. Proceedings of the 14th International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 2404, Springer-Verlag, 2002, pp. 414-427.

Cil: An Infrastructure for C Progam Analysis and Transformation. Cil (C Intermediate Language) is a high-level representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs.

[NMRW02]	Cil: Intermediate Language and Tools for Analysis and Transformation of C Programs [ ps ] George C. Necula, Scott McPeak, S. P. Rahul, Westley Weimer. International Conference on Compiler Construction (CC02), pp. 213-228, Grenoble, France, April 2002. (CC02 PPT presentation available)

Computer proof assistants

[CN06] Cooperative Integration of an Interactive Proof Assistant and an Automated Prover [ abstract/ps/pdf ] Adam Chlipala, George C. Necula. Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES'06).

The Cooperative Bug Isolation Project develops strategies for finding and fixing bugs in widely deployed software by using real data collected from real user runs. Statistical debugging combines techniques from program analysis and machine learning to identify anomalous program behavior that leads to application failure.



[LAZJ03a]	Sampling User Executions for Bug Isolation [ pdf | ps | bib ] Ben Liblit, Alex Aiken, Alice X. Zheng, and Michael I. Jordan. In First International Workshop on Remote Analysis and Measurement of Software Systems (RAMSS 2003). Portland, Oregon. May, 2003.
[LAZJ03b]	Bug Isolation via Remote Program Sampling [ pdf | ps | bib ] Ben Liblit, Alex Aiken, Alice X. Zheng, and Michael I. Jordan. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003). San Diego, California. June, 2003.
[LAZJ04]	Public Deployment of Cooperative Bug Isolation [ pdf | ps | bib ] Ben Liblit, Mayur Naik, Alice X. Zheng, Alex Aiken, and Michael I. Jordan. In Second International Workshop on Remote Analysis and Measurement of Software Systems (RAMSS 2004), Edinburgh, Scotland. May 2004.
[ZJLA03]	Statistical Debugging of Sampled Programs [ pdf | ps | bib ] Alice X. Zheng, Michael I. Jordan, Ben Liblit, and Alex Aiken. In Seventeenth Annual Conference on Neural Information Processing Systems (NIPS 2003). Vancouver and Whistler, British Columbia, Canada. December, 2003.




Cqual: A tool for adding type qualifiers to C. Cqual is a type-based analysis tool that provides a lightweight, practical mechanism for specifying and checking properties of C programs. Cqual extends the type system of C with extra user-defined type qualifiers. The programmer adds type qualifier annotations to their program in a few key places, and Cqual performs qualifier inference to check whether the annotations are correct. The analysis results are presented with a user interface that lets the programmer browse the inferred qualifiers and their flow paths. A C++ version of Cqual is available as part of the Oink project.

[FTA02]	Flow-Sensitive Type Qualifiers [ pdf | ps | ps.gz ] Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Draft, November 2001. Accepted for publication in PLDI 2002.
[FA01]	Checking Programmer-Specified Non-Aliasing [ ps | ps.gz ] Jeffrey S. Foster and Alex Aiken. Computer Science Division Tech Report UCB//CSD-01-1160. University of California, Berkeley. October 2001.
[STFW01]	Detecting Format-String Vulnerabilities with Type Qualifiers [ pdf | ps | ps.gz ] Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. In 10th USENIX Security Symposium, August 2001.
[FFA99]	A Theory of Type Qualifiers [ pdf | ps | ps.gz ] Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'99). Atlanta, Georgia. May 1999.

Delta: a testcase minimizer. Delta assists you in minimizing "interesting" files subject to a test of their interestingness. A common such situation is when attempting to isolate a small failure-inducing substring of a large input that causes your program to exhibit a bug. Our implementation is based on the algorithm of the Delta Debugging project at Saarland University.
Elkhound is a parser generator that uses a Generalized LR (GLR) parsing algorithm. GLR works with any context-free grammar, whereas LR parsers (such as Bison) require grammars to be LALR(1).

Parsing with arbitrary context-free grammars has two key advantages: (1) unbounded lookahead, and (2) support for ambiguous grammars. Unbounded lookahead is achieved by allowing multiple potential parses to coexist for as long as necessary. Similarly, ambiguity is handled by letting potential parses be coalesced, with special action taken to handle the ambiguous region of the input. In general, by using the GLR algorithm, Elkhound avoids the difficulty of trying to make a language grammar fit the LALR(1) restrictions.

What's more, the Elkhound implementation of GLR is competitive with good LR implementations (particularly Bison) for grammars and grammar fragments that are LALR(1). Its high performance is a result of a novel combination of GLR and LR parsing, wherein the parser decides on a token-by-token basis which algorithm to use. Programmers can start with a grammar that is convenient (but perhaps slower to parse with), and gradually modify it to conform to LALR(1) in places for improved performance. Grammars that are already LALR(1) will work in Elkhound unmodified (though the input syntax is different), and with parsing speeds within a few percent of Bison-generated parsers.


Elsa is a C/C++ parser implemented with Elkhound that can successfully parse much of the C++ code "in the wild."

Oink is a collection of composable backends for the Elsa C and C++ frontend. Oink aims to be industrial-strength for immediate utility in finding bugs, extensible for ease in adding backends, and composable for ease in combining existing backends. It computes both expression-level and type-level dataflow, and statement-level intra-procedural controlflow [by delegating to Elsa]. Oink also comes with a client of the dataflow analysis that does type qualifier inference: Cqual++, a C/C++ frontend for Cqual. Whole-program analyses may be attempted using the linker imitator.

The Open Verifier project

A re-invisioning of proof-carrying code with a focus on verification-time performance. We study general verifiers rather than individual proofs about untrusted programs, considering special architectures for interaction with proof-generating verifiers and, in the latest work, actually proving the correctness of verifiers written in general-purpose programming languages.

[SN02] A Gradual Approach to a More Trustworthy, yet Scalable, Proof-Carrying Code [ pdf ] Robert R. Schneck, George C. Necula. Proceedings of the Conference on Automated Deduction (CADE'02). [NS02] Proof-Carrying Code with Untrusted Proof Rules [ pdf ] George C. Necula, Robert R. Schneck. Proceedings of the 2nd International Software Security Symposium (ISSS'02). [SN03] A Sound Framework for Untrustred Verification-Condition Generators [ pdf ] Robert R. Schneck, George C. Necula. Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03). [CCNR05a] The Open Verifier Framework for Foundational Verifiers [ abstract/ps/pdf ] Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). [CCNR05b] Type-Based Verification of Assembly Language for Compiler Debugging [ abstract/ps/pdf ] Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). [CCN06] A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety [ abstract/ps/pdf ] Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula. Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'06). [Chl06] Modular Development of Certified Program Verifiers with a Proof Assistant [ abstract/ps/pdf ] Adam Chlipala. Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP'06).

Rc: a dialect of C that adds safe, region-based memory management to C. Region-based memory management allocates objects in a program-specified region. Objects cannot be freed individually; instead regions are deleted with all their contained objects. Region-based memory management is a fairly common programming style, for instance it is used in the Apache web server (where the regions are called pools and also used to manage other resources).

[GA01]	Language Support for Regions [ ps ] David Gay and Alex Aiken, ACM SIGPLAN '01 Conference on Programming Language Design and Implementation, Snowbird, Utah, June 2001.
[GA98]	Memory Management with Explicit Regions [ ps ] David Gay and Alex Aiken, ACM SIGPLAN '98 Conference on Programming Language Design and Implementation, Montreal, Canada, June 1998.

Page maintained by Joel Galenson.