PV0 UCLID5

Application domain/field

Type of tool

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.
Framework Synthesis

Links

- Repository: https://github.com/uclid-org/uclid

Related papers

Last publication date

7 August 2022

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.