The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification

DOI10.1007/978-3-540-76637-7_2MaRDI QIDQ3498430zbMATH OpenOpenAlexFDO

Authors Paritosh Shroff, Christian Skalka, Scott F. Smith

Publication date 15 May 2008

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-76637-7_2

zbMATH Keywords

0CFAhigher-orderprogram analysisprogram verification

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Automating relatively complete verification of higher-order functional programs
• Static complexity analysis of higher order programs
• Automata-based abstraction for automated verification of higher-order tree-processing programs
• Logic-flow analysis of higher-order programs
• Modular verification of higher-order functional programs

Cites work

• Combining programming with theorem proving
• Grammar Analysis and Parsing by Abstract Interpretation
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic-flow analysis of higher-order programs
• Programming Languages and Systems
• The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification

Cited in

(2)

• Crowfoot: A Verifier for Higher-Order Store Programs
• The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification

Describes a project that uses

Uses Software

• ACL2
• Isabelle/HOL

This page was built for publication: The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification

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