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

branching time temporal logiccorrectness of concurrent systemsPetri nets

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

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

Cited in

(13)

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

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)