The PROSPER toolkit

DOI10.1007/3-540-46419-0_7MaRDI QIDQ2729073zbMATH OpenFDO

Authors Louise A. Dennis, Graham P. Collins, Michael Norrish, Konrad Slind, Graham Robinson, Richard Boulton, Mike Gordon, Thomas F. Melham

Publication date 6 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46419-0_7

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• scientific article; zbMATH DE number 2086601
• System description: Embedding verification into Microsoft Excel
• scientific article; zbMATH DE number 2080773
• Web services as a new approach to distributing and coordinating semantics-based verification toolkits
• scientific article; zbMATH DE number 2087637

Cited in

(10)

• Integrating external deduction tools with ACL2
• PROSPER
• Hidden verification for computational mathematics
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools
• Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
• Linear Arithmetic with Stars
• scientific article; zbMATH DE number 2086601 (Why is no real title available?)
• Combining Isabelle and QEPCAD-B in the Prover’s Palette
• Faithful Logic Embeddings in HOL — Deep and Shallow (Isabelle/HOL dataset)
• Providing a formal linkage between MDG and HOL

This page was built for publication: The PROSPER toolkit

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