On partial state matching

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F17%3A10364753" target="_blank" >RIV/00216208:11320/17:10364753 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/s00165-016-0413-z" target="_blank" >http://dx.doi.org/10.1007/s00165-016-0413-z</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s00165-016-0413-z" target="_blank" >10.1007/s00165-016-0413-z</a>

Jazyk výsledku

angličtina

Název v původním jazyce

On partial state matching

Popis výsledku v původním jazyce

During explicit software model checking, the tools spend a lot of time in state matching. This is implied not only by processing a huge number of states, but also by the fact that state representation is usually not small either. In this article, we present two dead variable analyses; applying them during the code-model-checking process results in size reduction of both state representation and explored state space itself. We implemented the analyses inside Java PathFinder and evaluate their impact in terms of memory and time reduction using several non-trivial benchmarks.

Název v anglickém jazyce

On partial state matching

Popis výsledku anglicky

During explicit software model checking, the tools spend a lot of time in state matching. This is implied not only by processing a huge number of states, but also by the fact that state representation is usually not small either. In this article, we present two dead variable analyses; applying them during the code-model-checking process results in size reduction of both state representation and explored state space itself. We implemented the analyses inside Java PathFinder and evaluate their impact in terms of memory and time reduction using several non-trivial benchmarks.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA14-11384S" target="_blank" >GA14-11384S: Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí</a><br>

Návaznosti

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

Rok uplatnění

2017

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 periodika

Formal Aspects of Computing

ISSN

0934-5043

e-ISSN

—

Svazek periodika

29

Číslo periodika v rámci svazku

5

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

27

Strana od-do

777-803

Kód UT WoS článku

000407933300001

EID výsledku v databázi Scopus

2-s2.0-85010778020