MARC보기
LDR02263nmm uu200409 4500
001000000334221
00520240805175857
008181129s2018 |||||||||||||||||c||eng d
020 ▼a 9780438178731
035 ▼a (MiAaPQ)AAI10828970
035 ▼a (MiAaPQ)washington:19011
040 ▼a MiAaPQ ▼c MiAaPQ ▼d 248032
0820 ▼a 004
1001 ▼a Pernsteiner, Stuart.
24510 ▼a Practical Verification of Safety-Critical Systems.
260 ▼a [S.l.] : ▼b University of Washington., ▼c 2018
260 1 ▼a Ann Arbor : ▼b ProQuest Dissertations & Theses, ▼c 2018
300 ▼a 132 p.
500 ▼a Source: Dissertation Abstracts International, Volume: 79-12(E), Section: B.
500 ▼a Advisers: Zachary Tatlock
5021 ▼a Thesis (Ph.D.)--University of Washington, 2018.
520 ▼a Software-based control systems operate scientific equipment worth millions of dollars and even safety-critical medical devices, making them good targets for strong formal verification techniques. However, these systems are rarely verified in pr
520 ▼a First, safety properties of control systems often rely on correct operation and interaction of several heterogeneous hardware and software components. No single analysis tool can reason about all types of components. We present techniques, bas
520 ▼a Second, software components of control systems are often developed using proprietary or domain-specific languages for which no formal semantics yet exist. We present a methodology for rapidly developing language semantics, allowing application
520 ▼a Third, for control system software written in specialized languages, often no verified language implementations are available. We present a new technique for developing verified compilers that combines a verified denotation function with a veri
590 ▼a School code: 0250.
650 4 ▼a Computer science.
690 ▼a 0984
71020 ▼a University of Washington. ▼b Computer Science and Engineering.
7730 ▼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
85640 ▼u http://www.riss.kr/pdu/ddodLink.do?id=T14999239 ▼n KERIS
980 ▼a 201812 ▼f 2019
990 ▼a 관리자