Name
Abstract | ||
|---|---|---|
GPUs are now a mainstream compute device. They are widely used to render images on medical devices. Today, it has become impossible to imagine AI without them. To build confidence on the accuracy of rendering images and complex calculations, it is essential to consider formalizing the behaviour of GPU Instruction Set Architecture (ISA) at the assembly language level. In this paper, we present the formalization of GPU shader programs. We prove some properties of shader programs with respect to operational semantics of our formal model. We use Coq to mechanize the formalization of our model and proofs.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3299771.3299798 | Proceedings of the 12th Innovations on Software Engineering Conference (formerly known as India Software Engineering Conference) |
Keywords | Field | DocType |
Coq, Formal Methods, GPU, Operational Semantics, Theorem Proving | Operational semantics,Programming language,Instruction set,Automated theorem proving,Assembly language,Theoretical computer science,Mathematical proof,Engineering,Formal methods,Shader,Rendering (computer graphics) | Conference |
ISBN | Citations | PageRank |
978-1-4503-6215-3 | 0 | 0.34 |
References | Authors | |
2 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| nitin bhatia | 1 | 2 | 2.10 |
| Meenakshi D'Souza | 2 | 2 | 3.83 |
| Sujit Kumar Chakrabarti | 3 | 20 | 4.61 |