Automated Specification Discovery via User-Defined Predicates

Guanhua He, Shengchao Qin, Wei-Ngan Chin, Florin Craciun

Research output: Chapter in Book/Report/Conference proceedingChapterResearch

25 Downloads (Pure)

Abstract

Automated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science
Pages397-414
Volume8144
DOIs
Publication statusPublished - 2013

Publication series

NameFormal Methods and Software Engineering
Volume8144
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Data structures
Specifications
Data storage equipment
Experiments

Bibliographical note

Subject to 12 month embargo author can archive post-print (ie final draft post-refereeing).

Cite this

He, G., Qin, S., Chin, W-N., & Craciun, F. (2013). Automated Specification Discovery via User-Defined Predicates. In Lecture Notes in Computer Science (Vol. 8144, pp. 397-414). [Chapter 26] (Formal Methods and Software Engineering; Vol. 8144). https://doi.org/10.1007/978-3-642-41202-8_26
He, Guanhua ; Qin, Shengchao ; Chin, Wei-Ngan ; Craciun, Florin. / Automated Specification Discovery via User-Defined Predicates. Lecture Notes in Computer Science . Vol. 8144 2013. pp. 397-414 (Formal Methods and Software Engineering).
@inbook{3c03dd48d3bc46d18397a398ea5a55ee,
title = "Automated Specification Discovery via User-Defined Predicates",
abstract = "Automated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.",
author = "Guanhua He and Shengchao Qin and Wei-Ngan Chin and Florin Craciun",
note = "Subject to 12 month embargo author can archive post-print (ie final draft post-refereeing).",
year = "2013",
doi = "10.1007/978-3-642-41202-8_26",
language = "English",
volume = "8144",
series = "Formal Methods and Software Engineering",
pages = "397--414",
booktitle = "Lecture Notes in Computer Science",

}

He, G, Qin, S, Chin, W-N & Craciun, F 2013, Automated Specification Discovery via User-Defined Predicates. in Lecture Notes in Computer Science . vol. 8144, Chapter 26, Formal Methods and Software Engineering, vol. 8144, pp. 397-414. https://doi.org/10.1007/978-3-642-41202-8_26

Automated Specification Discovery via User-Defined Predicates. / He, Guanhua; Qin, Shengchao; Chin, Wei-Ngan; Craciun, Florin.

Lecture Notes in Computer Science . Vol. 8144 2013. p. 397-414 Chapter 26 (Formal Methods and Software Engineering; Vol. 8144).

Research output: Chapter in Book/Report/Conference proceedingChapterResearch

TY - CHAP

T1 - Automated Specification Discovery via User-Defined Predicates

AU - He, Guanhua

AU - Qin, Shengchao

AU - Chin, Wei-Ngan

AU - Craciun, Florin

N1 - Subject to 12 month embargo author can archive post-print (ie final draft post-refereeing).

PY - 2013

Y1 - 2013

N2 - Automated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.

AB - Automated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.

U2 - 10.1007/978-3-642-41202-8_26

DO - 10.1007/978-3-642-41202-8_26

M3 - Chapter

VL - 8144

T3 - Formal Methods and Software Engineering

SP - 397

EP - 414

BT - Lecture Notes in Computer Science

ER -

He G, Qin S, Chin W-N, Craciun F. Automated Specification Discovery via User-Defined Predicates. In Lecture Notes in Computer Science . Vol. 8144. 2013. p. 397-414. Chapter 26. (Formal Methods and Software Engineering). https://doi.org/10.1007/978-3-642-41202-8_26