Verification of fine-grain concurrent programs

DOI10.1016/J.ENTCS.2008.04.010MaRDI QIDQ2870197zbMATH OpenOpenAlexWikidataFDO

Authors Tony Hoare

Publication date 17 January 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.04.010

zbMATH Keywords

Petri netsflowchartsfine-grain concurrent programsFloyd assertions

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 50008
• Verification of sequential and concurrent programs
• Specification and verification of concurrent programs through refinements
• Verifying concurrent programs against sequential specifications
• Verification of concurrent programs using trace abstraction refinement
• scientific article; zbMATH DE number 1032897
• Verification of concurrent systems with VerCors

Cited in

(16)

• Formal verification of out-of-order execution with incremental flushing
• Simulation Refinement for Concurrency Verification
• PBMC: Symbolic Slicing for the Verification of Concurrent Programs
• Verifying Concurrent Systems with Symbolic Execution
• Modular Safety Checking for Fine-Grained Concurrency
• Efficient verification of sequential and concurrent C programs
• Verification of sequential and concurrent programs
• Synthesizing and verifying multicore parallelism in categories of nested code graphs
• Guest editors' preface to special issue on interval temporal logics
• Highly dependable concurrent programming using design for verification
• Verification and refinement with fine-grained action-based concurrent objects
• Formal verification of language-based concurrent noninterference
• Verification, Model Checking, and Abstract Interpretation
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Caper
• Verification of Concurrent Programs on Weak Memory Models

This page was built for publication: Verification of fine-grain concurrent programs

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