RustHorn: CHC-Based Verification for Rust Programs

Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulatin...

Descripción completa

Detalles Bibliográficos
Autores principales: Matsushita, Yusuke, Tsukada, Takeshi, Kobayashi, Naoki
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7702263/
http://dx.doi.org/10.1007/978-3-030-44914-8_18
_version_ 1783616579584393216
author Matsushita, Yusuke
Tsukada, Takeshi
Kobayashi, Naoki
author_facet Matsushita, Yusuke
Tsukada, Takeshi
Kobayashi, Naoki
author_sort Matsushita, Yusuke
collection PubMed
description Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
format Online
Article
Text
id pubmed-7702263
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-77022632020-12-01 RustHorn: CHC-Based Verification for Rust Programs Matsushita, Yusuke Tsukada, Takeshi Kobayashi, Naoki Programming Languages and Systems Article Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method. 2020-04-18 /pmc/articles/PMC7702263/ http://dx.doi.org/10.1007/978-3-030-44914-8_18 Text en © The Author(s) 2020 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.
spellingShingle Article
Matsushita, Yusuke
Tsukada, Takeshi
Kobayashi, Naoki
RustHorn: CHC-Based Verification for Rust Programs
title RustHorn: CHC-Based Verification for Rust Programs
title_full RustHorn: CHC-Based Verification for Rust Programs
title_fullStr RustHorn: CHC-Based Verification for Rust Programs
title_full_unstemmed RustHorn: CHC-Based Verification for Rust Programs
title_short RustHorn: CHC-Based Verification for Rust Programs
title_sort rusthorn: chc-based verification for rust programs
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7702263/
http://dx.doi.org/10.1007/978-3-030-44914-8_18
work_keys_str_mv AT matsushitayusuke rusthornchcbasedverificationforrustprograms
AT tsukadatakeshi rusthornchcbasedverificationforrustprograms
AT kobayashinaoki rusthornchcbasedverificationforrustprograms

Ejemplares similares