An initial survey of verification tools

VerificationToolAnalysis.md

Preliminary Tool Analysis

The Key Project

The Key Project is primarily a symbolic execution engine for Java Programs. It is available as a standalone application and an eclipse plugin.

Pros

• Heavy on formal methods: Pre-Conditions, Invariants, etc. must be understood to properly utilize the tool
• Appart from that, appears to be relatively easy to use
• Heavy focus on teaching
• Decent documentation

Cons

• Needs quite some onboarding. Concepts would have to be taught to utilize properly
• Requires knowledge of the Java Modelling Language

Further investigation is recommended. Probably a bit too complex to teach with other course contents. Would probably need its own course.

Static Analysis for Java: Findbugs, PMD, Checkstyles

A collection of static analysis tools that provide a decent overview of possible problems, but are not fully fledged symbolic execution engines. For example default branches that are never executed can be detected.

Pros

• Super easy to use, with instant benefits
• Good IDE integrations available
• Underlying theoretical concepts are relatively easy explained

Cons

• Partly made obsolete by other tools, e.g. SonarQube or Tools already included in IDEs.

Use in a course using Java is recommended. Code smells and bad design decisions can easily be made transparent using those tools.

Java pathfinder

Java pathfinder is a NASA backed project for - amongst other things - symbolic execution of Java bytecode. As such, it can be used to detect race conditions, invalid program states and bugs.

Pros

• Lots of documentation
• Easy to set up, easy to use
• Theoretical background for base applications can be easily explained

Cons

• Documentation is somewhat fragmented, but thats about it

I recommend utilizing Java Pathfinder in fitting Courses. Since the program can easily be set up it can easily be made part of an exercise.

Klee

Klee is a LLVM based project that uses symbolic execution to find bugs in existing C-programs.

Pros

• Good documentation and tutorials
• Okayish to set up

Cons

• Usage is a bit difficult
• Runs only on linux

For courses utilizing C this tool might provide some benefits. Due to the extensive dependencies this tool will probably break some students resolve.

Frama-C

Frama-C is a theorem prover for C-programs. It utilizes the dedicated language ACSL to specify program properties to be verified. Because of time constraints the program has not been tried by myself.

Pros

• Fairly thorough documentation
• Very easy to set up (Windows & Linux)
• Appears to be easy to use

Cons

• Properties are specified in ACSL, which is a specific modeling language
• Theoretical background is required.

Since proper usage of Frama-C requires knowledge of a specific modeling language usage is not recommended.

CBMC

CBMC is a bounded model checker for C and Java - although Java support appears to be experimental. It can be used to check for a variety of bugs.

Pros

• Cross platform
• Easy to set up.
• Lots of configuration possibilites - hard to master

Cons

• Lot's of functions, but hard to find out how to use

CBMC might be used in a course if a proper introduction to it's usage can be given.