Program

All sessions will take place in Metropolitan A unless otherwise indicated.

Thursday, August 10th

Thursday's program is also available with abstracts or side by side with other meetings.

09:45‑10:30  Session 1

09:45

Ed Clarke (Carnegie Mellon University) Bounded and Unbounded Model Checking using SAT [ppt]

10:30‑11:00  Break

11:00‑12:30  Session 2

11:00	Ken McMillan (Cadence Labs) SAT, interpolants, and software model checking [ppt]
11:45	Shuvendu Lahiri (Microsoft Research) Efficient SAT-based Techniques for Predicate Abstraction [ppt]

12:30‑14:00  Lunch break

14:00‑15:30  Session 3

14:00	Carla Gomes (Cornell University) Beyond Satisfiability: Model Counting, Quantification, and Randomization [ppt]
14:45	Daniel Kroening (ETH Zurich) SAT-based methods for proving properties in Reynolds/O'Hearn Separation Logic [ppt]

15:30‑16:00  Break

16:00‑16:45  Session 4

16:00

Alex Aiken (Stanford University) Scalable Program Analysis Using Boolean Satisfiability [pdf]

Friday, August 11th

Friday's program is also available with abstracts or side by side with other meetings.

09:45‑10:30  Session 5

09:45

Orna Grumberg (Technion) Hybrid BDD and All-SAT Method for Model Checking [ppt]

10:30‑11:00  Break

11:00‑12:30  Session 6

11:00	Aarti Gupta (NEC Labs) Verifying C Programs using SAT-based model checking [pdf]
11:45	Ofer Strichman (Technion) Decision Heuristics based on an Abstraction/Refinement model [ppt]

12:30‑14:00  Lunch break

14:00‑15:30  Session 7

14:00	Sharad Malik (Princeton University) Optimization and Relaxation in SAT Search [pdf]
14:45	Alessandro Cimatti (IRST) Reasoning about Bit Vector programs with Decision Procedures [ppt]

15:30‑16:00  Break

16:00‑16:45  Session 8

16:00

Robert Nieuwenhuis (Technical University of Catalonia) The new architecture and solvers in the Barcelogic tool for SAT modulo theories [pdf]