Predicate Abstraction in Java Pathfinder

Kód výsledku v 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>

Výsledek na webu

<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

—

Jazyk výsledku

angličtina

Název v původním jazyce

Predicate Abstraction in Java Pathfinder

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Predicate Abstraction in Java Pathfinder

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Vývoj a verifikace softwarových komponent v zapouzdřených systémech</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2013

Kód důvěrnosti údajů

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

Název statě ve sborníku

ACM SIGSOFT Software Engineering Notes

ISBN

—

ISSN

0163-5948

e-ISSN

—

Počet stran výsledku

5

Strana od-do

1-5

Název nakladatele

ACM

Místo vydání

Spojené Státy

Místo konání akce

Palo Alto, California, USA

Datum konání akce

12. 11. 2013

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—