Verification tools

To automate the use of the reasoning techniques devised in the ADVENT project, we are contributing to the development of the following verification tools.

VeriFast

VeriFast is a semi-automated verifier for C and Java programs. In the ADVENT project, we have added support for reasoning about:

• Concurrent programs under SC in the style of rely/guarantee [Read more],
• Concurrent programs under the x86-TSO memory model [Read more],
• Concurrent programs under the C/C++11 memory model, and
• Input/output [Read more].

[Website (including downloads for Windows, Linux, and MacOS)] [Tutorial]

Cave

Cave is an automatic verification tool for concurrent libraries. During the ADVENT project, we are extending the tool to support:

• Our novel aspect-oriented approach for verifying linearizability of concurrent queues,
• Verification of C11 programs using the GPS program logic, and
• Verifying lock-freedom of concurrent libraries.

For more information about Cave, please follow this link.