copilot-theorem-3.2.1: k-induction for Copilot.
Safe HaskellSafe
LanguageHaskell2010

Copilot.Theorem

Description

Highly automated proof techniques are a necessary step for the widespread adoption of formal methods in the software industry. Moreover, it could provide a partial answer to one of its main issue which is scalability.

Copilot-theorem is a Copilot library aimed at checking automatically some safety properties on Copilot programs. It includes:

  • A prover producing native inputs for the Kind2 model checker.
  • A What4 backend that uses SMT solvers to prove safety properties.
Synopsis

Documentation

instantiate :: Proof Universal -> Proof Existential Source #

Instantiate a universal proof into an existential proof.

assume :: PropRef Universal -> Proof a Source #

Assume that a property, given by reference, holds.

admit :: Proof a Source #

Assume that the current goal holds.

type Proof a = ProofScheme a () Source #

A proof scheme with unit result.

type PropId = String Source #

A unique property identifier

data PropRef a Source #

Reference to a property.

data Universal Source #

Empty datatype to mark proofs of universally quantified predicates.

data Existential Source #

Empty datatype to mark proofs of existentially quantified predicates.