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

Symbolic execution
Separation logic
Symbolic testing
Memory models

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

Last publication date

15 July 2021

Related tools

Other multi-language verification frameworks: coreStar, Viper.
Verification tools for JS based on separation logic: JaVerT
Verification tools for C based on separation logic: Verifast
The artefact description states that it "works in a close way to Klee's"

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

Program
Verification
Book

PV5 ⊧ Gillianverifies properties of a user-specified memory model

Application domain/field

Type of tool

Internals

Comments

Links

Related papers

Last publication date

Related tools

ProVerB specific

ProgramVerificationBook

PV5 ⊧ Gillianverifies properties of a user-specified memory model

Application domain/field

Type of tool

Internals

Comments

Links

Related papers

Last publication date

Related tools

ProVerB specific

Program
Verification
Book