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

• LLVM intermediate representation (LLVM-IR)
• Static analysis
• Reachability analysis
• Multi-threaded programs
• Concurrent programs

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.