Affiliates Workshop: Satisfiability Solvers and Program Verification

August 10 - 11, 2006

Schedule

All times in this Schedule are Pacific Time (PT)

Thursday, August 10, 2006

Morning Session

9:45 - 10:30
Edmund M. Clarke (Carnegie-Mellon University)

Bounded and Unbounded Model Checking using SAT
Presentation (PowerPoint File)

10:30 - 11:00 Break
11:00 - 11:45
Ken McMillan (Berkeley College of Engineering)

SAT, Interpolants, and Software Model Checking
Presentation (PowerPoint File)

11:45 - 12:30
Shuvendu Lahiri (Carnegie-Mellon University)

Efficient SAT-based Techniques for Predicate Abstraction
Presentation (PowerPoint File)

12:30 - 2:00 Lunch (on your own)

Afternoon Session

2:00 - 2:45
Carla Gomes (Cornell University)

Beyond Satisfiability: Model Counting, Quantification, and Randomization
Presentation (PowerPoint File)

2:45 - 3:30
Daniel Kroening (Eidgenössische TH Zürich-Zentrum)

SAT-based methods for proving properties in Reynolds/O'Hearn Separation Logic
Presentation (PowerPoint File)

3:30 - 4:00 Break
4:00 - 4:45
Alex Aiken (Stanford University)

Scalable Program Analysis Using Boolean Satisfiability
PDF Presentation


Friday, August 11, 2006

Morning Session

9:45 - 10:30
Orna Grumberg (Technion - Israel Institute of Technology)

Hybrid BDD and All-SAT Method for Model Checking
Presentation (PowerPoint File)

10:30 - 11:00 Break
11:00 - 11:45
Aarti Gupta (NEC Research Institute)

Verifying C Programs using SAT-based model checking
PDF Presentation

11:45 - 12:30
Ofer Strichman (Technion - Israel Institute of Technology)

Decision Heuristics based on an Abstraction/Refinement Model
Presentation (PowerPoint File)

12:30 - 2:00 Lunch (on your own)

Afternoon Session

2:00 - 2:45
Sharad Malik (Princeton University)

Optimization and Relaxation in SAT Search
Presentation (PowerPoint File)

2:45 - 3:30
Alessandro Cimatti (Istituto per la Ricerca Scientifica e Tecnologica (IRST))

Reasoning about Bit Vector Programs with Decision Procedures
Presentation (PowerPoint File)

3:30 - 4:00 Break
4:00 - 4:45
Robert Nieuwenhuis (Polytechnical University of Cataluña (Barcelona))

The New Architecture and Solvers in the Barcelogic Tool for SAT Modulo Theories
PDF Presentation