PV5 Gillianverifies properties of a user-specified memory model

Separation logic-based multi-language verification architecture/framework. It can be used to verify C and JavaScript code (Gillian-C and Gillian-JS respectively).

Application domain/field

Type of tool

Framework

Internals

Gillian uses compositional memory models of JS and C. Gillian does not seem to support reasoning about concurrent programs.

Comments

License: BSD-3-Clause
C JavaScript

Links

Last commit date

23 April 2022

Related papers

https://doi.org/10.1007/978-3-030-81688-9_38 (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.