TLV: Abstraction through testing, learning, and validation

A (Java) class provides a service to its clients (i.e., programs which use the class). The service must satisfy certain specifications. Different specifications might be expected at different levels of abstraction depending on the client's objective. In order to effectively contrast the class a...

Full description

Saved in:
Bibliographic Details
Main Authors: SUN, Jun, XIAO, Hao, LIU, Yang, LIN, Shang-Wei, QIN, Shengchao
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2015
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4975
https://ink.library.smu.edu.sg/context/sis_research/article/5978/viewcontent/tlv.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-5978
record_format dspace
spelling sg-smu-ink.sis_research-59782020-03-12T07:31:16Z TLV: Abstraction through testing, learning, and validation SUN, Jun XIAO, Hao LIU, Yang LIN, Shang-Wei QIN, Shengchao A (Java) class provides a service to its clients (i.e., programs which use the class). The service must satisfy certain specifications. Different specifications might be expected at different levels of abstraction depending on the client's objective. In order to effectively contrast the class against its specifications, whether manually or automatically, one essential step is to automatically construct an abstraction of the given class at a proper level of abstraction. The abstraction should be correct (i.e., over-approximating) and accurate (i.e., with few spurious traces). We present an automatic approach, which combines testing, learning, and validation, to constructing an abstraction. Our approach is designed such that a large part of the abstraction is generated based on testing and learning so as to minimize the use of heavy-weight techniques like symbolic execution. The abstraction is generated through a process of abstraction/refinement, with no user input, and converges to a specific level of abstraction depending on the usage context. The generated abstraction is guaranteed to be correct and accurate. We have implemented the proposed approach in a toolkit named TLV and evaluated TLV with a number of benchmark programs as well as three real-world ones. The results show that TLV generates abstraction for program analysis and verification more efficiently. 2015-04-09T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4975 info:doi/10.1145/2786805.2786817 https://ink.library.smu.edu.sg/context/sis_research/article/5978/viewcontent/tlv.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 Program Abstraction Automata Learning Behavior Models Symbolic Execution Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Program Abstraction
Automata Learning
Behavior Models
Symbolic Execution
Software Engineering
spellingShingle Program Abstraction
Automata Learning
Behavior Models
Symbolic Execution
Software Engineering
SUN, Jun
XIAO, Hao
LIU, Yang
LIN, Shang-Wei
QIN, Shengchao
TLV: Abstraction through testing, learning, and validation
description A (Java) class provides a service to its clients (i.e., programs which use the class). The service must satisfy certain specifications. Different specifications might be expected at different levels of abstraction depending on the client's objective. In order to effectively contrast the class against its specifications, whether manually or automatically, one essential step is to automatically construct an abstraction of the given class at a proper level of abstraction. The abstraction should be correct (i.e., over-approximating) and accurate (i.e., with few spurious traces). We present an automatic approach, which combines testing, learning, and validation, to constructing an abstraction. Our approach is designed such that a large part of the abstraction is generated based on testing and learning so as to minimize the use of heavy-weight techniques like symbolic execution. The abstraction is generated through a process of abstraction/refinement, with no user input, and converges to a specific level of abstraction depending on the usage context. The generated abstraction is guaranteed to be correct and accurate. We have implemented the proposed approach in a toolkit named TLV and evaluated TLV with a number of benchmark programs as well as three real-world ones. The results show that TLV generates abstraction for program analysis and verification more efficiently.
format text
author SUN, Jun
XIAO, Hao
LIU, Yang
LIN, Shang-Wei
QIN, Shengchao
author_facet SUN, Jun
XIAO, Hao
LIU, Yang
LIN, Shang-Wei
QIN, Shengchao
author_sort SUN, Jun
title TLV: Abstraction through testing, learning, and validation
title_short TLV: Abstraction through testing, learning, and validation
title_full TLV: Abstraction through testing, learning, and validation
title_fullStr TLV: Abstraction through testing, learning, and validation
title_full_unstemmed TLV: Abstraction through testing, learning, and validation
title_sort tlv: abstraction through testing, learning, and validation
publisher Institutional Knowledge at Singapore Management University
publishDate 2015
url https://ink.library.smu.edu.sg/sis_research/4975
https://ink.library.smu.edu.sg/context/sis_research/article/5978/viewcontent/tlv.pdf
_version_ 1770575164164014080