.
FRDCSA | git codebases | CPArec
Homepage

[Project image]
CPArec

Jump to: Project Description

Project Description

CPArec is a tool for verifying recursive C programs via source-to-source program transformation. It uses a recursion-free program analyzer CPAChecker as a black box and computes function summaries from the inductive invariants generated by CPAChecker_. Such function summaries enable CPArec to check recursive programs.


This page is part of the FWeb package.
Last updated Sat Oct 26 16:59:56 EDT 2019 .