Parallel Partial Order Reduction with Topological Sort Proviso

• Název česky: Paralelní redukce částečného uspořádání s využitím topologického třídění
• Autoři: BARNAT Jiří; BRIM Luboš; ROČKAI Petr
• Rok publikování: 2010
• Druh: Článek ve sborníku
• Konference: Software Engineering and Formal Methods (SEFM 2010)
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: LTL Model Checking; Partial Order Reduction; Parallel and Distributed Processing; DiVinE
• Popis: Redukce částečného uspořádání a počítáni v distribuované paměti jsou dvě klíčové techniky pro boj se stavovou explozí v kontextu enumerativní verifikace. Hlavním výsledkem této práce je nový paralelní algoritmus pro výpočet množiny vrcholů pokrývající všechny cykly v grafu, který umožňuje uspokojivou integraci obou klíčových technik. Nová technika byla implementována v rámci nástroje DiVinE.

Související projekty

• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy
• Verifikace a analýza velmi velkých počítačových systémů
• Automatizovaná formální verifikace s využitím soudobého hardware
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace