PV3 Skinkverifies assertions given in source code

Skink is a static analysis tool that analyses the LLVM intermediate representation (LLVM-IR) of a program source code

Application domain/field

Expected input

Program with assertions (assert(condition))


C file

Expected output

Verification output and witness file.


Uses Z3, SMTInterpol and CVC4. Skink may assume unbounded integers resulting in false negatives. Skink's analysis tries to determine whether an assertion can be violated.
C Compiler LLVM


Related papers

Skink: Static Analysis of Programs in LLVM Intermediate Representation (TACAS '17)

Last publication date

31 March 2017

ProVerB specific

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