| LDR | | 00000nam u2200205 4500 |
| 001 | | 000000434518 |
| 005 | | 20200226154936 |
| 008 | | 200131s2019 ||||||||||||||||| ||eng d |
| 020 | |
▼a 9781687955111 |
| 035 | |
▼a (MiAaPQ)AAI22619565 |
| 040 | |
▼a MiAaPQ
▼c MiAaPQ
▼d 247004 |
| 082 | 0 |
▼a 004 |
| 100 | 1 |
▼a Bornholt, James. |
| 245 | 10 |
▼a Optimizing the Automated Programming Stack. |
| 260 | |
▼a [S.l.]:
▼b University of Washington.,
▼c 2019. |
| 260 | 1 |
▼a Ann Arbor:
▼b ProQuest Dissertations & Theses,
▼c 2019. |
| 300 | |
▼a 135 p. |
| 500 | |
▼a Source: Dissertations Abstracts International, Volume: 81-04, Section: B. |
| 500 | |
▼a Advisor: Torlak, Emina |
| 502 | 1 |
▼a Thesis (Ph.D.)--University of Washington, 2019. |
| 506 | |
▼a This item must not be sold to any third party vendors. |
| 506 | |
▼a This item must not be added to any third party search indexes. |
| 520 | |
▼a 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. |
| 590 | |
▼a School code: 0250. |
| 650 | 4 |
▼a Computer science. |
| 690 | |
▼a 0984 |
| 710 | 20 |
▼a University of Washington.
▼b Computer Science and Engineering. |
| 773 | 0 |
▼t Dissertations Abstracts International
▼g 81-04B. |
| 773 | |
▼t Dissertation Abstract International |
| 790 | |
▼a 0250 |
| 791 | |
▼a Ph.D. |
| 792 | |
▼a 2019 |
| 793 | |
▼a English |
| 856 | 40 |
▼u http://www.riss.kr/pdu/ddodLink.do?id=T15493638
▼n KERIS
▼z 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
| 980 | |
▼a 202002
▼f 2020 |
| 990 | |
▼a ***1008102 |
| 991 | |
▼a E-BOOK |