Automatic and hierarchical verification for concurrent systems

DOI10.1007/BF02945312MaRDI QIDQ2277847zbMATH OpenOpenAlexFDO

Authors Xudong Zhao, Yulin Feng

Publication date 1990

Published in Journal of Computer Science and Technology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf02945312

zbMATH Keywords

Petri netsbranching time temporal logiccorrectness of concurrent systems

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Verification of concurrent programs: The automata-theoretic framework
• Automatic verification of concurrent systems using a formula-based compositional approach
• Automatic verification of concurrent stochastic systems
• Verification of concurrent systems with VerCors
• scientific article; zbMATH DE number 1140074
• scientific article; zbMATH DE number 2086795
• Automatic verification for a class of distributed systems
• Verifying Concurrent Systems with Symbolic Execution

Cites work

• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• Automatic Verification of Sequential Circuits Using Temporal Logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Hierarchical verification of asynchronous circuits using temporal logic
• The temporal logic of branching time
• “Sometimes” and “not never” revisited

Cited in

(12)

• scientific article; zbMATH DE number 1390251 (Why is no real title available?)
• Verifying Concurrent Systems with Symbolic Execution
• Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
• Automated Verification of Concurrent Search Structures
• scientific article; zbMATH DE number 4145305 (Why is no real title available?)
• Compositional verification of asynchronous concurrent systems using CADP
• Automatic Verification of Bossa Scheduler Properties
• Interactive verification of concurrent systems using symbolic execution
• Automatic generation of verified concurrent hardware using VHDL
• On the role of automated theorem proving in the compile-time derivation of concurrency
• A formal methodology using attributed grammars for multiprocessing-system software development. II. Validation
• Caper

This page was built for publication: Automatic and hierarchical verification for concurrent systems

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