Abstract
The paper presents a novel technique to create implementations of the basic primitives used in symbolic program analysis: forward symbolic evaluation, weakest liberal precondition, and symbolic composition. We used the technique to create a system in which, for the cost of writing just one specification—an interpreter for the programming language of interest—one obtains automatically-generated, mutually-consistent implementations of all three symbolic-analysis primitives. This can be carried out even for languages with pointers and address arithmetic. Our implementation has been used to generate symbolic-analysis primitives for x86 and PowerPC.
Supported by NSF under grants CCF-{0540955, 0524051, 0810053}, by AFRL under contract FA8750-06-C-0249, and by ONR under grant N00014-09-1-0510.
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.
Similar content being viewed by others
References
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI (2001)
Beckman, N., Nori, A., Rajamani, S., Simmons, R.: Proofs from tests. In: ISSTA (2008)
Brumley, D., Hartwig, C., Liang, Z., Newsome, J., Poosankam, P., Song, D., Yin, H.: Automatically identifying trigger-based behavior in malware. In: Botnet Analysis and Defense. Springer, Heidelberg (2008)
Cousot, P., Cousot, R.: Abstract interpretation. In: POPL (1977)
Ganesh, V., Dill, D.: A decision procesure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)
Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: PLDI (2005)
Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: NDSS (2008)
Jhala, R., Majumdar, R.: B2: Software model checking for C (2009), http://www.cs.ucla.edu/~rupak/b2/
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)
Malmkjær, K.: Abstract Interpretation of Partial-Evaluation Algorithms. PhD thesis, Dept. of Comp. and Inf. Sci., Kansas State Univ. (1993)
Morris, J.: A general axiom of assignment. In: Broy, M., Schmidt, G. (eds.) Theor. Found. of Program. Methodology. Reidel, Dordrechtz (1982)
Mycroft, A., Jones, N.: A relational framework for abstract interpretation. In: PADO (1985)
Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: FSE (2005)
**e, Y., Aiken, A.: Saturn: A scalable framework for error detection using Boolean satisfiability. TOPLAS 29(3) (2007)
**e, Y., Chou, A., Engler, D.: ARCHER: Using symbolic, path-sensitive analysis to detect memory access errors. In: FSE (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lim, J., Lal, A., Reps, T. (2009). Symbolic Analysis via Semantic Reinterpretation. In: Păsăreanu, C.S. (eds) Model Checking Software. SPIN 2009. Lecture Notes in Computer Science, vol 5578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02652-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-02652-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02651-5
Online ISBN: 978-3-642-02652-2
eBook Packages: Computer ScienceComputer Science (R0)