A theoretical limit for safety verification techniques with regular fix-point computations

DOI10.1016/J.IPL.2008.03.012MaRDI QIDQ963463zbMATH OpenOpenAlexFDO

Authors Yohan Boichut, Pierre-Cyrille Héam

Publication date 19 April 2010

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00204579/file/RR-6411.pdf

zbMATH Keywords

formal methodsregular tree languagesreachability problemtheoretical limit

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Reachability problems on regular ground tree rewriting graphs
• Reachability Analysis with State-Compatible Automata
• Reachability in conditional term rewriting systems
• Approximation-based tree regular model-checking
• Completeness of tree automata completion

Cites work

• scientific article; zbMATH DE number 1614701 (Why is no real title available?)
• scientific article; zbMATH DE number 794243 (Why is no real title available?)
• Abstract regular tree model checking
• Decidable approximations of term rewriting systems
• Handling Algebraic Properties in Automatic Analysis of Security Protocols
• Reachability analysis over term rewriting systems
• Regular sets of descendants by leftmost strategy
• Rewriting Approximations for Fast Prototyping of Static Analyzers

Cited in

(9)

• Termination criteria for tree automata completion
• How to Tackle Integer Weighted Automata Positivity
• Towards more precise rewriting approximations
• An Improved Safety Solver in Go Using Partial Regions
• Undecidability of safety for the schematic protection model with cyclic creates
• Synchronized tree languages for reachability in non-right-linear term rewrite systems
• Verifying relative safety, accuracy, and termination for program approximations
• HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA
• SAT-based automated completion for reachability analysis

Describes a project that uses

Uses Software

• Timbuk

This page was built for publication: A theoretical limit for safety verification techniques with regular fix-point computations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q963463)