Publications

BibTex format

@inproceedings{Hückelheim:2017:10.1145/3145344.3145488,
author = {Hückelheim, JC and Luo, Z and Luporini, F and Kukreja, N and Lange, M and Gorman, G and Siegel, S and Dwyer, M and Hovland, P},
doi = {10.1145/3145344.3145488},
publisher = {ACM},
title = {Towards self-verification in finite difference code generation},
url = {http://dx.doi.org/10.1145/3145344.3145488},
year = {2017}
}

Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - Code generation from domain-specific languages is becoming increasingly popular as a method to obtain optimised low-level code that performs well on a given platform and for a given problem instance. Ensuring the correctness of generated codes is crucial. At the same time, testing or manual inspection of the code is problematic, as the generated code can be complex and hard to read. Moreover, the generated code may change depending on the problem type, domain size, or target platform, making conventional code review or testing methods impractical. As a solution, we propose the integration of formal verification tools into the code generation process. We present a case study in which the CIVL verification tool is combined with the Devito finite difference framework that generates optimised stencil code for PDE solvers from symbolic equations. We show a selection of properties of the generated code that can be automatically specified and verified during the code generation process. Our approach allowed us to detect a previously unknown bug in the Devito code generation tool.
AU  - Hückelheim,JC
AU  - Luo,Z
AU  - Luporini,F
AU  - Kukreja,N
AU  - Lange,M
AU  - Gorman,G
AU  - Siegel,S
AU  - Dwyer,M
AU  - Hovland,P
DO  - 10.1145/3145344.3145488
PB  - ACM
PY  - 2017///
TI  - Towards self-verification in finite difference code generation
UR  - http://dx.doi.org/10.1145/3145344.3145488
UR  - http://hdl.handle.net/10044/1/51686
ER  -

Download

Fabio Luporini

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)