Verifying Concurrent Programs with Chalice

  • Rustan Leino ,
  • Peter Müller (ETH Zurich) ,
  • Jan Smans (KU Leuven)

VMCAI, Madrid, Spain |

Published by Microsoft Research

Download BibTex

Concurrent programs

  • Interleaving of thread executions
  • Unbounded number of: threads, locks, …
  • We need some basis for doing the reasoning
    • A way of thinking!