Exploiting partial knowledge for efficient model analysis

Conference object English OPEN
Macedo, Nuno; Cunha, Alcino; Pessoa, Eduardo José Dias;

The advancement of constraint solvers and model checkers has enabled the effective analysis of high-level formal specification languages. However, these typically handle a specification in an opaque manner, amalgamating all its constraints in a single monolithic verific... View more
  • References (22)
    22 references, page 1 of 3

    1. J. Abrial. The B-book { Assigning programs to meanings. Cambridge University Press, 2005.

    2. G. Audemard and L. Simon. Glucose, version 4.0. Available at http://alloy.mit. edu/kodkod/download.html, October 2014.

    3. G. Audemard and L. Simon. Lazy clause exchange policy for parallel SAT solvers. In C. Sinz and U. Egly, editors, SAT'14, held as part of VSL'14, volume 8561 of LNCS, pages 197{205. Springer, 2014.

    4. A. Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT race 2010. Technical Report 10/1, FMV Reports Series, Institute for Formal Models and Veri cation, Johannes Kepler University, 2010.

    5. A. Biere. Plingeling, version ayv-86bf266-140429. Available at http://fmv.jku. at/lingeling/, April 2014.

    6. J. M. Crawford, M. L. Ginsberg, E. M. Luks, and A. Roy. Symmetry-breaking predicates for search problems. In KR'96, pages 148{159. Morgan Kaufmann, 1996.

    7. N. Een and N. Sorensson. MiniSat, version 2.2.0. Available at http://minisat. se/MiniSat.html, July 2010.

    8. S. Holldobler, N. Manthey, V. H. Nguyen, J. Stecklina, and P. Steinke. A short overview on modern parallel SAT-solvers. In AICACSIS'11, pages 201{206. IEEE, 2011.

    9. D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, revised edition, 2012.

    10. L. Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.

  • Metrics
Share - Bookmark