Program synthesis using dual interpretation

DOI10.1007/978-3-319-21401-6_33MaRDI QIDQ3454117zbMATH OpenOpenAlexFDO

Authors Adrià Gascón, Bruno Dutertre, Ashish Tiwari

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://www.pure.ed.ac.uk/ws/files/24676075/cade2015.pdf

zbMATH Keywords

abstract interpretationencryptionexists-forall solvingprogram synthesisSMT solvingsyntax-guided synthesis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data encryption (aspects in computer science) (68P25)

Recommendations

• Look for the proof to find the program: decorated-component-based program synthesis
• From program verification to program synthesis
• Component-based synthesis for complex APIs
• Programmable program synthesis
• scientific article; zbMATH DE number 4084990

Cites work

• A theory for program and data type specification
• Automated verification of block cipher modes of operation, an improved method
• scientific article; zbMATH DE number 1088907 (Why is no real title available?)
• The shadow knows: refinement and security in sequential programs

Cited in

(7)

• Look for the proof to find the program: decorated-component-based program synthesis
• Refutation-based synthesis in SMT
• Using program synthesis for program analysis
• Satisfiability checking: theory and applications
• Solving program sketches with large integer values
• Component-based synthesis for complex APIs
• Program Synthesis in Saturation

Describes a project that uses

Uses Software

• Yices

This page was built for publication: Program synthesis using dual interpretation

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