Abstract
dc:description.abstractIn the world that we live in today, we greatly rely on software in nearly every aspect of our lives. In many critical applications, such as in transportation and medical systems, catastrophic consequences could occur in case of buggy software. As the computational power and storage capacity of computer hardware keep increasing, so are the size and complexity of the software. This makes testing and verification increasingly challenging in practice, and consequentially creates a chance for software with critical bugs to find their way into the consumer market. In this dissertation, I present a set of innovative new methods for automatically verifying, as well as synthesizing, critical software and hardware in embedded computing applications. Based on a set of rigorous formal analysis techniques, my methods can guarantee that the resulting software are efficient and secure as well as provably correct.
Degree
thesis:*- Name thesis:degree_name
- Ph. D.
- Level thesis:degree_level
- doctoral
- Discipline thesis:degree_discipline
- Computer Engineering
- Department dc:contributor.department
- Electrical and Computer Engineering
- Grantor dc:publisher
- Virginia Tech
- Year dc:date.issued
- 2015
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Eldib, Hassan Shoukry
- Chair dc:contributor.committeechair
-
- Wang, Chao
- Committee members dc:contributor.committeemember
-
- Tilevich, Eli
- Schaumont, Patrick R.
- Hsiao, Michael S.
- Shukla, Sandeep K.
Subjects
dc:subject × 6Rights
dc:rights- Statement dc:rights
-
- In Copyright
- Licence dc:rights.uri
Identifiers
dc:identifier.*- Dc Identifier Other
- vt_gsexam:5605
- OAI identifier oai:identifier
- oai:vtechworks.lib.vt.edu:10919/55120