System and method for modeling, abstraction, and analysis of software

摘要

A system and method is disclosed for formal verification of software programs that advantageously translates the software, which can have bounded recursion, into a Boolean representation comprised of basic blocks and which applies SAT-based model checking to the Boolean representation.