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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 31, 2013
Accession Number
ADA592937

Entities

People

  • Clark Barrett
  • Morgan Deters

Organizations

  • New York University

Tags

Communities of Interest

  • Cyber

DTIC Thesaurus Topics

  • Artificial Intelligence Computing
  • Collision Avoidance
  • Collision Avoidance Systems
  • Computer Programs
  • Computer Science
  • Computer-Aided Design
  • Computers
  • Engineering
  • Language
  • New York
  • Operating Systems
  • Product Prototyping
  • Software Prototyping
  • Standards
  • Theses
  • Traffic Collision Avoidance System
  • Vehicles

Fields of Study

  • Computer science

Readers

  • Computational Fluid Dynamics (CFD)
  • Mathematical Modeling and Probability Theory.
  • STEM Education