Abstract
Declarative specifications exhibit a variety of problems, such as inadvertently overconstrained axioms and underconstrained conjectures, that are hard to diagnose with model checking and theorem proving alone. Recycling core extraction is a new coverage analysis that pinpoints an irreducible unsatisfiable core of a declarative specification. It is based on resolution refutation proofs generated by resolution engines, such as SAT solvers and resolution theorem provers. The extraction algorithm is described, and proved correct, for a generalized specification language with a regular translation to the input logic of a resolution engine. It has been implemented for the Alloy language and evaluated on a variety of specifications, with promising results.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. LCNS 2031, 528 (2001)
Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. In: Conference on Correct Hardware Design and Verification Methods, pp. 82–96 (1999)
Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: ASE 2003 (2003)
Shlyakhter, I.: Declarative Symbolic Pure Logic Model Checking. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA (2005)
Jackson, D.: Software Abstractions: logic, language, and analysis. MIT Press, Cambridge (2006)
Chang, F.: Alloy analyzer 4.0 (2007), http://alloy.mit.edu/alloy4/
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT solver. In: DATE 2002, pp. 142–149 (2002)
Mahajan, Y.S., Fu, Z., Malik, S.: zchaff2004: An efficient SAT solver. In: SAT (Selected Papers), pp. 360–375 (2004)
Kalman, J.A.: Automated Reasoning with Otter. Rinton Press (2001)
Riazanov, A.: Implementing an Efficient Theorem Prover. PhD Thesis, The University of Manchester, Manchester (2003)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Handbook of automated reasoning, pp. 1965–2013 (2001)
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)
Claessen, K., Sörensson, N.: New techniques that improve MACE-style finite model finding. In: CADE-19 Workshop on Model Computation, Miami, FL (2003)
Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. In: Journal of Applied Logic (2007)
Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)
Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. ORSA Journal of Computing 3(2), 157–158 (1991)
Dershowitz, N., Hanna, Z., Nadel, A.: A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 36–41. Springer, Heidelberg (2006)
Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE 2003 (2003)
Liffiton, M.H., Sakallah, K.A.: On Finding All Minimally Unsatisfiable Subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 173–186. Springer, Heidelberg (2005)
Lynce, I.: On computing minimum unsatisfiable cores. In: SAT 2004 (2004)
Mneimneh, M., Lynce, I., Andraus, Z.: A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 467–474. Springer, Heidelberg (2005)
Oh, Y., Mneimneh, M., Andraus, Z., Sakallah, K., Markov, I.: Amuse: A minimally-unsatisfiable subformula extractor. In: DAC, ACM/IEEE, pp. 518–523 (2004)
Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formula. In: SAT 2003 (2003)
Grégoire, E., Mazure, B., Piette, C.: Extracting MUSes. In: ECAI 2006, Trento, Italy, pp. 387–391 (2006)
Grégoire, E., Mazure, B., Piette, C.: Local-search extraction of MUSes. Constraints Journal 12(3), 324–344 (2007)
Grégoire, E., Mazure, B., Piette, C.: Boosting a complete technique to find MSS and MUS thanks to a local search oracle. In: IJCAI 2007, Hyderabad, India, vol. 2, pp. 2300–2305 (2007)
Dennis, G., Chang, F., Jackson, D.: Modular verification of code. In: ISSTA 2006, Portland, Maine (2006)
Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a sat solver. In: ESEC-FSE 2007, pp. 195–204. ACM, New York (2007)
Taghdiri, M.: Automating Modular Program Verification by Refining Specifications. PhD thesis, Massachusetts Institute of Technology (2007)
Yeung, V.: Declarative configuration applied to course scheduling. Master’s thesis, Massachusetts Institute of Technology, Cambridge (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Torlak, E., Chang, F.SH., Jackson, D. (2008). Finding Minimal Unsatisfiable Cores of Declarative Specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds) FM 2008: Formal Methods. FM 2008. Lecture Notes in Computer Science, vol 5014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68237-0_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-68237-0_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68235-6
Online ISBN: 978-3-540-68237-0
eBook Packages: Computer ScienceComputer Science (R0)