Module type Trace.S

module type S = sig .. end

The interface of certificate generators

val certificate : Ast.t_system -> Node.t list -> unit

this takes a system in input and the list of visited nodes, of which the disjunction constitutes an inductive invariant for the system.

certificate s visited must write on the disk a certificate of induction (initialization, preservation, and implication) and print the location of the generated certificate on stdout.