Refinement-Based Verification of Communicating Unstructured Code

DOI10.1007/978-3-319-41591-8_5zbMATH Open1390.68185OpenAlexW2507015529MaRDI QIDQ4571128FDOQ4571128

Authors: Nils Jähnig, Thomas Göthel, Sabine Glesner 

Publication date: 6 July 2018

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL: https://depositonce.tu-berlin.de/handle/11303/10899

Recommendations

• A unified approach of program verification
• Effective generation of verification conditions for non-deterministic unstructured programs
• Verification of programs with half-duplex communication
• Specification and verification of concurrent programs through refinements
• Verifying Parallel Programs with Dynamic Communication Structures
• Verifying parallel programs with dynamic communication structures
• Trace Abstraction-Based Verification for Uninterpreted Programs
• Verifying programs with unreliable channels

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Communicating sequential processes
• FDR3 -- a modern refinement checker for CSP
• Theories of Programming Languages
• Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
• A compositional natural semantics and Hoare logic for low-level languages

Cited In (1)

• Verification of programs with half-duplex communication

Uses Software

• FDR3

This page was built for publication: Refinement-Based Verification of Communicating Unstructured Code

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