Refinement-Based Verification of Communicating Unstructured Code

DOI10.1007/978-3-319-41591-8_5MaRDI QIDQ4571128zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(1)

• Verification of programs with half-duplex communication

Describes a project that uses

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)