Synthesis of parallel programs invariants

Abstract

Most current methods for parallel programs design and verification are based on the concept of invariant. However, invariant synthesis is the most difficult part of those methods. This work presents a technique for invariant design usable for both parallel program synthesis and verification. This technique drastically reduces the risks of errors due to a bad statement serialization or to inadequate interprocess synchronization.