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



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


License: BSD-3-Clause
C JavaScript


Related papers

Gillian, Part II: Real-World Verification for JavaScript and C (CAV '21)

Last publication date

15 July 2021

Related tools

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.