Algebraic implementation of model checking algorithms

Theodor Rus; Erick Van Wyk

doi:10.1142/9789812708472_0014

Algebraic implementation of model checking algorithms

Research output: Chapter in Book/Report/Conference proceeding › Chapter

Abstract

The following sections are included: Introduction, Algebraic Specification of CTL, Algebraic Implementation of a Model Checker, Structure of an Algebraic Compiler, The Macro Processor Generating Satisfiability Sets, Generating a Model Checker Program, Implementing the Macro Processor formula, Conclusions.

Original language	English (US)
Title of host publication	Real-time Systems
Subtitle of host publication	Modeling, Design And Applications
Publisher	World Scientific Publishing Co.
Pages	309-327
Number of pages	19
ISBN (Electronic)	9789812708472
DOIs	https://doi.org/10.1142/9789812708472_0014
State	Published - Jan 1 2007
Externally published	Yes

Bibliographical note

Publisher Copyright:
© 2007 by World Scientific Publishing Co. Pte. Ltd.

Publisher link

10.1142/9789812708472_0014

Find It

Find It at U of M Libraries

Cite this

@inbook{9e6ea96ca7cf4f84866ee1621900e686,

title = "Algebraic implementation of model checking algorithms",

abstract = "The following sections are included: Introduction, Algebraic Specification of CTL, Algebraic Implementation of a Model Checker, Structure of an Algebraic Compiler, The Macro Processor Generating Satisfiability Sets, Generating a Model Checker Program, Implementing the Macro Processor formula, Conclusions.",

author = "Theodor Rus and {Van Wyk}, Erick",

note = "Publisher Copyright: {\textcopyright} 2007 by World Scientific Publishing Co. Pte. Ltd.",

year = "2007",

month = jan,

day = "1",

doi = "10.1142/9789812708472_0014",

language = "English (US)",

pages = "309--327",

booktitle = "Real-time Systems",

publisher = "World Scientific Publishing Co.",

}

TY - CHAP

T1 - Algebraic implementation of model checking algorithms

AU - Rus, Theodor

AU - Van Wyk, Erick

PY - 2007/1/1

Y1 - 2007/1/1

N2 - The following sections are included: Introduction, Algebraic Specification of CTL, Algebraic Implementation of a Model Checker, Structure of an Algebraic Compiler, The Macro Processor Generating Satisfiability Sets, Generating a Model Checker Program, Implementing the Macro Processor formula, Conclusions.

AB - The following sections are included: Introduction, Algebraic Specification of CTL, Algebraic Implementation of a Model Checker, Structure of an Algebraic Compiler, The Macro Processor Generating Satisfiability Sets, Generating a Model Checker Program, Implementing the Macro Processor formula, Conclusions.

UR - http://www.scopus.com/inward/record.url?scp=85115721414&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85115721414&partnerID=8YFLogxK

U2 - 10.1142/9789812708472_0014

DO - 10.1142/9789812708472_0014

M3 - Chapter

AN - SCOPUS:85115721414

SP - 309

EP - 327

BT - Real-time Systems

PB - World Scientific Publishing Co.

ER -

Algebraic implementation of model checking algorithms

Abstract

Bibliographical note

Publisher link

Find It

Other files and links

Fingerprint

Cite this