Papers

123
Foundational Proof Checkers with Small Witnesses by Dinghao Wu, Andrew W. Appel, and Aaron Stump PPDP 2003 document (pdf) slides (ppt)
122
Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules by Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers POPL 2005 document (pdf) slides (ppt)
121
From Max-SAT to Min-UNSAT: Insights and Applications by Mark H. Liffiton, Zaher S. Andraus, and Karem A. Sakallah document (pdf)
120
Discovery of Minimal Unsatisfiable Subsets of Constraints Using Hitting Set Dualization by James Bailey and Peter J. Stuckey PADL 2005 document (pdf)
119
Precise Interprocedural Analysis using Random Interpretation by Sumit Gulwani and George Necula POPL 2005 document (pdf) slides (ppt)
118
Discovering Affine Equalities using Random Interpretation by Sumit Gulwani and George Necula POPL 2003 document (pdf) slides (ppt)
117
Dynamic Partial-Order Reduction for Model Checking Software by Cormac Flanagan and Patrice Godefroid POPL 2005 document (ps) slides (ppt)
116
Downgrading Policies and Relaxed Noninterference by Peng Li and Steve Zdancewic POPL 2005 document (pdf) slides (pdf)
115
Predicate Abstraction of Ansi-C Programs using SAT by Edmund Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav FMSD 2004 document (pdf) slides (ppt)
114
Modular Verification of Software Components in C by Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith ICSE 2003 document (pdf)
113
Scalable Error Detection using Boolean Satisfiability by Yichen Xie and Alex Aiken POPL 2005 document (pdf) slides (ppt)
112
Review Session slides (ppt)
111
Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking by Edmund Clarke, Daniel Kroening, and Karen Yorav DAC 2003 document (pdf) slides (ppt) long version (pdf)
110
Explaining Abstract Counterexamples by Sagar Chaki, Alex Groce, and Ofer Strichman FSE 2004 document (pdf)
109
Symbolic Simulation with Approximate Values by Chris Wilson, David L. Dill, and Randal E. Bryant FMCAD 2000 document (ps) slides (ppt)
108
Reliable Verification Using Simulation with Scalar Values by Chris Wilson and David L. Dill DAC 2000 document (pdf) slides (ppt) acm portal
107
Generalized Symbolic Execution for Model Checking and Testing by Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser TACAS 2003 document (pdf)
106
Finding and Preventing Run-Time Error Handling Mistakes by Westley Weimer and George C. Necula OOPSLA 2004 document (pdf)
105
Which Pointer Analysis Should I Use? by Michael Hind and Anthony Pioli ISSTA 2000 document (pdf) acm portal
104
Points-to Analysis using BDDs by Marc Berndl, Ondrej Lhotak, Feng Qian, Laurie Hendren, and Navindra Umanee PLDI 2003 document (pdf) slides (pdf) acm portal
103
Industrial Experience with Test Generation Languages for Processor Verification by Michael Behm, John Ludden, Yossi Lichtenstein, Michal Rimon, Michael Vinov DAC 2004 document (pdf) slides (ppt) acm portal
102
Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams by John Whaley and Monica S. Lam PLDI 2004 (Best Paper) document (pdf) slides (ppt) acm portal
101
A Static Analyzer for Large Safety-Critical Software by Patrick Cousot et al PLDI 2003 document (pdf) acm portal citeseer
100
Reduction: A Method of Proving Properties of Parallel Programs by Richard J. Lipton Communications of the ACM, Vol. 18, No. 12 (1975) document (pdf)
99
A Type and Effect System for Atomicity by Cormac Flanagan and Shaz Qadeer PLDI 2003 document (pdf)
98
Types for Atomicity by Cormac Flanagan, Shaz Qadeer TLDI 2003 document (ps)
97
ABCD: Eliminating Array Bounds Checks on Demand by R. Bodik, R. Gupta, and V. Sarkar PLDI 2000 document (pdf)
96
Ownership Types for Safe Region-Based Memory Management in Real-Time Java by Chandrasekhar Boyapati PLDI 2003 document (pdf)
95
Address Obfsucation: an Efficient Approach to Combat a Broad Range of Memory Error Exploits by Sandeep Bhatkarm, Daniel C. DuVarney, and R. Sekar USENIX Security 2003 document (pdf)
94
PointGuard: Protecting Pointers From Buffer Overflow Vulnerabilities by Crsipin Cowan, Steve Beattie, John Johansen, and Perry Wagle USENIX Security 2003 document (pdf)
93
Some lessons from using static analysis and software model checking by Madanlal Musuvathi and Dawson Engler SoftMC 2003 document (pdf)
92
ARCHER: Using Symbolic, Path-sensitive Analysis to Detect Memory Access Errors by Yichen Xie, Andy Chou, and Dawson Engler FSE 2003 document (pdf)
91
Deriving a Simulation Input Generator and a Coverage Metric From a Formal Specification by Kanna Shimizu, David Dill DAC 2002 document (pdf)
90
Adoption and Focus: Practical Linear Types for Imperative Programming by Manuel Fahndrich, Robert DeLine PLDI 2002 document (pdf)
89
ESP: Path-Sensitive Program Verification in Polynomial Time by Das, Lerner, Seigle PLDI 2002 document (pdf)
88
CSSV: Towards a Realistic Tool for Statically Detecting All Buffer Overflows in C by Dor N., Rodeh M., and Sagiv M. PLDI 2003 document (pdf)
87
CCured in the Real World by Jeremy Condit, Matthew Harren, Scott McPeak, George C. Necula, Westley Weimer PLDI 2003 document (pdf)
86
Model Checking the Garbage Collection Mechanism of SMV by Cindy Eisner document (pdf)
85
Successive Approximation of Abstract Transition Relations by Satyaki Das, David L. Dill IEEE Symposium on Logic in Computer Science 2001 document (pdf)
84
Counter-Example Based Predicate Discovery in Predicate Abstraction by Satyaki Das, David L. Dill FMCAD 2002 document (pdf)
83
CMC: A Pragmatic Approach to Model Checking Real Code by Madanlal Musuvathi, David Y.W. Park, Andy Chou, Dawson R. Engler, David L. Dill OSDI 2002 document (pdf)
82
A Comparison of Publicly Available Tools for Dynamic Buffer Overflow Prevention by John Wilander and Mariam Kamkar NDSS 2003 document (pdf)
81
Testing C Programs for Buffer Overflow Vulnerabilities by Eric Haugh and Matt Bishop NDSS 2003 document (pdf)
80
Korat: Automated Testing Based on Java Predicates by Chandrasekhar Boyapati, Sarfraz Khurshid, Darko Marinov ACM International Symposium on Software Testing and Analysis (ISSTA), Rome, Italy, July 2002 document (pdf)
79
A BDD-based Model Checker for Recursive Programs by Javier Esparza, Stefan Schwoon Lecture Notes in Computer Science (2001) document (ps)
78
MOPS: an Infrastructure for Examining Security Properties of Software by Hao Chen and David Wagner ACM CCS 2002 document (pdf)
77
Type-Assisted Dynamic Buffer Overflow Detection by Kyung-suk Lhee and Steve J. Chapin USENIX Security '02 document (ps)
76
A Structural Approach to Operational Semantics by G. D. Plotkin document (ps)
75
CCured: Type-Safe Retrofitting of Legacy Code by George C. Necula, Scott McPeak, and Westley Weimer POPL 2002 document (pdf)
74
Dynamic Detection of Improperly Bounded Program Inputs by Eric Larson and Todd Austin document (pdf)
73
Symbolic Pointer Analysis by Jianwen Zhu ICCAD 2002 document (pdf) slides (pdf) acm portal
72
Putting Pointer Analysis to Work by Rakesh Ghiya and Laurie J. Hendren POPL 1998 document (ps)
71
Pointer Analysis: Haven't We Solved This Problem Yet? by Michael Hind PASTE 2001 document (pdf) slides (pdf)
70
MaC: A Framework for Run-time Correctness Assurance of Real-Time Systems by M. Kim, M. Viswanathan, H. Ben-Abdallah, S. Kannan, I. Lee, and O. Sokolsky 1999 document (pdf)
69
Automatic Generation of Program Specifications by Jeremy W. Nimmer and Michael D. Ernst ISSTA 2002 document (pdf)
68
A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities by David Wagner, Jeffrey S. Foster, Eric A. Brewer, and Alexander Aiken NDSS 2000 document (pdf)
67
Parametric shape analysis via 3-valued logic by Mooly Sagiv, Thomas Reps, Reinhard Wilhelm POPL 1999 document (pdf)
66
Modular Interprocedural Pointer Analysis Using Access Paths: Design, Implementation, and Evaluation by Ben-Chung Cheng and Wen-mei W. Hwu PLDI 2000 document (pdf)
65
Interprocedutal May-Alias Analysis for Pointers: Beyond k-limiting by Alain Deutsch PLDI 1994 document (pdf)
64
Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions by Radu Rugima and Martin Rinard PLDI 2000 document (pdf)
63
Solving Shape-Analysis Problems in Languages with Destructive Updating by Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm POPL 1996 document (pdf)
62
Shape Analysis as a Generalized Path Problem by Thomas Reps PEPM 1995 document (pdf)
61
Is it a Tree, a DAG, or a Cyclic Graph? by Rakesh Ghiya and Laurie J. Hendren POPL 1996 document (pdf)
60
Connection Analysis: A Pratical Interprocedural Heap Analysis for C by Rakesh Ghiya and Laurie J. Hendren LCPC 1995 document (pdf)
59
Unification-based Pointer Analysis with Directional Assignments by Manuvir Das document (pdf)
58
Program Slicing Using Dynamic Points-to Data by Darren Atkinson, Markus Mock, Craig Chambers, Susan J. Eggers document (pdf)
57
Points-to Analysis in Almost Linear Time by Bjarne Steensgaard document (pdf)
56
Pointer Analysis for Multithreaded Programs by Radu Regina, Martin Rinard document (pdf)
55
Demand-Driven Pointer Analysis by Nevin Heintze, Olivier Tardieu document (pdf)
54
Fast and Accurate Flow-Insensitive Points-To Analysis by Marc Shapiro, Susan Horwitz document (pdf)
53
Automatic Predicate Abstraction of C Programs by Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani document (pdf)
52
ESP: Path-Sensitive Program Verification in Polynomial Time by Manuvir Das, Sorin Lerner, and Mark Seigle PLDI 2002 document (pdf)
51
A System and Language for Building System-Specific, Static Analyses by Seth Hallem, Benjamin Chelf, Yichen Xie, and Dawson Engler PLDI 2002 document (ps)
49
A Survey of Authentication Protocol Literature by John Clark and Jeremy Jacob document (pdf) slides (ppt)
48
FLAVERS: A Finite State Verification Technique for Software Systems by Cobleigh, Clarke, Osterweil IBM Systems Journal Vol. 41, No. 1, 2002 document (pdf)
46
The Stanford Temporal Prover (STeP) Stanford University link
45
Java PathFinder NASA link
44
InVeSt (Invariants Verification System) University of Kiel link
43
The FeaVer Feature Verification System by Bell Laboratories link
42
Bandera: Software Model Construction for Finite-state Verification Kansas State University link
41
The aSpin Project Universitas Malacitana link
40
On-The-Fly, LTL Model Checking with SPIN Bell Labs link
39
Improving Computer Security using Extended Static Checking by Brian V. Chess document (pdf)
38
Using Programmer-Written Compiler Extensions to Catch Security Holes by Ken Ashcraft and Dawson Engler 2002 IEEE Symposium on Security and Privacy (to appear) document (pdf)
37
Ken Thompson's Turing Award Speech by Ken Thompson Communication of the ACM link
36
Wisconsin Program-Slicing Project link
35
Sofwtare Verification and Validation with Destiny: A parallel approach to automated theorem proving by Josiah Dykstra Crossroads: ACM Student Magazine, January 2002. document (pdf)
34
Statically Detecting Likely Buffer Overflow Vulnerabilities by David Larochelle, David Evans 2001 USENIX Security Symposium document (pdf)
33
Security Flaws link link link
32
Infrastructure for Correctness Tools by John Pincus UW-Microsoft Summer Institute, May 2000 slides (ppt)
31
Aspect: An Economical Bug-Detector by Daniel Jackson IEEE document (ps)
30
Validation of Optimizing Compilers by L. Zuck, A. Pnueli and R. Leviathan document (ps)
29
Software Model Checking by Gerard J. Holzmann Marktoberdorf Lecture Notes, August 2000 document (pdf)
28
Efficient Software-Based Fault Isolation by Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. SOSP 1993 document (pdf)
27
Enforcing High-Level Protocols in Low-Level Software by Robert DeLine and Manuel Fahndrich (Microsoft Research) PLDI 2001 document (pdf)
26
Lazy Abstraction by Thomas A. Henzinger Ranjit Jhala Rupak Majumdar Gregoire Sutre POPL 2002 document (ps)
25
Predicate Abstraction for Software Verification by Cormac Flanagan and Shaz Qadeer POPL 2002 document (ps)
24
Proving Correctness of Compiler Optimizations by Temporal Logic by David Lacey Neil D. Jones Eric Van Wyk Carl Christian Frederiksen POPL 2002 document (pdf)
23
Some of the Theory Behind LEDA by Kurt Mehlhorn, Stefan Naher, Christian Uhrig document (pdf)
22
SWERVE Summary - Jan. 30 by Brian Sierawski document (doc)
20
An Axiomatic Basis for Computer Programming by C. A. R. Hoare The Queens University of Belfast, Communications of the ACM, vol. 12 (10), 1969 document (pdf)
19
Extended Static Checking by David Detlefs, K Leino, Greg Nelson, and James Saxe Compaq, Systems Research Center, 1998 document (pdf)
18
Bebop: A Symbolic Model Checker for Boolean Programs by Thomas Ball and Sriram K. Rajamani SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, August/September 2000, pp. 113-130 document (pdf)
17
The SLAM Project: Debugging System Software via Static Analysis by Thomas Ball and Sriram K. Rajamani POPL 2000 document (pdf)
16
A Universal Dynamic Trace for Linux and other Operating Systems by Richard Moore UKUUG Linux Developers Conference 2001 document (pdf)
15
Alloy: A Lightweight Object Modelling Notation by Daniel Jackson July 2000 document (pdf)
14
Alcoa: the Alloy Constraint Analyzer by Daniel Jackson, Ian Schechter and Ilya Shlyakhter Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000 document (pdf)
13
Finding Bugs with a Constraint Solver by Daniel Jackson and Mandana Vaziri International Symposium on Software Testing and Analysis, Portland, OR, August 2000 document (pdf)
12
Applying the Cogito Program Development Environment to Real-Time System Design by C. J. Fidge, P. Kearney and A. P. Martin Technical report 97-36, Software Verification Research Centre, 1997 document (pdf)
11
Why effective proof tool support for Z is hard by Andrew Martin Technical report 97-34, Software Verification Research Centre, 1997 document (pdf)
10
A Tactic Language for Ergo by A. Martin, R. Nickson and M. Utting Technical report 97-16, Software Verification Research Centre, 1997 document (pdf)
9
Improving Angel's Parallel Operator: Gumtree's Approach by Andrew Martin, Ray Nickson and Mark Utting Technical report 97-15, Software Verification Research Centre, 1997 document (pdf)
8
A Revised Logic for Standard Z by A. Martin Technical report 98-21, Software Verification Research Centre, 1998 document (pdf)
7
A set-theoretic model for real-time specification and reasoning by C. J. Fidge, I. J. Hayes, A. P. Martin and A. K. Wabenhorst Technical report 98-07, Software Verification Research Centre, 1999 document (pdf)
6
Lifting in Z by Andrew Martin and Colin Fidge Technical report 98-06, Software Verification Research Centre, 2000 document (pdf)
5
Model Checking Large Software Specifications by William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon D. Reese In IEEE Transactions on Software Engineering 24(7), July 1998 document (pdf)
4
A static analyzer for finding dynamic programming errors by William R. Bush, Jonathan D. Pincus, David J. Sielaff Journal of Software Practice and Engineering, June 2000 document (pdf)
3
A Simple Method for Extracting Models from Protocol Code by David Lie, Andy Chou, Dawson Engler, and David Dill ISCA 2001 document (pdf)
2
Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions by Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Best Paper at OSDI 2000 document (pdf)
1
Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code by Dawson Engler, David Yu Chen, Seth Hallem, Andy Chou, and Benjamin Chelf SOSP 2001 document (pdf)