Skip to main content
SpringerLink
Log in

Exploiting Partial Knowledge for Efficient Model Analysis

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10482))

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 effective implementation of the technique is provided as an extension to the Kodkod relational constraint solver. Evaluation shows that, in average, the proposed technique outperforms the regular amalgamated verification procedure.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://baldur.iti.kit.edu/sat-race-2015/.

References

  1. Abrial, J.: The B-book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)

    Google Scholar 

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

  3. Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197–205. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_15

    Google Scholar 

  4. Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT race 2010. Technical report 10/1, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University (2010)

    Google Scholar 

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

  6. Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: KR 1996, pp. 148–159. Morgan Kaufmann (1996)

    Google Scholar 

  7. Eén, N., Sörensson, N.: MiniSat, version 2.2.0, July 2010. http://minisat.se/MiniSat.html

  8. Hölldobler, S., Manthey, N., Nguyen, V.H., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: AICACSIS 2011, pp. 201–206. IEEE (2011)

    Google Scholar 

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

    Google Scholar 

  10. Lamport, L.: Specifying Systems, The TLA\(^+\) Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)

    Google Scholar 

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

  12. Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: FSE 2016. ACM (2016)

    Google Scholar 

  13. Macedo, N., Cunha, A., Guimarães, T.: Exploring scenario exploration. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 301–315. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46675-9_20

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Montaghami, V., Rayside, D.: Extending alloy with partial instances. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 122–135. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30885-7_9

    Chapter  Google Scholar 

  16. Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)

    Article  Google Scholar 

  17. Rosner, N., López Pombo, C.G., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F.: Parallel bounded verification of alloy models by transcoping. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 88–107. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54108-7_5

    Chapter  Google Scholar 

  18. Rosner, N., Siddiqui, J.H., Aguirre, N., Khurshid, S., Frias, M.F.: Ranger: parallel analysis of alloy models by range partitioning. In: ASE 2013, pp. 147–157. IEEE (2013)

    Google Scholar 

  19. Singer, D., Monnet, A.: JaCk-SAT: a new parallel scheme to solve the satisfiability problem (SAT) based on join-and-check. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Wasniewski, J. (eds.) PPAM 2007. LNCS, vol. 4967, pp. 249–258. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68111-3_27

    Chapter  Google Scholar 

  20. Torlak, E.: Kodkod, version 2.1, September 2015. http://alloy.mit.edu/kodkod/download.html

  21. Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_49

    Chapter  Google Scholar 

  22. Uzuncaova, E., Khurshid, S.: Constraint prioritization for efficient analysis of declarative models. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 310–325. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68237-0_22

    Chapter  Google Scholar 

Download references

Acknowldgements

This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within project POCI-01-0145-FEDER-016826.

Author information

Authors and Affiliations

  1. INESC TEC & Universidade do Minho, Braga, Portugal

    Nuno Macedo, Alcino Cunha & Eduardo Pessoa

Authors
  1. Nuno Macedo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alcino Cunha
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eduardo Pessoa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nuno Macedo .

Editor information

Editors and Affiliations

  1. Indian Institute of Science, Bangalore, India

    Deepak D'Souza

  2. Chennai Mathematical Institute, Kelambakkam, India

    K. Narayan Kumar

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Macedo, N., Cunha, A., Pessoa, E. (2017). Exploiting Partial Knowledge for Efficient Model Analysis. In: D'Souza, D., Narayan Kumar, K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science(), vol 10482. Springer, Cham. https://doi.org/10.1007/978-3-319-68167-2_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68167-2_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68166-5

  • Online ISBN: 978-3-319-68167-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation