A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations

Yohan Boichut 1, 2 Pierre-Cyrille Heam 3
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In computer aided verification, the reachability problem is particularly relevant for safety analyses. Given a regular tree language L, a term t and a relation R, the reachability problem consists in deciding whether there exist a positive integer n and terms t0,t1,...,tn such that t0set membership, variantL, tn=t and for every 0less-than-or-equals, slanti
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/inria-00328487
Contributor : Pierre-Cyrille Heam <>
Submitted on : Friday, October 10, 2008 - 10:09:03 AM
Last modification on : Thursday, February 7, 2019 - 4:21:16 PM

Links full text

Identifiers

Citation

Yohan Boichut, Pierre-Cyrille Heam. A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations. Information Processing Letters, Elsevier, 2008, 108 (1), pp.1-2. ⟨10.1016/j.ipl.2008.03.012⟩. ⟨inria-00328487⟩

Share

Metrics

Record views

319