Citation
Wenchao Li. "Specification Mining - New Formalisms, Algorithms and Applications". Talk or presentation, 12, November, 2013.

Abstract
Specification is the first and arguably the most important step for formal verification and correct-by-construction synthesis. These tasks require understanding precisely a design's intended behavior, and thus are only effective if the specification is created right. For example,much of the challenge in bug finding lies in finding the specification that mechanized tools can use to find bugs. It is extremely difficult to manually create a complete suite of good-quality formal specifications, especially given the enormous scale and complexity of designs today. 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 mitigates this manual and error-prone process through automation. The overarching theme is specification mining - the process of inferring likely specifications by observing a design's behaviors. In the first part of the talk, I will describe two approaches to mine specifications dynamically from simulation or execution traces. The first approach offers a simple but effective template-based remedy to the aforementioned problem. The second approach presents a novel formalism of specification mining based on the notion of sparse coding, which can learn latent structures in an unsupervised setting. I will discuss tradeoffs and synergies of the two approaches and show how the mined specifications can be used to localize bugs effectively. In the second part of the talk, I will focus on the problem of synthesis from temporal logic specifications. While offering the attractive proposition of correct-by-construction, this synthesis approach completely relies on the user to not only specify the intended behaviors of the system but also the assumptions on the environment. Environment assumptions are especially hard to get right since they are often implicit knowledge and are seldom documented. We address this problem by learning assumptions from the counterstrategies of an unrealizable specification to systematically guide it towards realizability. We further show that, the proposed counterstrategy-guided assumption mining framework enables the automatic synthesis of a new class of semi-autonomous controllers, called human-in-the-loop (HuIL) controllers. Lastly, I will discuss two efforts on broadening the scope of specification mining with human inputs, one through gamification and crowdsourcing and the other through natural language processing.

Electronic downloads

• wenchao_li-specification_mining.pdf · application/pdf · 5698 kbytes

• HTML

  Wenchao Li. <a
  href="http://chess.eecs.berkeley.edu/pubs/1024.html"
  ><i>Specification Mining - New Formalisms,
  Algorithms and Applications</i></a>, Talk or
  presentation,  12, November, 2013.

• Plain text

  Wenchao Li. "Specification Mining - New Formalisms,
  Algorithms and Applications". Talk or presentation, 
  12, November, 2013.

• BibTeX

  @presentation{Li13_SpecificationMiningNewFormalismsAlgorithmsApplications,
      author = {Wenchao Li},
      title = {Specification Mining - New Formalisms, Algorithms
                and Applications},
      day = {12},
      month = {November},
      year = {2013},
      abstract = {Specification is the first and arguably the most
                important step for formal verification and
                correct-by-construction synthesis. These tasks
                require understanding precisely a design's
                intended behavior, and thus are only effective if
                the specification is created right. For
                example,much of the challenge in bug finding lies
                in finding the specification that mechanized tools
                can use to find bugs. It is extremely difficult to
                manually create a complete suite of good-quality
                formal specifications, especially given the
                enormous scale and complexity of designs today.
                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 mitigates this
                manual and error-prone process through automation.
                The overarching theme is specification mining -
                the process of inferring likely specifications by
                observing a design's behaviors. In the first part
                of the talk, I will describe two approaches to
                mine specifications dynamically from simulation or
                execution traces. The first approach offers a
                simple but effective template-based remedy to the
                aforementioned problem. The second approach
                presents a novel formalism of specification mining
                based on the notion of sparse coding, which can
                learn latent structures in an unsupervised
                setting. I will discuss tradeoffs and synergies of
                the two approaches and show how the mined
                specifications can be used to localize bugs
                effectively. In the second part of the talk, I
                will focus on the problem of synthesis from
                temporal logic specifications. While offering the
                attractive proposition of correct-by-construction,
                this synthesis approach completely relies on the
                user to not only specify the intended behaviors of
                the system but also the assumptions on the
                environment. Environment assumptions are
                especially hard to get right since they are often
                implicit knowledge and are seldom documented. We
                address this problem by learning assumptions from
                the counterstrategies of an unrealizable
                specification to systematically guide it towards
                realizability. We further show that, the proposed
                counterstrategy-guided assumption mining framework
                enables the automatic synthesis of a new class of
                semi-autonomous controllers, called
                human-in-the-loop (HuIL) controllers. Lastly, I
                will discuss two efforts on broadening the scope
                of specification mining with human inputs, one
                through gamification and crowdsourcing and the
                other through natural language processing.},
      URL = {http://chess.eecs.berkeley.edu/pubs/1024.html}
  }
  

Posted by Armin Wasicek on 14 Nov 2013.
Groups: chessworkshop
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.