Compositional verification of heap-manipulating programs through property-guided learning

Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order t...

Full description

Saved in:
Bibliographic Details
Main Authors: PHAM, Long H., SUN, Jun, LOC LE, Quang
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2019
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4639
https://ink.library.smu.edu.sg/context/sis_research/article/5642/viewcontent/Pham2019_Chapter_CompositionalVerificationOfHea.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-5642
record_format dspace
spelling sg-smu-ink.sis_research-56422024-07-30T08:02:58Z Compositional verification of heap-manipulating programs through property-guided learning PHAM, Long H. SUN, Jun LOC LE, Quang Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls. 2019-12-01T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4639 info:doi/10.1007/978-3-030-34175-6_21 https://ink.library.smu.edu.sg/context/sis_research/article/5642/viewcontent/Pham2019_Chapter_CompositionalVerificationOfHea.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Information Security Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Information Security
Software Engineering
spellingShingle Information Security
Software Engineering
PHAM, Long H.
SUN, Jun
LOC LE, Quang
Compositional verification of heap-manipulating programs through property-guided learning
description Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls.
format text
author PHAM, Long H.
SUN, Jun
LOC LE, Quang
author_facet PHAM, Long H.
SUN, Jun
LOC LE, Quang
author_sort PHAM, Long H.
title Compositional verification of heap-manipulating programs through property-guided learning
title_short Compositional verification of heap-manipulating programs through property-guided learning
title_full Compositional verification of heap-manipulating programs through property-guided learning
title_fullStr Compositional verification of heap-manipulating programs through property-guided learning
title_full_unstemmed Compositional verification of heap-manipulating programs through property-guided learning
title_sort compositional verification of heap-manipulating programs through property-guided learning
publisher Institutional Knowledge at Singapore Management University
publishDate 2019
url https://ink.library.smu.edu.sg/sis_research/4639
https://ink.library.smu.edu.sg/context/sis_research/article/5642/viewcontent/Pham2019_Chapter_CompositionalVerificationOfHea.pdf
_version_ 1814047733537832960