publication . Part of book or chapter of book . Conference object . 2017

Exploiting Partial Knowledge for Efficient Model Analysis

Nuno Macedo; Alcino Cunha; Eduardo José Dias Pessoa;
Open Access
  • Published: 26 Sep 2017
  • Publisher: Springer International Publishing
  • Country: Portugal
Abstract
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 verification task, which often proves to be a performance bottleneck. This paper addresses this issue by proposing a solving strategy that exploits user-provided partial knowledge, namely by assigning symbolic bounds to the problem’s variables, to automatically decompose a verification task into smaller ones, which are prone to being independently analyzed in parallel and with tighter search spaces. An e...
Persistent Identifiers
Subjects
free text keywords: Bottleneck, Programming language, computer.software_genre, computer, Computer science, Formal specification
Related Organizations
22 references, page 1 of 2

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.

11. N. Macedo. Pardinus, version 0.3. Available at https://github.com/nmacedo/ Pardinus/, September 2016.

12. N. Macedo, J. Brunel, D. Chemouil, A. Cunha, and D. Kuperberg. Lightweight speci cation and analysis of dynamic systems with rich con gurations. In FSE'16. ACM, 2016.

13. N. Macedo, A. Cunha, and T. Guimar~aes. Exploring scenario exploration. In FASE'15, volume 9033 of LNCS, pages 301{315. Springer, 2015.

14. R. Martins, V. M. Manquinho, and I. Lynce. An overview of parallel SAT solving. Constraints, 17(3):304{347, 2012.

15. V. Montaghami and D. Rayside. Extending Alloy with partial instances. In ABZ'12, volume 7316 of LNCS, pages 122{135. Springer, 2012.

22 references, page 1 of 2
Any information missing or wrong?Report an Issue