Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/36303
Full metadata record
DC FieldValueLanguage
dc.contributor.authorPiterman, Nir-
dc.contributor.authorBakhirkin, Alexey-
dc.date.accessioned2016-01-18T14:57:54Z-
dc.date.available2017-03-08T02:45:07Z-
dc.date.issued2016-04-03-
dc.identifier.citationFinding Recurrent Sets with Backward Analysis and Trace Partitioning. In: Chechik M., Raskin JF. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2016. Lecture Notes in Computer Science, vol 9636.en
dc.identifier.issn0302-9743-
dc.identifier.urihttps://link.springer.com/chapter/10.1007/978-3-662-49674-9_2en
dc.identifier.urihttp://hdl.handle.net/2381/36303-
dc.description.abstractWe propose an abstract-interpretation-based analysis for recurrent sets. A recurrent set is a set of states from which the execution of a program cannot or might not (as in our case) escape. A recurrent set is a part of a program’s nontermination proof (that needs to be complemented by reachability analysis). We find recurrent sets by performing a potentially over-approximate backward analysis that produces an initial candidate. We then perform over-approximate forward analysis on the candidate to check and refine it and ensure soundness. In practice, the analysis relies on trace partitioning that predicts future paths through the program that non-terminating executions will take. Using our technique, we were able to find recurrent sets in many benchmarks found in the literature including some that, to our knowledge, cannot be handled by existing tools. In addition, we note that typically, analyses that search for recurrent sets are applied to linear under-approximations of programs or employ some form of non-approximate numeric reasoning. In contrast, our analysis uses standard abstract-interpretation techniques and is potentially applicable to a larger class of abstract domains (and therefore – programs).en
dc.language.isoenen
dc.publisherSpringer Verlagen
dc.relation.ispartofseriesLecture Notes In Computer Science;9636-
dc.rightsCopyright © Springer Verlag. Deposited with reference to the publisher’s archiving policy available on the SHERPA/RoMEO website 18/01/2016.en
dc.titleFinding Recurrent Sets with Backward Analysis and Trace Partitioningen
dc.typeConference Paperen
dc.identifier.doi10.1007/978-3-662-49674-9_2-
dc.description.versionPost-printen
dc.description.presented22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2-8 April 2016, Eindhoven, The Netherlands.en
pubs.organisational-group/Organisationen
pubs.organisational-group/Organisation/COLLEGE OF SCIENCE AND ENGINEERINGen
pubs.organisational-group/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Scienceen
dc.dateaccepted2015-12-18-
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
paper_30.pdfPost-review (final submitted)233.79 kBUnknownView/Open


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