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
|
10:30 - 11:00
|
Break
|
11:00 - 11:45
|
Ken McMillan (Berkeley College of Engineering)
SAT, Interpolants, and Software Model Checking
|
11:45 - 12:30
|
Shuvendu Lahiri (Carnegie-Mellon University)
Efficient SAT-based Techniques for Predicate Abstraction
|
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
|
2:45 - 3:30
|
Daniel Kroening (Eidgenössische TH Zürich-Zentrum)
SAT-based methods for proving properties in Reynolds/O'Hearn Separation Logic
|
3:30 - 4:00
|
Break
|
4:00 - 4:45
|
Alex Aiken (Stanford University)
Scalable Program Analysis Using Boolean Satisfiability
|
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
|
10:30 - 11:00
|
Break
|
11:00 - 11:45
|
Aarti Gupta (NEC Research Institute)
Verifying C Programs using SAT-based model checking
|
11:45 - 12:30
|
Ofer Strichman (Technion - Israel Institute of Technology)
Decision Heuristics based on an Abstraction/Refinement Model
|
12:30 - 2:00
|
Lunch (on your own)
|
Afternoon Session
|
2:00 - 2:45
|
Sharad Malik (Princeton University)
Optimization and Relaxation in SAT Search
|
2:45 - 3:30
|
Alessandro Cimatti (Istituto per la Ricerca Scientifica e Tecnologica (IRST))
Reasoning about Bit Vector Programs with Decision Procedures
|
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
|