...

l

In recent years a major shift in hardware architectures towards multi-core and many-core systems has taken place. In this session we want to discuss recent developments and future options for exploiting these architectures to efficiently solve decision problems. We will be starting off with a talk outlining the state of the art in parallelized SAT-solving and SMT-solving. Topics of the subsequent discussion may range from personal experience reports to elaborate exploration of technical challenges. We are especially interested in the exploration of shared memory CPU and GPU multi-processor systems.

Abstract

The task is to find a suitable model for verification purposes of distributed algorithms. As an example we verified the S algorithm of Chandra/Toug within the theorem proving environment Isabelle/HOL. We first designed a TLA+ model and adopted and extended this model to formally show the three consensus properties Validity, Agreement and Termination.

...