ADVENT: Architecture-Driven Verification ADVENT
of Systems Software




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.