Automated Specification Discovery via User-Defined Predicates

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

Research output: Chapter in Book/Report/Conference proceedingChapter

221 Downloads (Pure)


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
Publication statusPublished - 2013

Publication series

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

Bibliographical note

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


Dive into the research topics of 'Automated Specification Discovery via User-Defined Predicates'. Together they form a unique fingerprint.

Cite this