Symbolic Reachability for Process Algebras with Recursive Data Types

DOI10.1007/978-3-540-85762-4_6MaRDI QIDQ5505595zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Stefan Blom, Jaco van de Pol

Publication date 27 January 2009

Published in Theoretical Aspects of Computing - ICTAC 2008 (Search for Journal in Brave)

Full work available at URL https://research.utwente.nl/en/publications/symbolic-reachability-for-process-algebras-with-recursive-data-types(aeb54cdd-d5b2-48b3-83cf-4a7222749107).html

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Reachability for finite-state process algebras using static analysis
• Reachability for finite-state process algebras using Horn clauses
• A symbolic approach to value-passing processes
• A logical reconstruction of reachability
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

Cites work

• A database approach to distributed state space generation
• Correct Hardware Design and Verification Methods
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 1796138 (Why is no real title available?)
• scientific article; zbMATH DE number 2090710 (Why is no real title available?)
• Model checking a cache coherence protocol of a Java DSM implementation
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Verification of a sliding window protocol in \(\mu\) CRL and PVS
• Verification of the link layer protocol of the IEEE-1394 serial bus (FireWire): An experiment with E-LOTOS

Cited in

(8)

• Reachability for finite-state process algebras using Horn clauses
• Reachability for finite-state process algebras using static analysis
• State space reduction of linear processes using control flow reconstruction
• scientific article; zbMATH DE number 1973989 (Why is no real title available?)
• A decision diagram operation for reachability
• Simplifying process parameters by unfolding algebraic data types
• Unfolding state variables improves model checking performance
• A linear process-algebraic format with data for probabilistic automata

Describes a project that uses

Uses Software

• E-LOTOS
• ATERM
• CADP

This page was built for publication: Symbolic Reachability for Process Algebras with Recursive Data Types

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