Predicate Abstraction in Java Pathfinder

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F13%3A10144093" target="_blank" >RIV/00216208:11320/13:10144093 - isvavai.cz</a>
Result on the web
<a href="http://d3s.mff.cuni.cz/publications/download/Daniel-jpf13.pdf" target="_blank" >http://d3s.mff.cuni.cz/publications/download/Daniel-jpf13.pdf</a>
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Predicate Abstraction in Java Pathfinder
Original language description
We present our ongoing effort to implement predicate abstraction in Abstract Pathfinder, which is an extension of Java Pathfinder. Our approach builds upon existing abstraction techniques that have been proposed mainly for low-level programs in C. We support predicates over variables having numerical data types. The main challenges that we have addressed include (1) the design of the predicate language, (2) support for arrays, (3) finding predicates affected by a given statement, (4) aliasing between variables, (5) propagating values of predicates over method call boundaries, and (6) computing weakest preconditions for complex predicates. We describe our solution to these challenges and selected details about the implementation. We also discuss our future plans and research ideas.
Czech name
—
Czech description
—

Project
<a href="/en/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Software Components in Embedded Systems: Development and Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)