HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Towards more precise rewriting approximations

Abstract : To check a system, some verification techniques consider a set of terms I that represents the initial configurations of the system, and a rewrite system R that represents the system behavior. To check that no undesirable configuration is reached, they compute an over-approximation of the set of descendants (successors) issued from I by R, expressed by a tree language. Some techniques have been presented using regular tree languages, and more recently using non-regular languages to get better approximations: using context-free tree languages on the one hand, using synchronized tree languages on the other hand. In this paper, we merge these two approaches to get even better approximations: we compute an over-approximation of the descendants, using synchronized-context-free tree languages expressed by logic programs. We give several examples for which our procedure computes the descendants in an exact way, unlike former techniques.
Document type :
Journal articles
Complete list of metadata

Contributor : Pierre Réty Connect in order to contact the contributor
Submitted on : Friday, May 12, 2017 - 11:31:37 AM
Last modification on : Tuesday, March 29, 2022 - 2:32:48 PM


  • HAL Id : hal-01521746, version 1


Yohan Boichut, Jacques Chabin, Pierre Réty. Towards more precise rewriting approximations. Journal of Computer and System Sciences, Elsevier, 2019, 104, pp.131-148. ⟨hal-01521746⟩



Record views