TAGED Approximations for Temporal Properties Model-Checking

DOI10.1007/978-3-642-02979-0_17zbMath1248.68323OpenAlexW1551595134MaRDI QIDQ3637350

Roméo Courbis, Pierre-Cyrille Héam, Olga Kouchnarenko

Publication date: 9 July 2009

Published in: Implementation and Application of Automata (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02979-0_17

Mathematics Subject Classification ID

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

Uses Software

• Timbuk
• Java PathFinder

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability analysis over term rewriting systems
• Linear generalized semi-monadic rewrite systems effectively preserve recognizability
• Conditional rewriting logic as a unified model of concurrency
• Tree automata with one memory set constraints and cryptographic protocols
• Automata for reduction properties solving
• Counterexample-guided abstraction refinement for symbolic model checking
• The Temporal Logic of Rewriting: A Gentle Introduction
• Finer Is Better: Abstraction Refinement for Rewriting Approximations
• Tree Automata with Global Constraints
• Tree Automata with Equality Constraints Modulo Equational Theories
• Term Rewriting and All That
• LTL model checking for security protocols
• Unranked Tree Automata with Sibling Equalities and Disequalities
• Rewriting Approximations for Fast Prototyping of Static Analyzers
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Automata, Languages and Programming
• Towards an Efficient Implementation of Tree Automata Completion

This page was built for publication: TAGED Approximations for Temporal Properties Model-Checking