가야대학교 분성도서관

상단 글로벌/추가 메뉴

회원 로그인

주메뉴

: • 전체검색; • 단행본; • 정기간행물; • 학위논문; • 비도서; • 특정번호 검색; • 기사색인; • 학습연구지원; • 지정도서

: • 전자자원통합검색; • 해외 WEB DB; • E-Book; • E-Learning; • 국내 WEB DB; • 인터넷검색

: • 대출현황조회/연장; • 예약현황조회/취소; • 희망도서; • 내서재; • 나의서평; • 나의태그; • 나의위젯; • RSS; • SDI; • 개인정보관리

: • 공지사항; • FAQ; • Q&A 일반·학술; • 신착/인기 도서; • 학위논문온라인제출; • 외부인 이용안내; • 설문조사

: • 도서관 소개; • 연혁; • 현황; • 이용안내; • 찾아오시는 길

자료검색

Home
상세정보

상세정보

검색결과 돌아가기

부가기능

MARC보기

Pushing the Limits of Compiler Verification

상세 프로파일

상세정보
자료유형	E-Book
개인저자	Mullen, Eric.
단체저자명	University of Washington. Computer Science and Engineering.
서명/저자사항	Pushing the Limits of Compiler Verification.
발행사항	[S.l.] : University of Washington., 2018
발행사항	Ann Arbor : ProQuest Dissertations & Theses, 2018
형태사항	97 p.
소장본 주기	School code: 0250.
ISBN	9780438178472
일반주기	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.
언어	영어
기본자료 저록	Dissertation Abstracts International79-12B(E). Dissertation Abstract International
대출바로가기	http://www.riss.kr/pdu/ddodLink.do?id=T14999231