Wenchao Li

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2014-20

March 17, 2014

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-20.pdf

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.

Advisors: Sanjit A. Seshia

---

BibTeX citation:

@phdthesis{Li:EECS-2014-20,
    Author= {Li, Wenchao},
    Title= {Specification Mining: New Formalisms, Algorithms and Applications},
    School= {EECS Department, University of California, Berkeley},
    Year= {2014},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-20.html},
    Number= {UCB/EECS-2014-20},
    Abstract= {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.},
}

EndNote citation:

%0 Thesis
%A Li, Wenchao 
%T Specification Mining: New Formalisms, Algorithms and Applications
%I EECS Department, University of California, Berkeley
%D 2014
%8 March 17
%@ UCB/EECS-2014-20
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-20.html
%F Li:EECS-2014-20