A mechanized proof environment for the convenient computations proof method

DOI10.1023/A:1024746015231MaRDI QIDQ1426938zbMATH OpenOpenAlexFDO

Authors Marcelo Glusman, Shmuel Katz

Publication date 15 March 2004

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1024746015231

zbMATH Keywords

formal verificationPVSconvenient computationsdeductive theorem provingproof environment

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 2102718
• scientific article; zbMATH DE number 1630111
• A verification system for concurrent programs based on the Boyer-Moore prover
• scientific article; zbMATH DE number 4060694
• A calculus of atomic actions

Cited in

(3)

• A mechanized proof system of the third generation calculus in Coq
• Cones and foci: A mechanical framework for protocol verification
• scientific article; zbMATH DE number 2102718 (Why is no real title available?)

Describes a project that uses

Uses Software

• PVS

This page was built for publication: A mechanized proof environment for the convenient computations proof method

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