Ten years of partial order reduction

Abstract

Checking the properties of concurrent systems is an ever growing challenge. Along with the development of improved verification methods, some critical systems that require careful attention have become highly concurrent and intricate. Partial order reduction methods were proposed for reducing the time and memory required to automatically verify concurrent asynchronous systems. We describe partial order reduction for various logical formalisms, such as LTL, CTL and process algebras. We show how one can combine partial order reduction with other efficient model checking techniques.