Proof movie -- a proof with the Boyer-Moore prover

DOI10.1007/BF01211302zbMath0798.68032MaRDI QIDQ2366695

Debora Weber-Wulff

Publication date: 18 August 1993

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

zbMATH Keywords

correctnessautomatic theorem provingcompiler verificationBoyer-Moore prover

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• NQTHM
• Kit
• Piton

Cites Work

• A mechanical proof of the Church-Rosser theorem
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof movie -- a proof with the Boyer-Moore prover