PVS\#: streamlined tacticals for PVS

DOI10.1016/J.ENTCS.2006.10.057zbMATH Open1277.68242OpenAlexW2169789783MaRDI QIDQ2864359FDOQ2864359

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

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

zbMATH Keywords

monadsstrategiesPVStacticsproof languagestacticals

Mathematics Subject Classification ID

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (9)

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

Uses Software

• Coq
• PVS
• ALF

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)