Verifying Concurrent Programs with Chalice - Leino, Rustan; Zurich), Peter Müller (ETH; Leuven), Jan Smans (KU (VMCAI, Madrid, Spain, 2010)
Concurrent programs Interleaving of thread executions Unbounded number of: threads, locks, … We need some basis for doing the reasoning A way of thinking!