Affiliates Workshop: Satisfiability Solvers and Program Verification - IPAM

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

09: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 (Cadence)
SAT, Interpolants, and Software Model Checking
11:45-12:30
Shuvendu Lahiri (Carnegie-Mellon University)
Efficient SAT-based Techniques for Predicate Abstraction

Afternoon Session

12:30-14:00
Lunch (on your own)
14:00-14:45
Carla Gomes (Cornell University)
Beyond Satisfiability: Model Counting, Quantification, and Randomization
14:45-15:30
Daniel Kroening (Eidgenössische TH Zürich-Zentrum)
SAT-based methods for proving properties in Reynolds/O'Hearn Separation Logic
15:30-16:00
Break
16:00-16:45
Alex Aiken (Stanford University)
Scalable Program Analysis Using Boolean Satisfiability

Friday, August 11, 2006

Morning Session

09: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

Afternoon Session

12:30-14:00
Lunch (on your own)
14:00-14:45
Sharad Malik (Princeton University)
Optimization and Relaxation in SAT Search
14:45-15:30
Alessandro Cimatti (Istituto per la Ricerca Scientifica e Tecnologica (IRST))
Reasoning about Bit Vector Programs with Decision Procedures
15:30-16:00
Break
16:00-16:45
Robert Nieuwenhuis (Polytechnical University of Cataluña (Barcelona))
The New Architecture and Solvers in the Barcelogic Tool for SAT Modulo Theories
Printable Version