Abstract
Given a white-box component 
with specified unsafe states, we address the problem of automatically generating an interface that captures safe orderings of invocations of 
’s public methods. Method calls in the generated interface are guarded by constraints on their parameters. Unlike previous work, these constraints are generated automatically through an iterative refinement process. Our technique, named Psyco (Predicate-based SYmbolic COmpositional reasoning), employs a novel combination of the L* automata learning algorithm with symbolic execution. The generated interfaces are three-valued, capturing whether a sequence of method invocations is safe, unsafe, or its effect on the component state is unresolved by the symbolic execution engine. We have implemented Psyco as a new prototype tool in the JPF open-source software model checking platform, and we have successfully applied it to several examples.
This research was supported by the NASA CMU grant NNA10DE60C.
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
Aarts, F., Jonsson, B., Uijen, J.: Generating models of infinite-state communication protocols using regular inference with abstraction. In: ICTSS, pp. 188–204 (2010)
Alur, R., Cerný, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: POPL, pp. 98–109 (2005)
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: A complete and automatic linearizability checker. In: PLDI, pp. 330–340 (2010)
Chaki, S., Strichman, O.: Three optimizations for assume-guarantee reasoning with L*. FMSD 32(3), 267–284 (2008)
Chen, Y.-F., Clarke, E.M., Farzan, A., Tsai, M.-H., Tsay, Y.-K., Wang, B.-Y.: Automated Assume-Guarantee Reasoning through Implicit Learning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 511–526. Springer, Heidelberg (2010)
Chen, Y.-F., Farzan, A., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Learning Minimal Separating DFA’s for Compositional Verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 31–45. Springer, Heidelberg (2009)
Cho, C.Y., Babić, D., Poosankam, P., Chen, K.Z., Wu, E.X., Song, D.: MACE: Model-inference-assisted concolic exploration for protocol and vulnerability discovery. In: USENIX Security Symposium (2011)
Dutertre, B., Moura, L.D.: The Yices SMT solver. Technical report, SRI International (2006)
Gheorghiu, M., Giannakopoulou, D., Păsăreanu, C.S.: Refining Interface Alphabets for Compositional Verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 292–307. Springer, Heidelberg (2007)
Giannakopoulou, D., Păsăreanu, C.S.: Interface Generation and Compositional Verification in JavaPathfinder. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 94–108. Springer, Heidelberg (2009)
Giannakopoulou, D., Rakamarić, Z., Raman, V.: Symbolic learning of component interfaces. Technical report, NASA Ames Research Center (2012)
Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. SIGPLAN Not. 40(6), 213–223 (2005)
Guava: Google core libraries, http://code.google.com/p/guava-libraries/
Gupta, A., McMillan, K.L., Fu, Z.: Automated Assumption Generation for Compositional Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 420–432. Springer, Heidelberg (2007)
Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: ESEC/FSE, pp. 31–40 (2005)
Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring Canonical Register Automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251–266. Springer, Heidelberg (2012)
Howar, F., Steffen, B., Merten, M.: Automata Learning with Automated Alphabet Abstraction Refinement. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 263–277. Springer, Heidelberg (2011)
Joshi, S., Lahiri, S.K., Lal, A.: Underspecified harnesses and interleaved bugs. In: POPL, pp. 19–30 (2012)
Java PathFinder (JPF), http://babelfish.arc.nasa.gov/trac/jpf
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. FMSD 32(3), 175–205 (2008)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Inf. Comput. 103(2), 299–347 (1993)
Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: ESEC/FSE, pp. 263–272 (2005)
Singh, R., Giannakopoulou, D., Păsăreanu, C.: Learning Component Interfaces with May and Must Abstractions. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 527–542. Springer, Heidelberg (2010)
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
Giannakopoulou, D., Rakamarić, Z., Raman, V. (2012). Symbolic Learning of Component Interfaces. 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_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-33125-1_18
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)