Abstract
This paper gives an account of Stålmarck’s method for validity checking of propositional-logic formulas, and explains each of the key components in terms of concepts from the field of abstract interpretation. We then use these insights to present a framework for propositional-logic validity-checking algorithms that is parametrized by an abstract domain and operations on that domain. Stålmarck’s method is one instantiation of the framework; other instantiations lead to new decision procedures for propositional logic.
Supported, in part, by NSF under grants CCF-{0810053, 0904371}, by ONR under grants N00014-{09-1-0510, 10-M-0251, 11-C-0447}, by ARL under grant W911NF-09-1-0413, and by AFRL under grants FA9550-09-1-0279 and FA8650-10-C-7088. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors, and do not necessarily reflect the views of the sponsoring agencies.
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
Björk, M.: First order Stålmarck. J. Autom. Reasoning 42(1), 99–122 (2009)
Cook, B., Gonthier, G.: Using Stålmarck’s Algorithm to Prove Inequalities. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 330–344. Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)
D’Silva, V., Haller, L., Kroening, D.: Satisfiability Solvers Are Static Analyzers. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 317–333. Springer, Heidelberg (2012)
D’Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric Bounds Analysis with Conflict-Driven Learning. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48–63. Springer, Heidelberg (2012)
Eén, N., Sjørensson, N.: The MiniSat solver (2006), minisat.se/MiniSat.html
Granger, P.: Improving the Results of Static Analyses Programs by Local Decreasing Iteration (Extended Abstract). In: Shyamasundar, R. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 68–79. Springer, Heidelberg (1992)
Harrison, J.: Stålmarck’s Algorithm as a HOL Derived Rule. In: von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 221–234. Springer, Heidelberg (1996)
Kunz, W., Pradhan, D.: Recursive learning: A new implication technique for efficient solutions to CAD problems–test, verification, and optimization. IEEE Trans. on CAD of Integrated Circuits and Systems 13(9), 1143–1158 (1994)
Marques Silva, J., Sakallah, K.: GRASP – a new search algorithm for satisfiability. In: ICCAD (1996)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC (2001)
Sheeran, M., Stålmarck, G.: A tutorial on Stålmarck’s proof procedure for propositional logic. FMSD 16(1), 23–58 (2000)
Spence, I.: tts: A SAT-solver for small, difficult instances. Journal on Sat., Boolean Modeling and Computation (2008), Benchmarks http://www.cs.qub.ac.uk/~i.spence/sdsb
Stålmarck, G.: A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula (1989), Swedish Patent No. 467,076 (approved 1992); U.S. Patent No. 5,276,897 (approved 1994); European Patent No. 403,454 (approved 1995)
Stålmarck, G., Säflund, M.: Modeling and verifying systems and software in propositional logic. In: Int. Conf. on Safety of Computer Controls Systems (1990)
Thakur, A., Reps, T.: A generalization of Stålmarck’s method. TR 1699 (revised), CS Dept., Univ. of Wisconsin, Madison, WI (June 2012), www.cs.wisc.edu/wpis/papers/tr1699r.pdf
Thakur, A., Reps, T.: A Method for Symbolic Computation of Abstract Operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174–192. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thakur, A., Reps, T. (2012). A Generalization of Stålmarck’s Method. In: Miné, A., Schmidt, D. (eds) Static Analysis. SAS 2012. Lecture Notes in Computer Science, vol 7460. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33125-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-33125-1_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33124-4
Online ISBN: 978-3-642-33125-1
eBook Packages: Computer ScienceComputer Science (R0)