Using forward reachability analysis for verification of lossy channel systems

DOI10.1023/B:FORM.0000033962.51898.1azbMath1073.68675OpenAlexW2053229198MaRDI QIDQ1878928

Parosh Aziz Abdulla, Bengt Jonsson, Ahmed Bouajjani, Aurore Collomb-Annichini

Publication date: 9 September 2004

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/b:form.0000033962.51898.1a

zbMATH Keywords

automatamodel checkinginfinite-state systemsprotocol verificationsimple regular expressions

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (31)

Zeno, Hercules, and the Hydra ⋮ Reachability problems on reliable and lossy queue automata ⋮ Ideal Abstractions for Well-Structured Transition Systems ⋮ Forward analysis and model checking for trace bounded WSTS ⋮ An Approach to Computing Downward Closures ⋮ Learning from positive and negative examples: dichotomies and parameterized algorithms ⋮ Handling infinitely branching well-structured transition systems ⋮ On the state complexity of closures and interiors of regular languages with subwords and superwords ⋮ A Trichotomy for Regular Trail Queries ⋮ Applying abstract acceleration to (co-)reachability analysis of reactive programs ⋮ When Is Reachability Intrinsically Decidable? ⋮ Unnamed Item ⋮ Mixing Lossy and Perfect Fifo Channels ⋮ On the Reachability Analysis of Acyclic Networks of Pushdown Systems ⋮ The Ideal Approach to Computing Closed Subsets in Well-Quasi-orderings ⋮ Well-Quasi Orders and Hierarchy Theory ⋮ Verification of Flat FIFO Systems ⋮ Forward Analysis and Model Checking for Trace Bounded WSTS ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness ⋮ On the termination and structural termination problems for counter machines with incrementing errors ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs ⋮ Forward analysis for WSTS, part I: completions ⋮ Non axiomatisability of positive relation algebras with constants, via graph homomorphisms ⋮ Unnamed Item ⋮ \(\pi\)-calculus with noisy channels ⋮ Verification of programs with half-duplex communication ⋮ Coding Mobile Synchronizing Petri Nets into Rewriting Logic ⋮ Generalized Post embedding problems

Uses Software

• TREX
• InVeSt

This page was built for publication: Using forward reachability analysis for verification of lossy channel systems