Presentation Schedule

Foundational Proof Checkers with Small Witnesses by Dinghao Wu, Andrew W. Appel, and Aaron Stump PPDP 2003 Presented by Stephen on 2005-03-16 document (pdf) slides (ppt)

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules by Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers POPL 2005 Presented by Paul on 2005-03-09 document (pdf) slides (ppt)

From Max-SAT to Min-UNSAT: Insights and Applications by Mark H. Liffiton, Zaher S. Andraus, and Karem A. Sakallah Presented by Mark on 2005-02-23 document (pdf)

Precise Interprocedural Analysis using Random Interpretation by Sumit Gulwani and George Necula POPL 2005 Presented by Murtaza on 2005-02-09 document (pdf) slides (ppt)

Dynamic Partial-Order Reduction for Model Checking Software by Cormac Flanagan and Patrice Godefroid POPL 2005 Presented by Paul on 2005-02-02 document (ps) slides (ppt)

Predicate Abstraction of Ansi-C Programs using SAT by Edmund Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav FMSD 2004 Presented by Zaher on 2005-01-26 document (pdf) slides (ppt)

Scalable Error Detection using Boolean Satisfiability by Yichen Xie and Alex Aiken POPL 2005 Presented by Paul on 2005-01-19 document (pdf) slides (ppt)

Review Session Presented by Paul on 2004-12-15 slides (ppt)

Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking by Edmund Clarke, Daniel Kroening, and Karen Yorav DAC 2003 Presented by Paul on 2004-11-17 document (pdf) slides (ppt) long version (pdf)

Explaining Abstract Counterexamples by Sagar Chaki, Alex Groce, and Ofer Strichman FSE 2004 Presented by Mark on 2004-11-03 document (pdf)

Symbolic Simulation with Approximate Values by Chris Wilson, David L. Dill, and Randal E. Bryant FMCAD 2000 Presented by Ilya on 2004-10-27 document (ps) slides (ppt)

Reliable Verification Using Simulation with Scalar Values by Chris Wilson and David L. Dill DAC 2000 Presented by Smitha on 2004-10-20 document (pdf) slides (ppt) acm portal

Generalized Symbolic Execution for Model Checking and Testing by Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser TACAS 2003 Presented by Pratibha on 2004-10-13 document (pdf)

Symbolic Pointer Analysis by Jianwen Zhu ICCAD 2002 Presented by Stephen on 2004-07-28 document (pdf) slides (pdf) acm portal

Points-to Analysis using BDDs by Marc Berndl, Ondrej Lhotak, Feng Qian, Laurie Hendren, and Navindra Umanee PLDI 2003 Presented by Mark on 2004-07-21 document (pdf) slides (pdf) acm portal

Industrial Experience with Test Generation Languages for Processor Verification by Michael Behm, John Ludden, Yossi Lichtenstein, Michal Rimon, Michael Vinov DAC 2004 Presented by Ilya on 2004-07-14 document (pdf) slides (ppt) acm portal

Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams by John Whaley and Monica S. Lam PLDI 2004 (Best Paper) Presented by Paul on 2004-07-07 document (pdf) slides (ppt) acm portal

A Static Analyzer for Large Safety-Critical Software by Patrick Cousot et al PLDI 2003 Presented by Chandra on 2004-06-30 document (pdf) acm portal citeseer