关键词：规范；编程；数字电路；线性时序逻辑；自动机
摘 要：Specification is the first and arguably the most important step for formal verification and correct-by-construction synthesis. It is extremely difficult to manually create a complete suite of good-quality formal specifications. Many real-world experiences indicate that poor or the lack of sufficient specifications can easily lead to misses of critical bugs, and in turn design re-spins and time-to-market slips. This dissertation presents research that seeks to mitigate the manual and error-prone process of creating formal specifications through automation. The overarching theme is specification mining - the process of inferring likely specifications by observing a design's behaviors. We explore novel formalisms and algorithms to mine specifications from different sources, and demonstrate that the mined specifications are useful if not essential for a wide variety of applications such as verification, diagnosis and LTL synthesis. Further, we describe efforts on broadening the scope of specification mining with creative use of human inputs, including the design of a crowdsourced game and judicious use of natural language processing techniques.