Please use this identifier to cite or link to this item: https://scholarbank.nus.edu.sg/handle/10635/40121
DC FieldValue
dc.titleA CLP method for compositional and intermittent predicate abstraction
dc.contributor.authorJaffar, J.
dc.contributor.authorSantosa, A.E.
dc.contributor.authorVoicu, R.
dc.date.accessioned2013-07-04T07:57:07Z
dc.date.available2013-07-04T07:57:07Z
dc.date.issued2006
dc.identifier.citationJaffar, J.,Santosa, A.E.,Voicu, R. (2006). A CLP method for compositional and intermittent predicate abstraction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3855 LNCS : 17-32. ScholarBank@NUS Repository.
dc.identifier.isbn3540311394
dc.identifier.issn03029743
dc.identifier.urihttp://scholarbank.nus.edu.sg/handle/10635/40121
dc.description.abstractWe present an implementation of symbolic reachability analysis with the features of compositionality, and intermittent abstraction, in the sense of pefrorming approximation only at selected program points, if at all. The key advantages of compositionality are well known, while those of intermittent abstraction are that the abstract domain required to ensure convergence of the algorithm can be minimized, and that the cost of performing abstractions, now being intermittent, is reduced. We start by formulating the problem in CLP, and first obtain compositionality. We then address two key efficiency challenges. The first is that reasoning is required about the strongest-postcondition operator associated with an arbitrarily long program fragment. This essentially means dealing with constraints over an unbounded number of variables describing the states between the start and end of the program fragment at hand. This is addressed by using the variable elimination or projection mechanism that is implicit in CLP systems. The second challenge is termination, that is, to determine which subgoals are redundant. We address this by a novel formulation of memoization called coinductive tabling. We finally evaluate the method experimentally. At one extreme, where abstraction is performed at every step, we compare against a model checker. At the other extreme, where no abstraction is performed, we compare against a program verifier. Of course, our method provides for the middle ground, with a flexible combination of abstraction and Hoare-style reasoning with predicate transformers and loop-invariants. © Springer-Verlag Berlin Heidelberg 2006.
dc.sourceScopus
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.sourcetitleLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
dc.description.volume3855 LNCS
dc.description.page17-32
dc.identifier.isiutNOT_IN_WOS
Appears in Collections:Staff Publications

Show simple item record
Files in This Item:
There are no files associated with this item.

Page view(s)

155
checked on Nov 24, 2022

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.