Sciweavers

CHARME
2005
Springer

Improvements to the Implementation of Interpolant-Based Model Checking

14 years 5 months ago
Improvements to the Implementation of Interpolant-Based Model Checking
The evolution of SAT technology over the last decade has motivated its application in model checking, initially through the utilization of SAT in bounded model checking (BMC) and, more recently, in unbounded model checking (UMC). This paper addresses the utilization of interpolants in UMC and proposes two techniques for improving the original interpolant-based UMC algorithm. These techniques include improvements to the computation of interpolants, and redefining the organization of the unbounded model checking algorithm given the information extracted from interpolant computation.
João P. Marques Silva
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CHARME
Authors João P. Marques Silva
Comments (0)