A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences

DOI10.1007/978-3-319-24953-7_6zbMATH Open1474.68051OpenAlexW2293338688MaRDI QIDQ3460547

David Mentré, Thibaut Girka, Yann Régis-Gianas

Publication date: 8 January 2016

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01238704/file/root.pdf

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Title not available (Why is that?)

Recommendations

• Generation of correctness conditions for imperative programs 👍 👎
• A means for the structural synthesis of programs 👍 👎
• Semantic synthesis of programs by matching compositions 👍 👎
• An approach to the inductive synthesis of programs 👍 👎
• Syntax-directed model checking of sequential programs 👍 👎
• From program verification to program synthesis 👍 👎
• Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs 👍 👎

This page was built for publication: A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences

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