PV4 COLIBRI (COnstraint LIBrary for veRIfication)produces a satisfiability result for a formula

Colibri is a family of three tools in Frama-C: COLIBRI (the ancestor in development since 2000), Colibri2 (its reimplementation in OCaml) and Colibrics (formally proved)

Application domain/field

SMT solving

Type of tool

SMT solver


ProVerB specific

Markdown description: view/edit

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