@hackage / afv

Infinite state model checking of iterative C programs.

Latest0.1.1

About

Metadata

  • Last updated , by TomHawkins
  • License BSD-3-Clause
  • Maintained by: Tom Hawkins <tomahawkins@gmail.com>

  • Lottery factor: 0

Links

Installation

Readme

AFV is an infinite state model checker that verifies iterative C programs by k-induction. AFV uses Yices as the backend SMT solver.