PVS\#: streamlined tacticals for PVS

DOI10.1016/J.ENTCS.2006.10.057MaRDI QIDQ2864359zbMATH OpenOpenAlexFDO

Authors Florent Kirchner, César Muñoz

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.10.057

zbMATH Keywords

monadsstrategiesPVStacticsproof languagestacticals

Mathematics Subject Classification ID

Recommendations

• A Brief Overview of PVS
• Operational techniques in PVS -- a preliminary evaluation
• Fixpoints and search in PVS
• Towards robustness analysis using PVS
• scientific article; zbMATH DE number 1231633
• Tinycals: step by step tacticals
• Formalising confluence in PVS
• scientific article; zbMATH DE number 1136103

Cited in

(9)

• The proof monad
• A Brief Overview of PVS
• Tactics for hierarchical proof
• Tinycals: step by step tacticals
• A tactic language for refinement of state-rich concurrent specifications
• Proof tactics for a theory of state machines in a graphical environment
• A Proof-Theoretic Approach to Tactics
• Querying proofs
• A method for proving ITL theorem by using PVS

Describes a project that uses

Uses Software

• ALF
• PVS
• Coq

This page was built for publication: PVS\#: streamlined tacticals for PVS

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