Advertisement

Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method

  • Allison SullivanEmail author
  • Darko Marinov
  • Sarfraz Khurshid
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)

Abstract

Formal methods are a key to engineering more reliable systems. In this paper, we focus on an important application of formal methods — enumerating solutions to logical formulas that encode properties of interest. Solution enumeration has many uses, e.g., in systematic software testing, model counting, or hardware analysis. We introduce solution enumeration abstraction, a novel idiom that allows users to define data abstractions to enhance solution enumeration by specifying how the solutions must differ, so enumeration creates a high quality set of solutions of a manageable size. We embody the idiom as a technique built on top of Alloy, a well-known lightweight formal method, which is comprised of a first-order relational logic with transitive closure, and a SAT-based analysis engine. Experimental results show that our technique supports a variety of data abstractions, and can substantially reduce the number of solutions enumerated and the time to enumerate them.

Notes

Acknowledgments

We thank Caroline Trippel for sharing some of her excellent Alloy models and commenting on an earlier paper draft. This work was partially supported by NSF grants. CNS-1646305, CCF-1718903, CNS-1740916, and CCF-1918189, and an Intel ISRA grant for research on hardware security.

References

  1. 1.
    Alloy analyzer Website (2019). http://alloytools.org
  2. 2.
    Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2008)CrossRefGoogle Scholar
  3. 3.
    Bagheri, H., Kang, E., Malek, S., Jackson, D.: A Formal Approach for Detection of Security Flaws in the Android Permission System. Formal Aspects of Computing. Springer, London (2018).  https://doi.org/10.1007/s00165-017-0445-zCrossRefGoogle Scholar
  4. 4.
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: ISSTA (2002)Google Scholar
  5. 5.
    CheckMate GitHub (2019). https://github.com/ctrippel/checkmate
  6. 6.
    Chong, N., Sorensen, T., Wickerson, J.: The semantics of transactions and weak memory in x86, Power, ARM, and C++. In: PLDI (2018)Google Scholar
  7. 7.
    Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)zbMATHGoogle Scholar
  8. 8.
    Crawford, J.: A theoretical analysis of reasoning by symmetry in first-order logic (extended abstract). In: AAAI 1992 Workshop on Tractable Reasoning (1992)Google Scholar
  9. 9.
    CryptoMiniSat Solver Website (2019). https://www.msoos.org/cryptominisat5/
  10. 10.
    Dutra, R., Bachrach, J., Sen, K.: SMTSampler: efficient stimulus generation from complex SMT constraints. In: ICCAD (2018)Google Scholar
  11. 11.
    Een, N., Sorensson, N.: An extensible SAT-solver. In: SAT (2003)Google Scholar
  12. 12.
    Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in Symbolic PathFinder. In: ICSE (2013)Google Scholar
  13. 13.
    Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. TSE 39(9), 1283–1307 (2013)Google Scholar
  14. 14.
    Ghiya, R., Hendren, L.J.: Is it a tree, a DAG, or a cyclic graph? a shape analysis for heap-directed pointers in C. In: POPL (1996)Google Scholar
  15. 15.
    Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D.: Test generation through programming in UDITA. In: ICSE (2010)Google Scholar
  16. 16.
    Glucose Solver Website (2019). https://www.labri.fr/perso/lsimon/glucose/
  17. 17.
    Gopinath, D., Malik, M.Z., Khurshid, S.: Specification-based program repair using SAT. In: TACAS (2011)Google Scholar
  18. 18.
    Guttag, J.V., Horning, J.J.: Larch: Languages and Tools for Formal Specification (1993)Google Scholar
  19. 19.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)Google Scholar
  20. 20.
    Jackson, D., Sullivan, K.J.: COM revisited: Tool-assisted modelling of an architectural framework. In: SIGSOFT FSE (2000)Google Scholar
  21. 21.
    Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA (2000)Google Scholar
  22. 22.
    Khurshid, S., Jackson, D.: Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In: ASE (2000)Google Scholar
  23. 23.
    Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D.: A case for efficient solution enumeration. In: SAT (2003)Google Scholar
  24. 24.
    Kuraj, I., Kuncak, V., Jackson, D.: Programming with enumerable sets of structures. In: OOPSLA (2015)Google Scholar
  25. 25.
    Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. Softw. Eng. Notes 31(3), 1–38 (2006)CrossRefGoogle Scholar
  26. 26.
    Leino, K.R.M., Müller, P.: A verification methodology for model fields. In: ESOP (2006)Google Scholar
  27. 27.
    Lingeling, Plingeling, and Treengeling Website (2019). http://fmv.jku.at/lingeling/
  28. 28.
    Liskov, B., Guttag, J.: Program development in Java: Abstraction, Specification, and Object-Oriented Design (2000)Google Scholar
  29. 29.
    Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: VMCAI, pp. 181–198 (2005)Google Scholar
  30. 30.
    Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: ASE (2001)Google Scholar
  31. 31.
    Meel, K.S., et al.: Constrained sampling and counting: universal hashing meets SAT solving. In: Beyond NP, AAAI Workshop (2016)Google Scholar
  32. 32.
    de Moura, L., Bjorner, N.: Z3: an efficient SMT solver. In: TACAS (2008)Google Scholar
  33. 33.
    Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE, pp. 232–241 (2013)Google Scholar
  34. 34.
    Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for Java. In: OOPSLA Companion, pp. 815–816 (2007)Google Scholar
  35. 35.
    Ponzio, P., Aguirre, N., Frias, M.F., Visser, W.: Field-exhaustive testing. In: SIGSOFT FSE (2016)Google Scholar
  36. 36.
    Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: FM (2018)Google Scholar
  37. 37.
    Păsăreanu, C.S., Pelánek, R., Visser, W.: Concrete model checking with abstract matching and refinement. In: CAV (2005)Google Scholar
  38. 38.
    Rayside, D., Benjamin, Z., Singh, R., Near, J.P., Milicevic, A., Jackson, D.: Equality and hashing for (almost) free: generating implementations from abstraction functions. In: ICSE (2009)Google Scholar
  39. 39.
    Rayside, D., Montaghami, V., Leung, F., Yuen, A., Xu, K., Jackson, D.: Synthesizing iterators from abstraction functions. In: GPCE (2012)Google Scholar
  40. 40.
    Ringer, T., Grossman, D., Schwartz-Narbonne, D., Tasiran, S.: A solver-aided language for test input generation. In: PACMPL OOPSLA (2017)Google Scholar
  41. 41.
    Samimi, H., Aung, E.D., Millstein, T.D.: Falling back on executable specifications. In: ECOOP (2010)Google Scholar
  42. 42.
    SAT4J Solver Website (2019). https://www.sat4j.org/
  43. 43.
    Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. In: SAT (2001)Google Scholar
  44. 44.
    Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: ICST (2017)Google Scholar
  45. 45.
    Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: TACAS (2007)Google Scholar
  46. 46.
    Trippel, C., Lustig, D., Martonosi, M.: CheckMate: automated synthesis of hardware exploits and security litmus tests. In: MICRO (2018)Google Scholar
  47. 47.
    Trippel, C., Lustig, D., Martonosi, M.: Security verification via automatic hardware-aware exploit synthesis: The CheckMate approach. In: IEEE Micro (2019)Google Scholar
  48. 48.
    Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: POPL (2017)Google Scholar
  49. 49.
    Xie, T., Marinov, D., Notkin, D.: Rostra: a framework for detecting redundant object-oriented unit tests. In: ASE (2004)Google Scholar
  50. 50.
    Zaeem, R.N., Khurshid, S.: Contract-based data structure repair using Alloy. In: ECOOP (2010)Google Scholar
  51. 51.
    Zave, P.: Reasoning about identifier spaces: how to make chord correct. IEEE Trans. Softw. Eng. 43(12), 1144–1156 (2017)CrossRefGoogle Scholar
  52. 52.
    Zhang, J.: The generation and application of finite models. Ph.D. thesis, Institute of Software, Academia Sinica, Beijing (1994)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Allison Sullivan
    • 1
    Email author
  • Darko Marinov
    • 2
  • Sarfraz Khurshid
    • 3
  1. 1.North Carolina A&T State UniversityGreensboroUSA
  2. 2.University of Illinois at Urbana-ChampaignUrbanaUSA
  3. 3.University of Texas at AustinAustinUSA

Personalised recommendations