Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions

DOI10.1109/TAC.2013.2248255MaRDI QIDQ5353290zbMATH OpenOpenAlexFDO

Authors Robi Malik, Ryan J. Leduc

Publication date 8 September 2017

Published in IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/tac.2013.2248255

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Discrete event control/observation systems (93C65)

Recommendations

• Compositional verification of the generalized nonblocking property using abstraction and canonical automata
• On the computation of counterexamples in compositional nonblocking verification
• A framework for compositional nonblocking verification of extended finite-state machines
• Compositional verification of termination-preserving refinement of concurrent programs
• Concurrency verification. Introduction to compositional and noncompositional methods
• Automata, Languages and Programming
• Compositional verification of concurrent systems by combining bisimulations
• Compositional verification of asynchronous concurrent systems using CADP
• scientific article; zbMATH DE number 1897216
• A system for compositional verification of asynchronous objects

Cited in

(7)

• A framework for compositional nonblocking verification of extended finite-state machines
• Compositional Bitvector Analysis for Concurrent Programs with Nested Locks
• Hierarchical modelling of manufacturing systems using discrete event systems and the conflict preorder
• Progressive events in supervisory control and compositional verification
• A survey on compositional algorithms for verification and synthesis in supervisory control
• Compositional verification of the generalized nonblocking property using abstraction and canonical automata
• On the computation of counterexamples in compositional nonblocking verification

This page was built for publication: Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions

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