상세정보
Export to Refworks부가기능
Pushing the Limits of Compiler Verification
상세 프로파일
| 자료유형 | 학위논문 |
|---|---|
| 서명/저자사항 | Pushing the Limits of Compiler Verification. |
| 개인저자 | Mullen, Eric. |
| 단체저자명 | University of Washington. Computer Science and Engineering. |
| 발행사항 | [S.l.]: University of Washington., 2018. |
| 발행사항 | Ann Arbor: ProQuest Dissertations & Theses, 2018. |
| 형태사항 | 97 p. |
| 기본자료 저록 | Dissertation Abstracts International 79-12B(E). Dissertation Abstract International |
| ISBN | 9780438178472 |
| 학위논문주기 | Thesis (Ph.D.)--University of Washington, 2018. |
| 일반주기 |
Source: Dissertation Abstracts International, Volume: 79-12(E), Section: B.
Advisers: Zach Tatlock |
| 요약 | 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 |
| 요약 | 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 |
| 요약 | 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 |
| 요약 | 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 |
| 요약 | 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. |
| 요약 | 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 |
| 요약 | 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 |
| 일반주제명 | Computer science. Logic. Mathematics. |
| 언어 | 영어 |
| 바로가기 | 
: 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
