Code2Inv: A Deep Learning Framework for Program Verification

We propose a general end-to-end deep learning framework Code2Inv, which takes a verification task and a proof checker as input, and automatically learns a valid proof for the verification task by interacting with the given checker. Code2Inv is parameterized with an embedding module and a grammar: th...

Descripción completa

Detalles Bibliográficos
Autores principales: Si, Xujie, Naik, Aaditya, Dai, Hanjun, Naik, Mayur, Song, Le
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363181/
http://dx.doi.org/10.1007/978-3-030-53291-8_9
_version_ 1783559618630254592
author Si, Xujie
Naik, Aaditya
Dai, Hanjun
Naik, Mayur
Song, Le
author_facet Si, Xujie
Naik, Aaditya
Dai, Hanjun
Naik, Mayur
Song, Le
author_sort Si, Xujie
collection PubMed
description We propose a general end-to-end deep learning framework Code2Inv, which takes a verification task and a proof checker as input, and automatically learns a valid proof for the verification task by interacting with the given checker. Code2Inv is parameterized with an embedding module and a grammar: the former encodes the verification task into numeric vectors while the latter describes the format of solutions Code2Inv should produce. We demonstrate the flexibility of Code2Inv by means of two small-scale yet expressive instances: a loop invariant synthesizer for C programs, and a Constrained Horn Clause (CHC) solver.
format Online
Article
Text
id pubmed-7363181
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73631812020-07-16 Code2Inv: A Deep Learning Framework for Program Verification Si, Xujie Naik, Aaditya Dai, Hanjun Naik, Mayur Song, Le Computer Aided Verification Article We propose a general end-to-end deep learning framework Code2Inv, which takes a verification task and a proof checker as input, and automatically learns a valid proof for the verification task by interacting with the given checker. Code2Inv is parameterized with an embedding module and a grammar: the former encodes the verification task into numeric vectors while the latter describes the format of solutions Code2Inv should produce. We demonstrate the flexibility of Code2Inv by means of two small-scale yet expressive instances: a loop invariant synthesizer for C programs, and a Constrained Horn Clause (CHC) solver. 2020-06-16 /pmc/articles/PMC7363181/ http://dx.doi.org/10.1007/978-3-030-53291-8_9 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
Si, Xujie
Naik, Aaditya
Dai, Hanjun
Naik, Mayur
Song, Le
Code2Inv: A Deep Learning Framework for Program Verification
title Code2Inv: A Deep Learning Framework for Program Verification
title_full Code2Inv: A Deep Learning Framework for Program Verification
title_fullStr Code2Inv: A Deep Learning Framework for Program Verification
title_full_unstemmed Code2Inv: A Deep Learning Framework for Program Verification
title_short Code2Inv: A Deep Learning Framework for Program Verification
title_sort code2inv: a deep learning framework for program verification
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363181/
http://dx.doi.org/10.1007/978-3-030-53291-8_9
work_keys_str_mv AT sixujie code2invadeeplearningframeworkforprogramverification
AT naikaaditya code2invadeeplearningframeworkforprogramverification
AT daihanjun code2invadeeplearningframeworkforprogramverification
AT naikmayur code2invadeeplearningframeworkforprogramverification
AT songle code2invadeeplearningframeworkforprogramverification

Ejemplares similares