Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction

MORAVEC, Pavel. Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction. In 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Mikulov, Czech Republic: FI MU Report Series, 2006, s. 129-136.

Základní údaje

Originální název

Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction

Název česky

Experimentální porovnání algoritmů ověřujících proviso pro redukci pomocí reprezentantů

Autoři

MORAVEC, Pavel (203 Česká republika, garant)

Vydání

Mikulov, Czech Republic, 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), s. 129-136, 2006

Nakladatel

FI MU Report Series

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/06:00015445

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

model checking; partial order reduction; proviso checking

Štítky

Model checking, partial order reduction, proviso checking

---

Anotace

V originále

In this paper we have summed up all known algorithms checking proviso for partial order reduction in LTL model checking. All mentioned algorithms have been implemented and experimentally evaluated on a large collection of models. Experiments mostly confirmed theoretical expectations of algorithms comparison.

Česky

Článek shrnuje všechny známé algoritmy pro ověřování provisa u redukce pomocí reprezentantů pro ověřování LTL vlastností modelu. Všechny zmíněné algoritmy byly implementovány a experimentálně vyhodnoceny na rozsáhlé sbírce modelů. Experimenty ve většině případů potvrdily teoretická očekávání z porovnání algoritmů.

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
GD102/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky