Rewriting models of boolean programs

Ahmed Bouajjani, Javier Esparza

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

14 Scopus citations


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 languageEnglish
Title of host publicationTerm Rewriting and Applications - 17th International Conference, RTA 2006, Proceedings
PublisherSpringer Verlag
Number of pages15
ISBN (Print)3540368345, 9783540368342
StatePublished - 2006
Externally publishedYes
Event17th International Conference on Term Rewriting and Applications, RTA 2006 - Seattle, WA, United States
Duration: 12 Aug 200614 Aug 2006

Publication series

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


Conference17th International Conference on Term Rewriting and Applications, RTA 2006
Country/TerritoryUnited States
CitySeattle, WA


Dive into the research topics of 'Rewriting models of boolean programs'. Together they form a unique fingerprint.

Cite this