Computing Specification-Sensitive Abstractions for Program Verification

  • Tianhai LiuEmail author
  • Shmuel Tyszberowicz
  • Mihai Herda
  • Bernhard Beckert
  • Daniel Grahl
  • Mana Taghdiri
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


To enable scalability and address the needs of real-world software, deductive verification relies on modularization of the target program and decomposition of its requirement specification. In this paper, we present an approach that, given a Java program and a partial requirement specification written using the Java Modeling Language, constructs a semantic slice. In the slice, the parts of the program irrelevant w.r.t. the partial requirements are replaced by an abstraction. The core idea of our approach is to use bounded program verification techniques to guide the construction of these slices. Our approach not only lessens the burden of writing auxiliary specifications (such as loop invariants) but also reduces the number of proof steps needed for verification.


Original Program Symbolic Execution Java Modeling Language Partial Property Program Verification 
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.



This work has been partially supported by GIF (grant No. 1131-9.6/2011) and by DFG under project “DeduSec” within SPP 1496 “RS3” and by BMBF under project FIfAKS within the Software Campus program.


  1. 1.
    Ahrendt, W., et al.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55–71. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-12154-3_4 Google Scholar
  2. 2.
    Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-24756-2_1 CrossRefGoogle Scholar
  3. 3.
    Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, The University of Iowa (2015)Google Scholar
  4. 4.
    Barros, J.B., da Cruz, C.D., Henriques, P.R., Pinto, J.S.: Assertion-based slicing and slice graphs. Formal Asp. Comput. 24(2), 217–248 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT 9(5–6), 505–525 (2007)CrossRefGoogle Scholar
  6. 6.
    Bormer, T.: Advancing Deductive Program-Level Verification for Real-World Application: Lessons Learned from an Industrial Case Study. Ph.D. thesis, KIT (2014)Google Scholar
  7. 7.
    Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng. 30(6), 388–402 (2004)CrossRefGoogle Scholar
  8. 8.
    Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC, pp. 1284–1291. ACM (2012)Google Scholar
  9. 9.
    Chung, I.S.: Program slicing based on specification. In: SAC, pp. 605–609. ACM (2001)Google Scholar
  10. 10.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-31980-1_40 CrossRefGoogle Scholar
  11. 11.
    Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-03359-9_2 CrossRefGoogle Scholar
  12. 12.
    Comuzzi, J.J., Hart, J.M.: Program slicing using weakest preconditions. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 557–575. Springer, Heidelberg (1996). doi: 10.1007/3-540-60973-3_107 CrossRefGoogle Scholar
  13. 13.
    da Cruz, D.C., Henriques, P.R., Pinto, J.S.: GamaSlicer: an online laboratory for program verification and analysis. In: LDTA. ACM (2010)Google Scholar
  14. 14.
    Dennis, G.D.: A Relational Framework for Bounded Program Verification. Ph.D. thesis, MIT (2009)Google Scholar
  15. 15.
    Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 351–368. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-23702-7_26 CrossRefGoogle Scholar
  16. 16.
    Ghazi, A.A., Ulbrich, M., Gladisch, C., Tyszberowicz, S., Taghdiri, M.: JKelloy: a proof assistant for relational specifications of Java programs. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 173–187. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-06200-6_13 CrossRefGoogle Scholar
  17. 17.
    Fox, C., Danicic, S., Harman, M., Hierons, R.M.: ConSIT: a fully automated conditioned program slicer. Softw. Pract. Experience 34(1), 15–46 (2004)CrossRefGoogle Scholar
  18. 18.
    Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. ACM SIGPLAN Not. 46(1), 331–344 (2011)CrossRefzbMATHGoogle Scholar
  19. 19.
    Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 634–640. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02658-4_48 CrossRefGoogle Scholar
  20. 20.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2012)Google Scholar
  21. 21.
    King, J.C.: Symbolic execution and program testing. CACM 19(7), 385–394 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT SEN 31(3), 1–38 (2006)CrossRefGoogle Scholar
  23. 23.
    Liu, T., Nagel, M., Taghdiri, M.: Bounded program verification using an SMT solver: a case study. In: ICST, pp. 101–110. IEEE (2012)Google Scholar
  24. 24.
    Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146–161. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-27705-4_12 CrossRefGoogle Scholar
  25. 25.
    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). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  26. 26.
    Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. Autom. Softw. Eng. 14(1), 87–121 (2007)CrossRefGoogle Scholar
  27. 27.
    Vaziri, M.: Finding Bugs in Software with a Constraint Solver. Ph.D. thesis, MIT (2004)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Tianhai Liu
    • 1
    Email author
  • Shmuel Tyszberowicz
    • 3
  • Mihai Herda
    • 1
  • Bernhard Beckert
    • 1
  • Daniel Grahl
    • 1
  • Mana Taghdiri
    • 2
  1. 1.Karlsruhe Institute of TechnologyKarlsruheGermany
  2. 2.Horus Software GmbHEttlingenGermany
  3. 3.The Academic College Tel Aviv YaffoTel AvivIsrael

Personalised recommendations