Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring

  • Falk HowarEmail author
  • Dimitra Giannakopoulou
  • Malte Mues
  • Jorge A. Navas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


Behavioral interfaces describe the safe interactions with a component without exposing its internal variables and computation. As such, they can serve as documentation or formal contracts for black-box components in safety-critical systems. Learning-based generation of interaces relies on learning algorithms for inferring behavioral interfaces from observations, which are in turn checked for correctness by formal analysis techniques. Learning-based interface generation is therefore an interesting target when studying integration and combination of different formal analysis methods. In this paper, which accompanies an invited talk at the ISoLA 2018 track “A Broader View on Verification: From Static to Runtime and Back”, we introduce interpolation and symbolic search for validating inferred interfaces. We discuss briefly how interface validation may utilize information from runtime monitoring.


  1. 1.
    Alur, R., Cerný, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 98–109 (2005)Google Scholar
  2. 2.
    Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 146–162. Springer, Heidelberg (2006). Scholar
  4. 4.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). Scholar
  5. 5.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.-J.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)Google Scholar
  6. 6.
    Caso, G.D., Braberman, V., Garbervetsky, D., Uchitel, S.: Enabledness-based program abstractions for behavior validation. ACM Trans. Softw. Eng. Methodol. 22(3), 25:1–25:46 (2013)CrossRefGoogle Scholar
  7. 7.
    Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012). Scholar
  8. 8.
    Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). Scholar
  9. 9.
    Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 365–373. Springer, Heidelberg (1990). Scholar
  10. 10.
    Craig, W.: Three uses of Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Comput. 22, 269–285 (1955)MathSciNetzbMATHGoogle Scholar
  11. 11.
    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). Scholar
  12. 12.
    Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009). Scholar
  13. 13.
    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). Scholar
  14. 14.
    Giannakopoulou, D., Rakamarić, Z., Raman, V.: Symbolic learning of component interfaces. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 248–264. Springer, Heidelberg (2012). Scholar
  15. 15.
    Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2005, pp. 213–223. ACM (2005)Google Scholar
  16. 16.
    Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. In: European Software Engineering Conference (ESEC) Held Jointly with ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 31–40 (2005)Google Scholar
  17. 17.
    Howar, F., Giannakopoulou, D., Rakamaric, Z.: Hybrid learning: interface generation through static, dynamic, and symbolic analysis. In: ISSTA 2013, pp. 268–279 (2013)Google Scholar
  18. 18.
    Howar, F., Kahsai, T., Gurfinkel, A., Tinelli, C.: Trusting outsourced components in flight critical systems. In: AIAA Infotech@ Aerospace. AIAA (2015)Google Scholar
  19. 19.
    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). Scholar
  20. 20.
    Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307–322. Springer, Cham (2014). Scholar
  21. 21.
    Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib - a framework for active automata learning. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 487–495. Springer, Cham (2015). Scholar
  22. 22.
    Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758–766. Springer, Heidelberg (2012). Scholar
  23. 23.
    Jaffar, J., Navas, J.A., Santosa, A.E.: Unbounded symbolic execution for program verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 396–411. Springer, Heidelberg (2012). Scholar
  24. 24.
    Jaffar, J., Santosa, A.E., Voicu, R.: An interpolation method for CLP traversal. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 454–469. Springer, Heidelberg (2009). Scholar
  25. 25.
    Luckow, K., et al.: JDart: a dynamic symbolic analysis framework. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 442–459. Springer, Heidelberg (2016). Scholar
  26. 26.
    McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002). Scholar
  27. 27.
    McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104–118. Springer, Heidelberg (2010). Scholar
  28. 28.
    Mues, M., Howar, F., Luckow, K.S., Kahsai, T., Rakamaric, Z.: Releasing the PSYCO: using symbolic search in interface generation for Java. ACM SIGSOFT Softw. Eng. Notes 41(6), 1–5 (2016)CrossRefGoogle Scholar
  29. 29.
    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). Scholar
  30. 30.
    Wintersteiger, C.M., Hamadi, Y., De Moura, L.: Efficiently solving quantified bit-vector formulas. Form. Methods Syst. Des. 42(1), 3–23 (2013)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Falk Howar
    • 1
    Email author
  • Dimitra Giannakopoulou
    • 2
  • Malte Mues
    • 3
  • Jorge A. Navas
    • 4
  1. 1.Dortmund University of Technology and Fraunhofer ISSTDortmundGermany
  2. 2.NASA Ames Research CenterMoffett FieldUSA
  3. 3.Dortmund University of TechnologyDortmundGermany
  4. 4.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations