Nian-Ze Lee

Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs

Circuit-Based Program Verification is presented, a modular framework that translates C programs into sequential circuits and employs off-the-shelf hardware model checkers as backends and integrates multiple state-of-the-art hardware model checkers, which together provide access to diverse verification algorithms.