Theories for mechanical proofs of imperative programs

DOI10.1007/BF01211455MaRDI QIDQ1267030zbMATH OpenOpenAlexFDO

Authors W. 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

Recommendations

• Publication:4944851
• Mechanical proofs about computer programs
• Imperative programs as proofs via game semantics
• scientific article; zbMATH DE number 2217740
• scientific article; zbMATH DE number 2079677
• Proof Abstraction for Imperative Languages
• scientific article; zbMATH DE number 3916263
• Mechanized semantics
• Proof methods for corecursive programs
• scientific article; zbMATH DE number 4120164

Cites work

• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 50008 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 732976 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• A verification system for concurrent programs based on the Boyer-Moore prover
• Myths about the mutual exclusion problem
• Refinement concepts formalised in higher order logic
• The derivation of systolic computations
• The verified incremental design of a distributed spanning tree algorithm: Extended abstract

Cited in

(6)

• Characteristic formulae for the verification of imperative programs
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• A verification system for concurrent programs based on the Boyer-Moore prover
• Mechanized semantics
• A FOOLish encoding of the next state relations of imperative programs
• Proving correctness of imperative programs by linearizing constrained Horn clauses

Describes a project that uses

Uses Software

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

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

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