Lazy Decomposition for Distributed Decision Procedures

Youssef Hamadi
(Microsoft Research)
Joao Marques-Silva
(University College Dublin)
Christoph M. Wintersteiger
(Microsoft Research)

The increasing popularity of automated tools for software and hardware verification puts ever increasing demands on the underlying decision procedures. This paper presents a framework for distributed decision procedures (for first-order problems) based on Craig interpolation. Formulas are distributed in a lazy fashion, i.e., without the use of costly decomposition algorithms. Potential models which are shown to be incorrect are reconciled through the use of Craig interpolants. Experimental results on challenging propositional satisfiability problems indicate that our method is able to outperform traditional solving techniques even without the use of additional resources.

In Jiří Barnat and Keijo Heljanko: Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2011), Snowbird, Utah, USA, July 14, 2011, Electronic Proceedings in Theoretical Computer Science 72, pp. 43–54.
Published: 31st October 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.72.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org