\textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system

DOI10.1007/B12001MaRDI QIDQ5305658zbMATH OpenOpenAlexFDO

Authors Amir Pnueli, Tamarah Arons

Publication date 23 March 2010

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

Full work available at URL https://doi.org/10.1007/b12001

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 4153903
• Sound verification procedures for temporal properties of infinite-state systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• An LTL proof system for runtime verification
• Publication:4490758

Cited in

(8)

• TLPVS
• Verification of Boolean programs with unbounded thread creation
• A method for proving ITL theorem by using PVS
• Temporal Verification of Fault-Tolerant Protocols
• Explicit fair scheduling for dynamic control
• A theorem prover based approach for SAT-based model checking certification
• Concurrent IMP
• Sound verification procedures for temporal properties of infinite-state systems

This page was built for publication: \textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system

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