Theories for mechanical proofs of imperative programs
From MaRDI portal
Publication:1267030
DOI10.1007/BF01211455zbMath0905.68138MaRDI QIDQ1267030
Publication date: 6 October 1998
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Uses Software
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