Rewriting models of boolean programs

Ahmed Bouajjani; Javier Esparza

doi:10.1007/11805618_11

Rewriting models of boolean programs

Ahmed Bouajjani, Javier Esparza

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

14 Scopus citations

Abstract

We show that rewrite systems can be used to give semantics to imperative programs with boolean variables, a class of programs used in software model-checking as over- or underapproximations of real programs. We study the classes of rewrite systems induced by programs with different features like procedures, concurrency, or dynamic thread creation, and survey a number of results on their word problem and their symbolic reachability problem.

Original language	English
Title of host publication	Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings
Publisher	Springer Verlag
Pages	136-150
Number of pages	15
ISBN (Print)	3540368345, 9783540368342
DOIs	https://doi.org/10.1007/11805618_11
State	Published - 2006
Externally published	Yes
Event	17th International Conference on Term Rewriting and Applications, RTA 2006 - Seattle, WA, United States Duration: 12 Aug 2006 → 14 Aug 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4098 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Conference on Term Rewriting and Applications, RTA 2006
Country/Territory	United States
City	Seattle, WA
Period	12/08/06 → 14/08/06

Access to Document

10.1007/11805618_11

Cite this

Bouajjani, A., & Esparza, J. (2006). Rewriting models of boolean programs. In Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings (pp. 136-150). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4098 LNCS). Springer Verlag. https://doi.org/10.1007/11805618_11

@inproceedings{53cc687cd3674aadb676004f20cc91fe,

title = "Rewriting models of boolean programs",

abstract = "We show that rewrite systems can be used to give semantics to imperative programs with boolean variables, a class of programs used in software model-checking as over- or underapproximations of real programs. We study the classes of rewrite systems induced by programs with different features like procedures, concurrency, or dynamic thread creation, and survey a number of results on their word problem and their symbolic reachability problem.",

author = "Ahmed Bouajjani and Javier Esparza",

year = "2006",

doi = "10.1007/11805618_11",

language = "English",

isbn = "3540368345",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "136--150",

booktitle = "Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings",

note = "17th International Conference on Term Rewriting and Applications, RTA 2006 ; Conference date: 12-08-2006 Through 14-08-2006",

}

Bouajjani, A & Esparza, J 2006, Rewriting models of boolean programs. in Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4098 LNCS, Springer Verlag, pp. 136-150, 17th International Conference on Term Rewriting and Applications, RTA 2006, Seattle, WA, United States, 12/08/06. https://doi.org/10.1007/11805618_11

Rewriting models of boolean programs. / Bouajjani, Ahmed; Esparza, Javier.
Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings. Springer Verlag, 2006. p. 136-150 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4098 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Rewriting models of boolean programs

AU - Bouajjani, Ahmed

AU - Esparza, Javier

PY - 2006

Y1 - 2006

N2 - We show that rewrite systems can be used to give semantics to imperative programs with boolean variables, a class of programs used in software model-checking as over- or underapproximations of real programs. We study the classes of rewrite systems induced by programs with different features like procedures, concurrency, or dynamic thread creation, and survey a number of results on their word problem and their symbolic reachability problem.

AB - We show that rewrite systems can be used to give semantics to imperative programs with boolean variables, a class of programs used in software model-checking as over- or underapproximations of real programs. We study the classes of rewrite systems induced by programs with different features like procedures, concurrency, or dynamic thread creation, and survey a number of results on their word problem and their symbolic reachability problem.

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

U2 - 10.1007/11805618_11

DO - 10.1007/11805618_11

M3 - Conference contribution

AN - SCOPUS:33749404295

SN - 3540368345

SN - 9783540368342

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 136

EP - 150

BT - Term Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings

PB - Springer Verlag

T2 - 17th International Conference on Term Rewriting and Applications, RTA 2006

Y2 - 12 August 2006 through 14 August 2006

ER -

Rewriting models of boolean programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this