Constraint Based Program Synthesis for Embedded Software

In 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 conse-quences 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. Acknowledgment First and foremost, I would like to express my deepest appreciation to my Ph.D. advisor, Professor Chao Wang, from whom I have learned incredibly a lot. His continuous guidance, dedication and encouragement has helped me become a more mature researcher and shape my future goals. Professor Wang will always remain a source of inspiration for me, even after graduation. I would also like to express my gratitude to Professor Patrick Schaumont, Professor Michael Hsiao, Professor Sandeep Shukla, and Professor Eli Tilevich for serving on my committee. It has been a great honor for me to work closely with them. I am grateful to my parents for their never-ending encouragement and support throughout my life. I am truly fortunate to have such parents. Finally, I want to thank my wife and my daughter for their endless love and support throughout these years. Hassan Eldib iii Contents Abstract ii Acknowledgment ii