Necessary and sufficient preconditions via eager abstraction

Seghir, Mohamed Nassim and Schrammel, Peter (2014) Necessary and sufficient preconditions via eager abstraction. In: Garrigue, Jacques (ed.) Programming languages and systems : 12th Asian Symposium, APLAS 2014, Singapore, Singapore, November 17-19, 2014, Proceedings. Lecture notes in computer science (8858). Springer, pp. 236-254. ISBN 9783319127354

[img] PDF - Published Version
Restricted to SRO admin only

Download (395kB)


The precondition for safe execution of a procedure is useful for understanding, verifying and debugging programs. We have previously presented a cegar-based approach for inferring necessary and sufficient preconditions based on the iterative abstraction-refinement of the set of safe and unsafe states until they become disjoint. A drawback of that approach is that safe and unsafe traces are explored separately and each time they are built entirely before being checked for consistency. In this paper, we present an eager approach that explores shared prefixes between safe and unsafe traces conjointly. As a result, individual state sets, by construction, fulfil the property of separation between safe and unsafe states without requiring any refinement. Experiments using our implementation of this technique in the precondition generator P-Gen show a significant improvement compared to our previous cegar-based method. In some cases the running time drops from several minutes to several seconds.

Item Type: Book Section
Keywords: verification, precondition inference, predicate abstraction, CEGAR
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Peter Schrammel
Date Deposited: 09 May 2016 05:43
Last Modified: 09 May 2016 05:43

View download statistics for this item

📧 Request an update