Sound and complete verification condition generator for functional recursive programs

DOI10.1007/978-3-7091-0794-2_11MaRDI QIDQ2912122zbMATH OpenOpenAlexFDO

Authors Nikolaj Popov, Tudor Jebelean

Publication date 14 September 2012

Published in Texts & Monographs in Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-7091-0794-2_11

zbMATH Keywords

completenessfunctional recursive programssoundnessverificationverification condition generator

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Mechanical verification of mutually recursive procedures
• Secure mechanical verification of mutually recursive procedures
• Automatic Termination Verification for Higher-Order Functional Programs
• Automated verification of recursive programs with pointers
• Verification Condition Generation Via Theorem Proving

Cited in

(4)

• Sound and complete concolic testing for higher-order functions
• Mechanical verification of mutually recursive procedures
• Verifying and synthesizing software with recursive functions (invited contribution)
• The correctness of a code generator for a functional language

This page was built for publication: Sound and complete verification condition generator for functional recursive programs

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