Viktor Vafeiadis
Effective bounded verification of concurrent programs
Expecting automated verification techniques, such as model checking, to scale up so as to prove the correctness of non-trivial concurrent software is unrealistic. Rather than lowering our expectations in terms of the size and/or complexity of the programs to be verified, we can instead prove bounded notions of correctness, which do not guarantee complete absence of software errors, but only absence of “common” or “simple” errors. The talk will review recent results in making such bounded verification effective.
back to overview
Watch Recording
