scientific article

zbMath1009.68020MaRDI QIDQ2768503

Ulrich Hannemann, Job Zwiers, J. J. M. Hooman, Mannes Poel, Yassine Lakhneche, Frank S. de Boer, Willem Paul de Roever

Publication date: 3 February 2002

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

program transformation temporal logic transition system soundness Hoare logic program verification concurrent program compositional reasoning semantic completeness shared variable inductive assertion absence of deadlock assumption commitment communication-closed-layers paradigm noncompositional proof method rely-guarantee method synchronous message

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (54)

Local Symmetry and Compositional Verification ⋮ Mechanizing a process algebra for network protocols ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos ⋮ Compositional Reasoning ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ Theory and methodology of assumption/commitment based system interface specification and architectural contracts ⋮ An application of temporal projection to interleaving concurrency ⋮ Convolution and concurrency ⋮ Splitting atoms safely ⋮ On Rely-Guarantee Reasoning ⋮ Automated compositional proofs for real-time systems ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Compositional reasoning about active objects with shared futures ⋮ Just testing ⋮ A system for compositional verification of asynchronous objects ⋮ Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification ⋮ Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language ⋮ Formal communication elimination and sequentialization equivalence proofs for distributed system models ⋮ Compositional verification of sequential programs with procedures ⋮ Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs ⋮ Verifying correctness of persistent concurrent data structures: a sound and complete method ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Compositional reasoning using intervals and time reversal ⋮ A framework for compositional verification of security protocols ⋮ Proving linearizability with temporal logic ⋮ Elucidating concurrent algorithms via layers of abstraction and reification ⋮ Compositional CSP Traces Refinement Checking ⋮ Assumption-Commitment Support for CSP Model Checking ⋮ Semantic models of a timed distributed dataspace architecture ⋮ A unified approach of program verification ⋮ A Bibliography of Willem-Paul de Roever ⋮ Synchronous Message Passing: On the Relation between Bisimulation and Refusal Equivalence ⋮ Meanings of Model Checking ⋮ Encoding fairness in a synchronous concurrent program algebra ⋮ Automated Compositional Reasoning of Intuitionistically Closed Regular Properties ⋮ Fifty years of Hoare's logic ⋮ Contracts for BIP: Hierarchical Interaction Models for Compositional Verification ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Derivation of concurrent programs by stepwise scheduling of Event-B models ⋮ Towards a Thread-Local Proof Technique for Starvation Freedom ⋮ A Coinductive Calculus for Asynchronous Side-Effecting Processes ⋮ AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES ⋮ Proving Reachability-Logic Formulas Incrementally ⋮ Fine-grained concurrency with separation logic ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers ⋮ Local proofs for global safety properties ⋮ Assumption-commitment support for CSP model checking ⋮ A verification-driven framework for iterative design of controllers ⋮ Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems ⋮ Formal Sequentialization of Distributed Systems via Program Rewriting

This page was built for publication: