@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 Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{CFMSV15a,
  title={On Parallel Scalable Uniform SAT Witness Generator},
  bib2html_dl_pdf={../Papers/Tacas15.pdf},
  code={https://bitbucket.org/kuldeepmeel/unigen},
  author={
    Chakraborty, Supratik and Fremont, Daniel J. and Meel, Kuldeep S. and
    Seshia, Sanjit A. and Vardi, Moshe Y.
  },
  booktitle=TACAS,
  pages={304--319},
  year={2015},
  month=apr,
  bib2html_rescat={Sampling},
  bib2html_pubtype={Refereed Conference},
  abstract={
    Constrained-random verification (CRV) is widely used in industry for
    validating hardware designs. The effectiveness of CRV depends on the
    uniformity of test stimuli generated from a given set of constraints. Most
    existing techniques sacrifice either uniformity or scalability when
    generating stimuli. While recent work based on random hash functions has
    shown that it is possible to generate almost uniform stimuli from
    constraints with 100,000+ variables, the performance still falls short of
    today's industrial requirements. In this paper, we focus on pushing the
    performance frontier of uniform stimulus generation further. We present a
    random hashing-based, easily parallelizable algorithm, UniGen2, for sampling
    solutions of propositional constraints. UniGen2 provides strong and relevant
    theoretical guarantees in the context of CRV, while also offering
    significantly improved performance compared to existing almost-uniform
    generators. Experiments on a diverse set of benchmarks show that UniGen2
    achieves an average speedup of about 20X over a state-of-the-art sampling
    algorithm, even when running on a single core. Moreover, experiments with
    multiple cores show that UniGen2 achieves a near-linear speedup in the
    number of cores, thereby boosting performance even further.
  },
}