Module VerificationSource

Sourcemodule Conditions : sig ... end

Generates verification conditions from scope definitions

Sourcemodule Io : sig ... end

Common code for handling the IO of all proof backends supported

Sourcemodule Solver : sig ... end

Solves verification conditions using various proof backends

Sourcemodule Z3backend : sig ... end

Interfacing with the Z3 SMT solver