Domain Pattern Abstraction + Ptolemaic Abstract Domains = Environment Abstraction for Concurrent Systems
Murali Talupur, Helmut Veith · 2008
With the rapid onset of the multi-core era, the verification of multi-threaded systems and concurrent algorithms has become a pressing problem in the hardware and software industries. While traditional techniques like testing and simulation are often adequate for sequential software and hardware, they are not suited for validating concurrent systems; due to their their massive parallelism, concurrent systems have way too many possible interleavings for these informal techniques. Therefore, concurrent systems should be verified formally using techniques like model checking or theorem proving. In this talk, we discuss environment abstraction [13, 4, 5], a novel model checking based approach for the verification of concurrent software. Environment abstraction is designed for systems with replicated processes, i.e., systems where the same process/algorithm is executed by multiple agents concurrently. Such systems often form the basic building blocks of larger systems, and tend to be combinatorially intricate; many of them, for instance cache coherence protocols, are also very large. At design time, the number of concurrent processes is unknown, and thus we speak of parameterized verification. We have applied environment abstraction successfully to a broad