A formal correctness proof for code generation from SSA form in Isabelle/HOL
| dc.contributor.author | Blech, Jan Olaf | |
| dc.contributor.author | Glesner, Sabine | |
| dc.contributor.editor | Dadam, Peter | |
| dc.contributor.editor | Reichert, Manfred | |
| dc.date.accessioned | 2019-10-11T11:37:51Z | |
| dc.date.available | 2019-10-11T11:37:51Z | |
| dc.date.issued | 2004 | |
| dc.description.abstract | Optimizations in compilers are the most error-prone phases in the compilation process. Since correct compilers are a vital precondition for software correctness, it is necessary to prove their correctness. We develop a formal semantics for static single assignment (SSA) intermediate representations and prove formally within the Isabelle/HOL theorem prover that a relatively simple form of code generation preserves the semantics of the transformed programs in SSA form. This formal correctness proof does not only verify the correctness of a certain class of code generation algorithms but also gives us a sufficient, easily checkable correctness criterion characterizing correct compilation results obtained from implementations (compilers) of these algorithms. | en |
| dc.identifier.isbn | 3-88579-380-6 | |
| dc.identifier.pissn | 1617-5468 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/28810 | |
| dc.language.iso | en | |
| dc.publisher | Gesellschaft für Informatik e.V. | |
| dc.relation.ispartof | Informatik 2004, Informatik verbindet, Band 2, Beiträge der 34. Jahrestagung der Gesellschaft für Informatik e.V. (GI) | |
| dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Proceedings, Volume P-51 | |
| dc.title | A formal correctness proof for code generation from SSA form in Isabelle/HOL | en |
| dc.type | Text/Conference Paper | |
| gi.citation.endPage | 458 | |
| gi.citation.publisherPlace | Bonn | |
| gi.citation.startPage | 449 | |
| gi.conference.date | 20.-24. September 2004 | |
| gi.conference.location | Ulm | |
| gi.conference.sessiontitle | Regular Research Papers |
Dateien
Originalbündel
1 - 1 von 1
Lade...
- Name:
- GI-Proceedings.51-94.pdf
- Größe:
- 357.05 KB
- Format:
- Adobe Portable Document Format