Abstract
This paper concerns how to automatically create abstractions for program analysis. We show that inductive learning, the goal of which is to identify general rules from a set of observed instances, provides new leverage on the problem. An advantage of an approach based on inductive learning is that it does not require the use of a theorem prover.
Chapter PDF
Similar content being viewed by others
References
TVLA system, http://www.cs.tau.ac.il/~tvla/
Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Chase, D.R., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: PLDI, pp. 296–310 (1990)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV, pp. 154–169 (2000)
Das, S., Dill, D.: Counter-example based predicate discovery in predicate abstraction. In: FMCAD, pp. 19–32 (2002)
Flanagan, C.: Software model checking via iterative abstraction refinement of constraint logic queries. In: CP+CV (2004)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)
Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL, pp. 232–244 (2004)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: The boundary between decidability and undecidability for transitive closure logics. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 160–174. Springer, Heidelberg (2004)
Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 39–50. Springer, Heidelberg (1999)
Jones, N., Muchnick, S.: Flow analysis and optimization of Lisp-like structures. In: Program Flow Analysis: Theory and Applications, pp. 102–131. Prentice-Hall, Englewood Cliffs (1981)
Kurshan, R.: Computer-aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)
Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001)
Lavrač, N., Džeroski, S.: Inductive Logic Programming: Techniques and Applications. Ellis Horwood (1994)
Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: ISSTA, pp. 26–38 (2000)
Loginov, A., Reps, T., Sagiv, M.: Learning abstractions for verifying data-structure properties. report TR-1519, Comp. Sci. Dept., Univ. of Wisconsin (January 2005), Available at http://www.cs.wisc.edu/wpis/papers/tr1519.ps
Muggleton, S.: Inductive logic programming. New Generation Comp. 8(4), 295–317 (1991)
Pasareanu, C., Dwyer, M., Visser, W.: Finding feasible counter-examples when model checking Java programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 284–298. Springer, Heidelberg (2001)
Quinlan, J.R.: Learning logical definitions from relations. Mach. Learn. 5, 239–266 (1990)
Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas with applications to program analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 380–398. Springer, Heidelberg (2003)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217–298 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Loginov, A., Reps, T., Sagiv, M. (2005). Abstraction Refinement via Inductive Learning. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_50
Download citation
DOI: https://doi.org/10.1007/11513988_50
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
