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...
Saved in:
Main Authors: | , , |
---|---|
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 |