CertifCheckerval generate_certificate : TransSys.t -> string -> unitGenerate a certificate from a (possibly) proved system. It is written in the file <input_file>.certificate.smt2 placed in the current directory by default. It is bundled with an SMT2 script to check its validity.
Generate a system for observational equivalence for the frontend translation / simplification phases as a system in native input. To be verified, this certificate is expected to be fed back to Kind 2.
val generate_smt2_certificates : 'a InputSystem.t -> TransSys.t -> unitGenerate intermediate SMT-LIB 2 certificates in the directory given by Flags.output_dir.
val generate_slicing_certificates :
'a InputSystem.t ->
TransSys.t ->
Analysis.param ->
unitGenerate intermediate slicing certificates in the directory given by Flags.output_dir.
val generate_all_proofs : int -> 'a InputSystem.t -> TransSys.t -> unitGenerate CPC proofs in the directory given by Flags.output_dir.
val minimize_invariants :
TransSys.t ->
Term.t list option ->
(Term.t -> bool) option ->
int * Term.t listMinimization of certificate: returns the minimum bound for k-induction and a list of useful invariants for this preservation step.
The second parameter is an optional list of properties (if None, all the safe properties are considered).
The third parameter is an optional predicate that forces the minimization to only consider invariants that evaluates to true.
val is_two_state : Term.t -> boolReturns true if the term contains at least two different var offsets