Accession Number:

ADA592937

Title:

Scalable and Accurate SMT-Based Model Checking of Data Flow Systems

Descriptive Note:

Final rept. 1 Aug 2009-31 Oct 2013

Corporate Author:

NEW YORK UNIV NY

Personal Author(s):

Report Date:

2013-10-31

Pagination or Media Count:

21.0

Abstract:

In this project, we developed CVC4, a new SMT solver for use in verification and other applications, especially in the KIND model checker developed collaboratively at U Iowa. CVC4 was developed from scratch into an award-winning 200K LOC solver extensively used and cited by academic and industry users around the world. CVC4 is competitive with the very best SMT solvers and outperforms all other SMT solvers on certain classes of problems.

Subject Categories:

  • Computer Programming and Software
  • Computer Hardware

Distribution Statement:

APPROVED FOR PUBLIC RELEASE