This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Abstract. Automatic formal verification techniques generally require exponential resources with respect to the number of primary inputs of a netlist. In this paper, we present sev...
Abstract. Unbounded model checking of invariant properties is typically solved using symbolic reachability. However, BDD based reachability methods suffer from lack of robustness ...
Debashis Sahoo, Jawahar Jain, Subramanian K. Iyer,...
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, ...
Abstract. We propose a new saturation-based symbolic state-space generation algorithm for finite discrete-state systems. Based on the structure of the high-level model specificat...