Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction

MORAVEC, Pavel. Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction. Online. 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. [citováno 2024-04-24]

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

• Originální 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

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.

Anotace č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