Abstract
Computing minimal (or even just small) certificates is a central problem in automated reasoning and, in particular, in automated formal verification. For unsatisfiable formulas in CNF such certificates take the form of Minimal Unsatisfiable Subsets (MUSes) and have a wide range of applications. As a formula can have multiple MUSes that each provide different insights on unsatisfiability, commonly studied problems include computing a smallest MUS (SMUS) or computing all MUSes (AllMUS) of a given unsatisfiable formula. In this paper, we consider certificates to safety properties in the form of Minimal Safe Inductive Sets (MSISes), and we develop algorithms for exploring such certificates by computing a smallest MSIS (SMSIS) or computing all MSISes (AllMSIS) of a given safe inductive invariant. More precisely, we show how the well-known MUS enumeration algorithms CAMUS and MARCO can be adapted to MSIS enumeration.
R. Berryhill—This work was completed while Ryan Berryhill was an intern at IBM Research Haifa.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Hardware Model Checking Competition (2011). http://fmv.jku.at/hwmcc11
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2005. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30557-6_14
Berryhill, R., Ivrii, A., Veira, N., Veneris, A.: Learning support sets in IC3 and Quip: The good, the bad, and the ugly. In: 2017 Formal Methods in Computer Aided Design (FMCAD) (2017)
Berryhill, R., Veira, N., Veneris, A., Poulos, Z.: Learning lemma support graphs in Quip and IC3. In: Proceedings of the 2nd International Verification and Security Workshop, IVSW 2017 (2017)
Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: 2011 Formal Methods in Computer-Aided Design (FMCAD), pp. 144–153, October 2011
Bradley, A.: SAT-based model checking without unrolling. In: International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011 (2011)
E\(\rm \acute{e}\)n, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011 (2011)
Ghassabani, E., Whalen, M., Gacek, A.: Efficient generation of all minimal inductive validity cores. In: 2017 Formal Methods in Computer Aided Design (FMCAD) (2017)
Gupta, A.: Learning Abstractions for Model Checking. Ph.D. thesis, Pittsburgh, PA, USA (2006), aAI3227784
Hassan, Z., Bradley, A.R., Somenzi, F.: Incremental, inductive CTL model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 532–547. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_38
Ignatiev, A., Previti, A., Liffiton, M., Marques-Silva, J.: Smallest MUS extraction with minimal hitting set dualization. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 173–182. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23219-5_13
Ivrii, A., Gurfinkel, A., Belov, A.: Small inductive safe invariants. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, FMCAD 2014 (2014)
Janota, M., Marques-Silva, J.: On the query complexity of selecting minimal sets for monotone predicates. Artif. Intell. 233, 73–83 (2016)
Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016). https://doi.org/10.1007/s10601-015-9183-0
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008). https://doi.org/10.1007/s10817-007-9084-z
Marques-Silva, J., Janota, M., Belov, A.: Minimal Sets over Monotone Predicates in Boolean Formulae (2013). https://doi.org/10.1007/978-3-642-39799-8_39
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_1
McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_2
Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, pp. 221–229 (2010)
Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. J. Comput. Syst. Sci. 37(1), 2–13 (1988)
Previti, A., Marques-Silva, J.: Partial MUS enumeration. In: Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2013 (2013)
Simmonds, J., Davies, J., Gurfinkel, A., Chechik, M.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. In: FMCAD, pp. 3–12. IEEE Computer Society (2007)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Berryhill, R., Ivrii, A., Veneris, A. (2018). Finding All Minimal Safe Inductive Sets. In: Beyersdorff, O., Wintersteiger, C. (eds) Theory and Applications of Satisfiability Testing – SAT 2018. SAT 2018. Lecture Notes in Computer Science(), vol 10929. Springer, Cham. https://doi.org/10.1007/978-3-319-94144-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-94144-8_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94143-1
Online ISBN: 978-3-319-94144-8
eBook Packages: Computer ScienceComputer Science (R0)