Artifact - Gillian, Part II: Real-World Verification for JavaScript and C

We introduce compositional symbolic execution and verification based on separation logic to Gillian, a multi-language platform for the development of symbolic analysis tools. Our work develops a methodology for constructing compositional memory models for Gillian, leading to a unified presentation of the JavaScript and C memory models. We verify the JavaScript and C implementations of the Amazon AWS Encryption SDK message header deserialisation module, specifically designing common abstractions used for both verification tasks, and find two bugs in the JavaScript and three bugs in the C implementation. The artifact contains the implementation of Gillian and its instantiations to JavaScript and C, together with the verified specifications of the JavaScript and C implementations of the Amazon AWS Encryption SDK message header deserialisation module. The artifact is submitted to be evaluated for the functional badge.

Related Organizations

Keywords

Symbolic Execution, Software Verification, Formal methods

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	1
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average