Verifying and synthesizing software with recursive functions (invited contribution)

DOI10.1007/978-3-662-43948-7_2MaRDI QIDQ5167727zbMATH OpenOpenAlexFDO

Authors Viktor Kuncak

Publication date 1 July 2014

Published in Automata, Languages, and Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• From program verification to program synthesis
• Automated synthesis of recursive programs from a logical specification
• Dafny: an automatic program verifier for functional correctness
• Sound and complete verification condition generator for functional recursive programs
• Deductive software verification: from pen-and-paper proofs to industrial tools

Cited in

(2)

• Unraveling recursion: compiling an IR with recursion to System F
• Synthesis of recursive ADT transformations from reusable templates

Describes a project that uses

Uses Software

• z3
• SIMPLIFY
• Scala
• Leon
• CVC4

This page was built for publication: Verifying and synthesizing software with recursive functions (invited contribution)

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