Description: Academic prototype to build enabledness-based program abstractions (EPAs) out of APIs written in C and pre/post contracts written in (a kind of) FOL. Contractor generates a finite abstraction representing the contract of software and validates such abstraction with respect to user-defined properties. For programs in C, Contractor relies on Blast model checkers and for deciding contracts it uses tools based on SMT (Satisfiability Modulo Theories) (e.g, CVC/Z3).

Developed at: UBA

Contacts: diegog@dc.uba.ar

Available at: https://lafhis.dc.uba.ar/dependex/contractor/Welcome.html