PVS as a proof obligation generator

DOI10.1007/978-3-032-13711-1_8MaRDI QIDQ7285343zbMATH OpenFDO

Authors Natarajan Shankar

Publication date 19 June 2026

Full work available at URL https://doi.org/10.1007/978-3-032-13711-1_8

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cites work

• An axiomatic proof technique for parallel programs
• Embedding differential dynamic logic in PVS
• Formal methods for components and objects. 4th international symposium, FMCO 2005, Amsterdam, The Netherlands, November 1--4, 2005. Revised lectures.
• Formal techniques in real-time and fault-tolerant systems. 3rd international symposium organized jointly with the working group provably correct systems -- ProCoS, Lübeck, Germany, September 19--23, 1994. Proceedings
• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 1863391 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic

This page was built for publication: PVS as a proof obligation generator

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