Theories for mechanical proofs of imperative programs

DOI10.1007/BF01211455zbMath0905.68138OpenAlexW2033367408MaRDI QIDQ1267030

Wim H. Hesselink

Publication date: 6 October 1998

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01211455

zbMATH Keywords

operational semanticsshared-memory concurrent programswhile-theorem

Mathematics Subject Classification ID

Uses Software

• ML
• LARCH
• HOL
• NQTHM
• UNITY
• Piton

Cites Work

• Refinement concepts formalised in higher order logic
• The derivation of systolic computations
• The verified incremental design of a distributed spanning tree algorithm: Extended abstract
• Myths about the mutual exclusion problem
• A verification system for concurrent programs based on the Boyer-Moore prover
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Theories for mechanical proofs of imperative programs