Automating relatively complete verification of higher-order functional programs

DOI10.1145/2429069.2429081MaRDI QIDQ2931785zbMATH OpenOpenAlexFDO

Authors Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi

Publication date 27 November 2014

Published in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://tsukuba.repo.nii.ac.jp/record/29119/files/POPL2013.pdf

zbMATH Keywords

higher-order programsrelative completenesssoftware model checkingtype inference

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Modular verification of higher-order functional programs
• Verifying higher-order functions with tree automata
• Automatic Termination Verification for Higher-Order Functional Programs
• Model checking higher-order programs
• Automata-based abstraction for automated verification of higher-order tree-processing programs

Cited in

(23)

• Verifying higher-order functions with tree automata
• Sound and complete concolic testing for higher-order functions
• Efficient verification of imperative programs using auto2
• Executing and verifying higher-order functional-imperative programs in Maude
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• A relational framework for higher-order shape analysis
• Temporal verification of higher-order functional programs
• Context dependent procedures and computed types in \texttt{VeriFun}
• Combining interactive and automatic reasoning in first order theories of functional programs
• Compositional and lightweight dependent type inference for ML
• Modular verification of higher-order functional programs
• Certifying and Reasoning on Cost Annotations of Functional Programs
• Automata-based abstraction for automated verification of higher-order tree-processing programs
• The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification
• Automatic Termination Verification for Higher-Order Functional Programs
• Automating Side Conditions in Formalized Partial Functions
• scientific article; zbMATH DE number 970706 (Why is no real title available?)
• ICE-based refinement type discovery for higher-order functional programs
• Automating the functional correspondence between higher-order evaluators and abstract machines
• Parameterized recursive refinement types for automated program verification
• Automated synthesis of functional programs with auxiliary functions
• An overview of the HFL model checking project
• On recursion-free Horn clauses and Craig interpolation

This page was built for publication: Automating relatively complete verification of higher-order functional programs

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