Framework for modelling, verification and synthesis of systems
Expected input
Model
Format:
UCLID5 language
Expected output
Depends on the analysis that is used
Internals
Specifications can be written in several formats, including inline assertions in sequential code, pre-/postconditions for procedures, global axioms and invariants.
UCLID5 supports several verification techniques including bounded model checking, induction and k-induction, and more.
UCLID5 can also be used to synthesize function bodies for user-declared functions such that the verification task will succeed.
