Translation Templates to Support Strategy Development in PVS

DOI10.1016/j.entcs.2007.01.057zbMath1277.68243OpenAlexW2038609413MaRDI QIDQ2864361

Hongping Lim, Myla M. Archer

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.2007.01.057

zbMATH Keywords

templateshybrid automatatimed automataI/O automatastrategiesmechanical theorem provingspecification translation

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• LARCH
• Uppaal
• TAME

Cites Work

• Formal stystems specification. The RPC-memory specification case study
• TAME: Using PVS strategies for special-purpose theorem proving
• Uppaal in a nutshell
• Proving invariants of I/O automata with TAME
• Formal Modeling and Analysis of Timed Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Translation Templates to Support Strategy Development in PVS