Fixpoints and Search in PVS

DOI10.1007/978-3-642-13010-6_5zbMath1186.68302OpenAlexW1579364886MaRDI QIDQ3558967

Natarajan Shankar

Publication date: 11 May 2010

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

Full work available at URL: https://doi.org/10.1007/978-3-642-13010-6_5

Mathematics Subject Classification ID

Nonnumerical algorithms (68W05) Complete lattices, completions (06B23) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

PVS

Uses Software

• Isabelle
• ML
• Isabelle/HOL
• HOL
• Nuprl

Cites Work

• A note on two problems in connexion with graphs
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Isabelle/HOL. A proof assistant for higher-order logic
• Set theory for verification. II: Induction and recursion
• A lattice-theoretical fixpoint theorem and its applications
• The B-Book
• Planning Algorithms
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Fixpoints and Search in PVS