Inexpensive Program Analysis
at the University of Virginia
If you want a guarantee, buy a toaster.
Clint Eastwood (The Rookie, 1990)
Courses - Funding - Papers - People - Software - Talks
Research SummaryDespite considerable progress in program analysis tools, typical software development processes make little use of advanced analysis techniques, even when they are producing mission critical software. Our group is exploring analysis approaches that combine dynamic and static analysis techniques.
We co-organized the Workshop on Dynamic Analysis (25 May 2004, colocated with ICSE).
SoftwareSplintSplint is a tool for statically checking C programs for security vulnerabilities and coding mistakes. With minimal effort, Splint can be used as a better lint. If additional effort is invested adding annotations to programs, Splint can perform stronger checking than can be done by any standard lint.PerracottaPerracotta is a dynamic analysis tool for automatically inferring temporal properties of a target program. It takes the program's execution traces as input and outputs a set of likely temporal properties. The properties can enhance program understanding, be used to aid program evolution, or be used as input properties for a model checker.
CoursesCS201J: Engineering Software, Fall 2003
CS201J: Engineering Software, Fall 2002CS201J is an introductory software engineering (CS2) course focused on teaching students to produce dependable and secure software. It uses lightweight analysis tools (primarily ESC/Java) throughout the course.
Selected PapersSee http://www.cs.virginia.edu/evans/pubs/ for full publications listJinlin Yang, David Evans, Deepali Bhardwaj, Thirumalesh Bhat, Manuvir Das. Perracotta: Mining Temporal API Rules From Imperfect Traces. 28th International Conference in Software Engineering, Research Track, Shanghai, China, May 2006.
David Evans and Michael Peck. Inculcating Invariants in Introductory Courses. 28th International Conference in Software Engineering, Education Track, Shanghai, China, May 2006.
David Evans. Toasters, Seat Belts, and Inferring Program Properties . IFIP Working Conference on Verified Software: Theories, Tools, Experiments. Zürich, Switzerland. 10-13 October 2005. (PDF, 8 pages)
Jinlin Yang and David Evans. Automatically Inferring Temporal Properties for Program Evolution. Fifteenth IEEE International Symposium on Software Reliability Engineering (ISSRE 2004). Saint-Malo, France. 2-5 November 2004. (PDF, 12 pages)
Jinlin Yang and David Evans. Dynamically Inferring Temporal Properties. ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004). 7-8 June 2004. (PDF, 6 pages)
Michael Peck. Improving the Usability of the ESC/Java Static Analysis Tool. University of Virginia Fourth Year Thesis. 25 March 2004. (PDF, 26 pages)
Joel Winstead and David Evans. Towards Differential Program Analysis. Workshop on Dynamic Analysis. 9 May 2003. (PDF, 4 pages)
David Evans and David Larochelle. Improving Security Using Extensible Lightweight Static Analysis. IEEE Software, Jan/Feb 2002. (PDF, 10 pages) (CiteSeer Page, 16 citations)
David Larochelle and David Evans. Statically Detecting Likely Buffer Overflow Vulnerabilities. USENIX Security Symposium 2001. [PDF] (CiteSeer Page, 25 citations)
David Evans. Static Detection of Dynamic Memory Errors. SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), May 1996. [PDF] (CiteSeer Page, 79 citations)
David Evans, John Guttag, Jim Horning and Yang Meng Tan. LCLint: A Tool for Using Specifications to Check Code. SIGSOFT Symposium on the Foundations of Software Engineering, December 1994. [PDF] (55 citations, CiteSeer Page)
See http://www.splint.org/pubs/ for more publications about Splint and LCLint. See http://www.cs.virginia.edu/evans/pubs/ for more papers by David Evans.
TalksAutomatically Inferring Temporal Properties for Program Evolution [PPT] (Jinlin Yang and David Evans). Conference talk at 15th IEEE International Symposium on Software Reliability Engineering (ISSRE 2004). 5 November 2004.
Dynamically Inferring Temporal Properties for Daisy [PPT] (Jinlin Yang). Technical talk at the Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software. July 14, 2004.
Dynamically Inferring Temporal Properties [PPT] (Jinlin Yang). Technical talk at ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004). 7 June 2004.
Finding Security Vulnerabilities Before Evildoers Do [SXI (OpenOffice), PPT] (David Evans). Invited talk at Conferencia Internacional de Software Libre, Malaga, Spain, 20 February 2004.
Statically Detecting Likely Buffer Overflow Vulnerabilities (David Larochelle) [PPT] [PDF]. USENIX Security '01 for Statically Detecting Likely Buffer Overflow Vulnerabilities.
Extensible Lightweight Static Checking [PPT] [PDF] (David Evans). Short talk at University of Washington and Microsoft Research Summer Institute on Specifying and Checking Properties of Software, 14 August 2001.
Let's Stop Beating Dead Horses and Start Beating Trojan Horses [PPT] (David Evans). Short presentation in a debate on Proof-Carrying Code with Peter Lee at the Infosec Research Council, Malicious Code Study Group. San Antonio, 13 January 2000.
Systems for Safety and Dependability [PPT] (David Evans). Invited seminar at Reliable Software Technologies. Sterling, VA, 14 December 1999.
PeopleProject Leader: David Evans
Current PhD Students
Current Undergraduate Students
David Larochelle (MCS 2001)
MCS Project: Statically Detecting Likely Buffer Overflow Vulnerabilities
Mike Peck (BS 2004) — graduate student at Johns Hopkins University
Thesis: Improving the Usability of the ESC/Java Static Analysis Tool
David Friedman (BS 2002) — graduate student at Johns Hopkins University
Thesis: Using Splint to Detect Buffer Overflow Vulnerabilities in Sendmail
Michael Lanouette (BS 2002)
Thesis: Static Checking of Coding Standards
Hien Phan (BS 2002)
Thesis: Developing a Web Interface for the LCLint Static Checker
Other LCLint and Splint Contributors
FundingOur research is partially supported by the National Science Foundation through
Previously, we have been supported by these grants:
CPA: Automatic Inference and Effective Use of Temporal Properties (Award 0541123), 2006-2008.
Previously, our work was funded by a grant from NASA and a USENIX Student Research Grant.
ITR: A Framework for Environment-Aware, Massively Distributed Computing (with Tarek Abdelzaher and David Brogan), 2001 - 2005.
CCLI: Teaching Software Engineering Using Lightweight Analysis, January 2002 - December 2003. (PDF, PS)
University of Virginia
Department of Computer Science
Inexpensive Program Analysis
|Sponsored by the National Science Foundation||