Composing leads-to properties

DOI10.1016/S0304-3975(98)00233-3MaRDI QIDQ1575647zbMATH OpenFDO

Authors N. Delaunay

Publication date 21 August 2000

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

zbMATH Keywords

verificationcommutativityparallel compositionleads-to

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Eliminating disjunctions of leads-to properties
• scientific article; zbMATH DE number 2087508
• scientific article; zbMATH DE number 1759496
• scientific article; zbMATH DE number 1612492

Cites work

• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 3938541 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• A predicate transformer for progress
• Composition of assumption-commitment specifications in a UNITY style
• Data refinement of mixed specifications: A generalization of UNITY
• Eliminating the substitution axiom from UNITY logic
• Extensions of the UNITY methodology: compositionality, fairness and probability in parallelism
• Predicate transformers for reasoning about concurrent computation
• Reduction
• Specifying modules to satisfy interfaces: A state transition system approach
• Tentative steps toward a development method for interfering programs

Cited in

(1)

• Invariants, composition, and substitution

Describes a project that uses

Uses Software

• UNITY

This page was built for publication: Composing leads-to properties

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