Skink Software Verification Tool

    

Computer software routinely contains bugs and in many cases these bugs can be exploited to cause it to malfunction, including to reveal security issues. Skink belongs to a growing collection of tools that can automatically analyse the software code to diagnose and report bugs.

Skink is a new tool that combines existing trace abstraction refinement techniques with a new implementation approach based on programming language specifications and tools.

We have entered Skink in the International Competition on Software Verification (SV-COMP) in 2016-2018.

Participants

• Anthony Sloane
• Franck Cassez

Publications

Cassez, F., Sloane, A. M., Roberts, M., Pigram, M., Suvanpong, P., and de Aledo, P. G. 2017. Skink: Static Analysis of Programs in {LLVM} Intermediate Representation. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 380-384. PDF

Cassez, F. and Sloane, A. M. 2017. ScalaSMT: satisfiability modulo theory in Scala. International Symposium on Scala. 51-55. PDF

Software

The Skink source code can be found on github. Binary versions that were used in the International Competition on Software Verification can be found via the competition website.

Skink uses the following libraries and tools:

• Kiama Language Processing Library
• sbt-rats parser generator
• ScalaSMT SMT solver library