Abstract: Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment transitions, to enable scalable, compositional reasoning.  Once  the environment  transitions are identified,  we can prove  program  properties  by  considering  each  program  thread  in isolation,  as   the  environment  transitions  keep  track   of  the interleaving  with   other  threads.   Finding   adequate  environment transitions that are sufficiently  precise to yield conclusive results and yet do  not overwhelm the verifier with  unnecessary details about the interleaving  with other  threads is a  major challenge.   In this talk  we present a  method for  safety verification  of multi-threaded programs  that  applies   (transition)   predicate  abstraction-based discovery  of environment  transitions, exposing  a minimal  amount of information about the thread interleaving.   The crux of our method is an  abstraction  refinement procedure  that  uses recursion-free  Horn clauses to eclaratively  state abstraction refinement queries.  Then, the  queries  are  resolved  by  a  corresponding  constraint  solving algorithm.   We present  preliminary experimental  results  for mutual exclusion protocols and multi-threaded device drivers.

Hompage Andrey Rybalchenko

Article in Technology Review