Abstract
Given a concrete domain \(\mathcal{C}\), a concrete operation \(\tau: \mathcal{C} \to \mathcal{C}\), and an abstract domain \(\mathcal{A}\), a fundamental problem in abstract interpretation is to find the best abstract transformer \(\tau^{\#}: \mathcal{A} \to \mathcal{A}\) that over-approximates τ. This problem, as well as several other operations needed by an abstract interpreter, can be reduced to the problem of symbolic abstraction: the symbolic abstraction of a formula ϕ in logic \(\mathcal{L}\), denoted by \(\widehat{\alpha}(\varphi)\), is the best value in \(\mathcal{A}\) that over-approximates the meaning of ϕ. When the concrete semantics of τ is defined in \(\mathcal{L}\) using a formula ϕ τ that specifies the relation between input and output states, the best abstract transformer τ # can be computed as \(\widehat{\alpha}(\varphi_\tau)\).
In this paper, we present a new framework for performing symbolic abstraction, discuss its properties, and present several instantiations for various logics and abstract domains. The key innovation is to use a bilateral successive-approximation algorithm, which maintains both an over-approximation and an under-approximation of the desired answer.
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, by AFRL under grants FA9550-09-1-0279 and FA8650-10-C-7088; and by DARPA under cooperative agreement HR0011-12-2-0012. 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
Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian Abstraction for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)
Barrett, E., King, A.: Range and set abstraction using SAT. ENTCS 267(1) (2010)
Brauer, J., King, A.: Automatic Abstraction for Intervals Using Boolean Formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 167–183. Springer, Heidelberg (2010)
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD 25(2-3) (2004)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)
Cousot, P., Cousot, R., Mauborgne, L.: Logical abstract domains and interpretations. In: The Future of Software Engineering (2011)
Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: POPL (1978)
Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Sym. Logic 22(3) (September 1957)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Dutertre, B., de Moura, L.: Yices: An SMT solver (2006), yices.csl.sri.com/
Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.: Abstract Domains of Affine Relations. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 198–215. Springer, Heidelberg (2011)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Gulwani, S., Musuvathi, M.: Cover Algorithms and Their Combination. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 193–207. Springer, Heidelberg (2008)
Kidd, N., Lal, A., Reps, T.: WALi: The Weighted Automaton Library (2007), http://www.cs.wisc.edu/wpis/wpds/download.php
King, A., Søndergaard, H.: Automatic Abstraction for Congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 197–213. Springer, Heidelberg (2010)
Lal, A., Reps, T.: Improving Pushdown System Model Checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 343–357. Springer, Heidelberg (2006)
Lal, A., Reps, T., Balakrishnan, G.: Extended Weighted Pushdown Systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 434–448. Springer, Heidelberg (2005)
Lassez, J.-L., Maher, M.J., Marriott, K.: Unification Revisited. In: Boscarol, M., Carlucci Aiello, L., Levi, G. (eds.) Foundations of Logic and Functional Programming. LNCS, vol. 306, pp. 67–113. Springer, Heidelberg (1988)
Lim, J., Reps, T.: A System for Generating Static Analyzers for Machine Instructions. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 36–52. Springer, Heidelberg (2008)
Miné, A.: The octagon abstract domain. In: WCRE, pp. 310–322 (2001)
Mitchell, T.: Machine Learning. WCB/McGraw-Hill, Boston (1997)
Monniaux, D.: Automatic modular abstractions for template numerical constraints. Logical Methods in Comp. Sci. 6(3) (2010)
Plotkin, G.: A note on inductive generalization. In: Machine Intelligence, vol. 5, pp. 153–165. Edinburgh Univ. Press (1970)
Regehr, J., Reid, A.: HOIST: A system for automatically deriving static analyzers for embedded systems. In: ASPLOS (2004)
Reps, T., Sagiv, M., Yorsh, G.: Symbolic Implementation of the Best Transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004)
Reynolds, J.: Transformational systems and the algebraic structure of atomic formulas. Machine Intelligence 5(1), 135–151 (1970)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217–298 (2002)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable Analysis of Linear Systems Using Mathematical Programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Sheeran, M., Stålmarck, G.: A tutorial on Stålmarck’s proof procedure for propositional logic. FMSD 16(1), 23–58 (2000)
Steffen, B., Knoop, J., Rüthing, O.: The value flow graph: A program representation for optimal program transformations. In: ESOP (1990)
Steffen, B., Knoop, J., Rüthing, O.: Efficient Code Motion and an Adaption to Strength Reduction. In: Abramsky, S., Maibaum, T.S.E. (eds.) TAPSOFT 1991, CCPSD 1991, and ADC-Talks 1991. LNCS, vol. 494, pp. 394–415. Springer, Heidelberg (1991)
Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. TR 1713, CS Dept., Univ. of Wisconsin, Madison, WI (March 2012), http://www.cs.wisc.edu/wpis/papers/tr1713.pdf
Thakur, A., Reps, T.: A Generalization of Stålmarck’s Method. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 334–351. Springer, Heidelberg (2012)
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)
Yorsh, G., Reps, T., Sagiv, M.: Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)
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., Elder, M., Reps, T. (2012). Bilateral Algorithms for Symbolic Abstraction. 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_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-33125-1_10
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)