@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@InProceedings{brady-fmcad11,
  author = 	 {Bryan Brady and Randal E. Bryant and Sanjit A. Seshia},
  title = 	 {Learning Conditional Abstractions},
  booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  month = {October},
  year = 	 {2011},
  pages = "116--124",
  abstract = {Abstraction is central to formal verification. In term-level
abstraction, the design is abstracted using a fragment of
first-order logic with background theories, such as the theory of
uninterpreted functions with equality. The main challenge in using
term-level abstraction is determining what components to abstract
and under what conditions. In this paper, we present an automatic
technique to conditionally abstract register transfer level (RTL)
hardware designs to the term level. Our approach is a layered
approach that combines random simulation and machine learning
inside a counter-example guided abstraction refinement (CEGAR)
loop. First, random simulation is used to determine modules that
are candidates for abstraction. Next, machine learning is used on the
resulting simulation traces to generate candidate conditions under
which those modules can be abstracted. Finally, a verifier is invoked.
If spurious counter-examples arise, we refine the abstraction by
performing a further iteration of random simulation and machine
learning. We present an experimental evaluation on processor and
low-power designs.},
}