Chao Wang    

 Project: Shield Synthesizer




Description: The objective of this research is to apply program synthesis-based techniques to automatically improve the performance, safety, and security of complex digital systems (hardware, software, and embedded systems). For example, scalability issues may prevent users from verifying critical properties of a complex design. In this situation, we propose to synthesize a safety shield that is attached to the design to enforce the properties at run time. Such shield synthesis method can succeed where model checking and reactive synthesis fail, because it only considers a small set of critical properties, as opposed to the complex design, or the complete specification in the case of reactive synthesis.