GenProg Project

Introduction

GenProg is an advanced code generation tool developed to convert verified Coq models into efficient and reliable C code. Built on the language of DPIA (Data Parallel Idealised Algol), GenProg facilitates the seamless translation of high-level functional models into practical, executable programs.
This tool is particularly valuable for applications requiring stringent correctness guarantees, such as flight control systems, ensuring the consistency and reliability of the generated code. GenProg is an essential resource for developers and researchers working on high-assurance systems, providing a robust solution for code generation from formally verified models.

Resources

Below are main links of this project: