A method for proving ITL theorem by using PVS

MaRDI QIDQ3051901zbMATH OpenFDO

Authors Yiran Wang, Qinglei Zhou, Wei-jun Zhu

Publication date 5 November 2010

zbMATH Keywords

interval temporal logicprototype verification systemtheorem proving

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• \textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system
• scientific article; zbMATH DE number 1614710
• Proof assistance for real-time systems using an interactive theorem prover
• A proof system for a unified temporal logic
• PVS\#: streamlined tacticals for PVS

Describes a project that uses

Uses Software

• PVS

This page was built for publication: A method for proving ITL theorem by using PVS

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