| LDR | | 03119nmm uu200493 4500 |
| 001 | | 000000334213 |
| 005 | | 20240805175848 |
| 008 | | 181129s2018 |||||||||||||||||c||eng d |
| 020 | |
▼a 9780438178472 |
| 035 | |
▼a (MiAaPQ)AAI10828911 |
| 035 | |
▼a (MiAaPQ)washington:18984 |
| 040 | |
▼a MiAaPQ
▼c MiAaPQ
▼d 248032 |
| 082 | 0 |
▼a 004 |
| 100 | 1 |
▼a Mullen, Eric. |
| 245 | 10 |
▼a Pushing the Limits of Compiler Verification. |
| 260 | |
▼a [S.l.] :
▼b University of Washington.,
▼c 2018 |
| 260 | 1 |
▼a Ann Arbor :
▼b ProQuest Dissertations & Theses,
▼c 2018 |
| 300 | |
▼a 97 p. |
| 500 | |
▼a Source: Dissertation Abstracts International, Volume: 79-12(E), Section: B. |
| 500 | |
▼a Advisers: Zach Tatlock |
| 502 | 1 |
▼a Thesis (Ph.D.)--University of Washington, 2018. |
| 520 | |
▼a Modern computer systems rely on the correctness of at least one compiler for correct operation. Formal verification is a powerful technique for constructing correct systems. While there have been many efforts to develop formally verified compile |
| 520 | |
▼a OEuf: Verifying systems by implementing them in the programming language of a proof assistant (e.g., Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementatio |
| 520 | |
▼a Here I present OEuf, a verified compiler from a subset of Gallina to assembly. OEuf's correctness theorem ensures that compilation preserves the semantics of the source Gallina program. I describe how OEuf's specification can be used as a foreig |
| 520 | |
▼a Using OEuf: OEufwas developed in order to allow verified systems to be developed and verified in Coq, compiled to executable code using OEuf, with all guarantees proven at the Gallina level preserved through compilation to the assembly level. In |
| 520 | |
▼a Here I present the WordFreq verified system, its correctness guarantee, and the major parts of its correctness proof. I discuss the development of the system and its proof, as well as the axiomatic primitives necessary to tie it together. |
| 520 | |
▼a Peek: Transformations over assembly code are common in many compilers. These transformations are also some of the most bug-dense compiler components. Such bugs could be eliminated by formally verifying the compiler, but state-of-the-art formally |
| 520 | |
▼a Verifying peephole optimizations in Peek requires proving only a set of local properties, which my collaborators and I have proved are sufficient to ensure global transformation correctness. We have proven these local properties for 28 peephole |
| 590 | |
▼a School code: 0250. |
| 650 | 4 |
▼a Computer science. |
| 650 | 4 |
▼a Logic. |
| 650 | 4 |
▼a Mathematics. |
| 690 | |
▼a 0984 |
| 690 | |
▼a 0395 |
| 690 | |
▼a 0405 |
| 710 | 20 |
▼a University of Washington.
▼b Computer Science and Engineering. |
| 773 | 0 |
▼t Dissertation Abstracts International
▼g 79-12B(E). |
| 773 | |
▼t Dissertation Abstract International |
| 790 | |
▼a 0250 |
| 791 | |
▼a Ph.D. |
| 792 | |
▼a 2018 |
| 793 | |
▼a English |
| 856 | 40 |
▼u http://www.riss.kr/pdu/ddodLink.do?id=T14999231
▼n KERIS |
| 980 | |
▼a 201812
▼f 2019 |
| 990 | |
▼a 관리자 |