상세정보
Export to Refworks부가기능
Optimizing the Automated Programming Stack
상세 프로파일
| 자료유형 | 학위논문 |
|---|---|
| 서명/저자사항 | Optimizing the Automated Programming Stack. |
| 개인저자 | Bornholt, James. |
| 단체저자명 | University of Washington. Computer Science and Engineering. |
| 발행사항 | [S.l.]: University of Washington., 2019. |
| 발행사항 | Ann Arbor: ProQuest Dissertations & Theses, 2019. |
| 형태사항 | 135 p. |
| 기본자료 저록 | Dissertations Abstracts International 81-04B. Dissertation Abstract International |
| ISBN | 9781687955111 |
| 학위논문주기 | Thesis (Ph.D.)--University of Washington, 2019. |
| 일반주기 |
Source: Dissertations Abstracts International, Volume: 81-04, Section: B.
Advisor: Torlak, Emina |
| 이용제한사항 | This item must not be sold to any third party vendors.This item must not be added to any third party search indexes. |
| 요약 | The scale and pervasiveness of modern software poses a challenge forprogrammers: software reliability is more important than ever, but thecomplexity of computer systems continues to grow. Automated programmingtools are a powerful way for programmers to tackle this challenge:verifiers that check software correctness, and synthesizers thatgenerate new correct-by-construction programs. These tools are mosteffective when they apply domain-specific optimizations, but doing sotoday requires considerable formal methods expertise.This dissertation shows that new abstractions and techniques can empowerprogrammers to build specialized automated programming tools that ensuresoftware reliability. We first demonstrate the importance andeffectiveness of automated tools in the context of memory consistencymodels, which define the behavior of multiprocessor CPUs and whosesubtleties often elude even experts. MemSynth is a tool thatautomatically synthesizes formal descriptions of memory consistencymodels from examples of CPU behavior, and has found ambiguities andunderspecifications in two major computer architectures. We thenintroduce two new programmer techniques for developing automatedprogramming tools. Metasketches are a new abstraction for buildingprogram synthesis tools that integrate search strategy into the problemdefinition, allowing a metasketch solver to solve synthesis problemsthat other tools cannot. Symbolic profiling is a technique forsystematically identifying and resolving scalability bottlenecks inautomated programming tools. Symbolic profiling generalizes acrossdifferent symbolic evaluation engines and has been used to improve theperformance of state-of-the-art automated tools by orders of magnitude.Together, these three contributions demonstrate the value of automatedprogramming tools for building reliable software, and offer guidance onhow to build such tools efficiently for new problem domains. |
| 일반주제명 | Computer science. |
| 언어 | 영어 |
| 바로가기 | 
: 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
