54
IRUS TotalDownloads
Altmetric
Gillian, Part II: real-world verification for JavaScript and C
| File | Description | Size | Format | |
|---|---|---|---|---|
 2021_Book_ComputerAidedVerification.pdf | Published version | 29.67 MB | Adobe PDF | View/Open |
| Title: | Gillian, Part II: real-world verification for JavaScript and C |
| Authors: | Maksimovic, P Fragoso Santos, J Ayoun, SE Gardner, P |
| Item Type: | Conference Paper |
| Abstract: | We introduce verification based on separation logic to Gillian, a multi-language platform for the development of symbolic analysis tools which is parametric on the memory model of the target language. 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 AWS Encryption SDK message header deserialisation module, specificallydesigning common abstractions used for both verification tasks, and find two bugs in the JavaScript and three bugs in the C implementation. |
| Issue Date: | 15-Jul-2021 |
| Date of Acceptance: | 17-Apr-2021 |
| URI: | http://hdl.handle.net/10044/1/89626 |
| DOI: | 10.1007/978-3-030-81688-9_38 |
| ISSN: | 0302-9743 |
| Publisher: | Springer Verlag |
| Start Page: | 827 |
| End Page: | 850 |
| Journal / Book Title: | Lecture Notes in Computer Science |
| Copyright Statement: | © 2021 The Author(s). Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
| Sponsor/Funder: | Engineering & Physical Science Research Council (E |
| Funder's Grant Number: | EP/R034567/1 Continuous Reasoning Call |
| Conference Name: | 33rd International Conference on Computer-Aided Verification, (CAV 2021) |
| Keywords: | Science & Technology Technology Computer Science, Hardware & Architecture Computer Science, Software Engineering Computer Science, Theory & Methods Computer Science Artificial Intelligence & Image Processing |
| Publication Status: | Published |
| Start Date: | 2021-07-18 |
| Finish Date: | 2021-07-24 |
| Conference Place: | Virtual |
| Online Publication Date: | 2021-07-15 |
| Appears in Collections: | Computing Faculty of Engineering |
This item is licensed under a Creative Commons License
