$\xor$-OBDD in Symbolic Model Checking

ŘEHÁK, Vojtěch. $\xor$-OBDD in Symbolic Model Checking. In SOFSEM 2002: Student Research Forum. Milovy (Czech Republic): Slovak University of Technology, 2002, p. 41-46.

Basic information

Original name

$\xor$-OBDD in Symbolic Model Checking

Authors

ŘEHÁK, Vojtěch (203 Czech Republic, guarantor)

Edition

Milovy (Czech Republic), SOFSEM 2002: Student Research Forum, p. 41-46, 2002

Publisher

Slovak University of Technology

---

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

20206 Computer hardware and architecture

Country of publisher

Czech Republic

Confidentiality degree

is not subject to a state or trade secret

RIV identification code

RIV/00216224:14330/02:00006715

Organization unit

Faculty of Informatics

Keywords in English

Data structures; $\xor$-OBDD; symbolic model checking;

Tags

$\xor$-OBDD, data structures, symbolic model checking

Tags

Reviewed

---

Abstract

In the original language

We present a feasibility study of using $\oplus$-OBDD data structure in symbolic model checking (SMC). $\xor$-OBDD has been proposed as a more succinct modification of well known OBDD data structure which is of common use in nowadays SMC. We introduce three modifications of $\xor$-OBDD, analyze their respective efficiency, and present some experimental results based on implementations of $\xor$-OBDD within a symbolic model checker NuSMV.

---

Links

GA201/00/1023, research and development project	Name: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů Investor: Czech Science Foundation, Algorithms and tools for practical verification of concurrent systems.
MSM 143300001, plan (intention)	Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing