Finding Rare Bugs in Concurrent Programs

  • Date April 9, 2018
  • Hour 5 pm
  • Room GSSI Library
  • Speaker Salvatore La Torre (Universit√† di Salerno)
  • Area Computer Science

Abstract: Concurrent program verification remains a stubbornly hard problem. The large number of interleavings that a verifier must analyze poses a serious challenge to the traditional verification methods. Sequentializations, i.e., code-to-code translations of concurrent programs into "equivalent" sequential programs, provide an effective way to obtain tools by reusing existing technology developed for sequential programs.  Recent results have shown that sequentialization-based methods are very effective at finding bugs in practice.

In this talk, we will survey on the main sequentializations and discuss in more details the methods developed within the CSeq framework. The tools within this framework have been gold-medal winners for several editions of the software competition SV-COMP (TACAS) and are able to find bugs in benchmarks that are out of reach for the other verification tools, including testing.