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))

Format:

C file

Expected output

Verification output and witness file.

Internals

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

Links

Last commit date

24 December 2015

Related papers

https://doi.org/10.1007/978-3-662-54580-5_27 (TACAS '17)

Last publication date

31 March 2017

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.