Monadoc

copilot-verifier

Version 4.0 revision 0 uploaded by ryanglscott.

Package meta

Synopsis
System for verifying the correctness of generated Copilot programs
Description

copilot-verifier is an add-on to the Copilot Stream DSL for verifying the correctness of C code generated by the copilot-c99 package.

copilot-verifier uses the Crucible symbolic simulator to interpret the semantics of the generated C program and and to produce verification conditions sufficient to guarantee that the meaning of the generated program corresponds in a precise way to the meaning of the original stream specification. The generated verification conditions are then dispatched to SMT solvers to be automatically solved.

Author
Galois Inc.
Bug reports
n/a
Category
Language
Copyright
(c) Galois, Inc 2021-2024
Homepage
n/a
Maintainer
rscott@galois.com
Package URL
n/a
Stability
n/a

Components