Parameterized recursive refinement types for automated program verification

DOI10.1007/978-3-031-22308-2_18zbMath1524.68100MaRDI QIDQ6109429

Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato

Publication date: 28 July 2023

Published in: Static Analysis (Search for Journal in Brave)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• SMT-based model checking for recursive programs
• Refinement types for Haskell
• Automating relatively complete verification of higher-order functional programs
• Horn Clause Solvers for Program Verification
• Learning refinement types
• The size-change principle for program termination
• Low-level liquid types
• Abstract Refinement Types
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Automatic Termination Verification for Higher-Order Functional Programs
• On-Demand Refinement of Dependent Types
• Verification, Model Checking, and Abstract Interpretation
• ICE-based refinement type discovery for higher-order functional programs

This page was built for publication: Parameterized recursive refinement types for automated program verification