Embedded domain specific verifiers

DOI10.1007/978-3-031-22337-2_26MaRDI QIDQ6113993zbMATH OpenOpenAlexFDO

Authors Ranjit Jhala

Publication date 10 August 2023

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

Full work available at URL https://doi.org/10.1007/978-3-031-22337-2_26

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Refinement types for Haskell
• Theory refinement for program verification
• Parameterized recursive refinement types for automated program verification
• Dafny: an automatic program verifier for functional correctness
• A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking

Cites work

• An axiomatic basis for computer programming
• Bounded refinement types
• Guarded commands, nondeterminacy and formal derivation of programs
• 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
• LMS-Verify: abstraction without regret for verified systems programming
• Low-level liquid types
• Refinement for structured concurrent programs
• Refinement types for Haskell
• Refinement types for Ruby
• Simplify: a theorem prover for program checking

This page was built for publication: Embedded domain specific verifiers

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