Skip to main content
SpringerLink
Log in

Program Transformation Based on Symbolic Execution and Deduction

  • Conference paper
Software Engineering and Formal Methods (SEFM 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8137))

Included in the following conference series:

Abstract

We present a program transformation framework based on symbolic execution and deduction. Its virtues are: (i) behavior preservation of the transformed program is guaranteed by a sound program logic, and (ii) automated first-order solvers are used for simplification and optimization. Transformation consists of two phases: first the source program is symbolically executed by sequent calculus rules in a program logic. This involves a precise analysis of variable dependencies, aliasing, and elimination of infeasible execution paths. In the second phase, the target program is synthesized by a leaves-to-root traversal of the symbolic execution tree by backward application of (extended) sequent calculus rules. We prove soundness by a suitable notion of bisimulation and we discuss one possible approach to automated program optimization.

This work has been partially supported by the IST program of the European Commission, Future and Emerging Technologies under the IST-231620 HATS project.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alkassar, E., Hillebrand, M.A., Paul, W.J., Petrova, E.: Automated verification of a small hypervisor. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 40–54. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  2. Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification – specification is the new bottleneck. In: SSV. EPTCS, vol. 102, pp. 18–32 (2012)

    Google Scholar 

  3. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  4. Bubel, R., Hähnle, R., Ji, R.: Program specialization via a software verification tool. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 80–101. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Sangiorgi, D.: Introduction to Bisimulation and Coinduction (2011)

    Google Scholar 

  6. King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)

    Article  MATH  Google Scholar 

  7. Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool: integrating object oriented design and formal verification. SoSyM 4(1), 32–54 (2005)

    Article  Google Scholar 

  8. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)

    Google Scholar 

  9. Ji, R., Hähnle, R., Bubel, R.: Program transformation based on symbolic execution and deduction, technical report (2013)

    Google Scholar 

  10. Bubel, R., Hähnle, R., Ji, R.: Interleaving symbolic execution and partial evaluation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 125–146. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60-61, 17–139 (2004)

    Article  MathSciNet  Google Scholar 

  12. Kahn, G.: Natural semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  13. Rümmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 422–436. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for Java. ACM-TPLS 25(4), 452–499 (2003)

    Article  Google Scholar 

  15. Ruf, E.S.: Topics in online partial evaluation. PhD thesis, Stanford University, Stanford, CA, USA, UMI Order No. GAX93-26550 (1993)

    Google Scholar 

  16. Hatcliff, J., Danvy, O.: A computational formalization for partial evaluation. Mathematical Structures in Computer Science 7(5), 507–541 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  17. Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM 50, 63–69 (2003)

    Article  Google Scholar 

  18. Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  19. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Barthe, G., Crespo, J.M., Gulwani, S., Kunz, C., Marron, M.: From relational verification to SIMD loop synthesis. In: PPOPP, pp. 123–134. ACM (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technische Universität Darmstadt, Germany

    Ran Ji, Reiner Hähnle & Richard Bubel

Authors
  1. Ran Ji
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Richard Bubel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Information Systems, Computing and Mathematics, Brunel University, UB8 3PH, Uxbridge, Middlesex, UK

    Robert M. Hierons

  2. Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid, 28040, Madrid, Spain

    Mercedes G. Merayo

  3. Dipartimento di Scienze dell’Informazione, Università di Bologna, 40127, Bologna, Italy

    Mario Bravetti

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ji, R., Hähnle, R., Bubel, R. (2013). Program Transformation Based on Symbolic Execution and Deduction. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science, vol 8137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40561-7_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40561-7_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40560-0

  • Online ISBN: 978-3-642-40561-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation