SSPV on Thursday, August 10th

Session 1 (09:45‑10:30)

09:45‑10:30

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

Break (10:30‑11:00)

Session 2 (11:00‑12:30)

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

Lunch break (12:30‑14:00)

Session 3 (14:00‑15:30)

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

Break (15:30‑16:00)

Session 4 (16:00‑16:45)

16:00‑16:45

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