Skip to main content
SpringerLink
Log in

Using Program Synthesis for Program Analysis

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9450))

Included in the following conference series:

Abstract

In this paper, we propose a unified framework for designing static analysers based on program synthesis. For this purpose, we identify a fragment of second-order logic with restricted quantification that is expressive enough to capture numerous static analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We call this fragment the synthesis fragment. We build a decision procedure for the synthesis fragment over finite domains in the form of a program synthesiser. Given our initial motivation to solve static analysis problems, this synthesiser is specialised for such analyses. Our experimental results show that, on benchmarks capturing static analysis problems, our program synthesiser compares positively with other general purpose synthesisers.

This research was supported by ERC project 280053 (CPROVER).

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 EPUB and 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

References

  1. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)

    Google Scholar 

  2. Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: DAC, pp. 368–371 (2003)

    Google Scholar 

  3. Floyd, R.W.: Assigning meanings to programs (1967)

    Google Scholar 

  4. Gupta, A., et al.: Proving non-termination. In: POPL (2008)

    Google Scholar 

  5. Gulwani, S.: Dimensions in program synthesis. In: Formal Methods in Computer-Aided Design, FMCAD, p. 1 (2010)

    Google Scholar 

  6. Kong, S., Jung, Y., David, C., Wang, B.-Y., Yi, K.: Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 328–343. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Alur, R., et al.: Syntax-guided synthesis. In: FMCAD (2013)

    Google Scholar 

  8. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405–416 (2012)

    Google Scholar 

  9. Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869–882. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. In: FMCAD (2010)

    Google Scholar 

  11. Piskac, R., de Moura, L.M., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning 44(4), 401–424 (2010)

    Article  MATH  Google Scholar 

  12. Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281–292 (2008)

    Google Scholar 

  13. David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 183–204. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  14. David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. CoRR abs/1508.07829 (2015)

    Google Scholar 

  15. Solar-Lezama, A.: Program sketching. STTT 15(5–6), 475–495 (2013)

    Article  Google Scholar 

  16. Brain, M., Crick, T., De Vos, M., Fitch, J.: TOAST: applying answer set programming to superoptimisation. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 270–284. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  17. Langdon, W.B., Poli, R.: Foundations of Genetic Programming. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  18. Brameier, M., Banzhaf, W.: Linear Genetic Programming. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  19. Gomez, F., Miikkulainen, R.: Incremental evolution of complex general behavior. Adapt. Behav. 5, 317–342 (1997)

    Article  Google Scholar 

  20. Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62–73 (2011)

    Google Scholar 

  21. SV-COMP. http://sv-comp.sosy-lab.org/2015/

  22. David, C., Kroening, D., Lewis, M.: Danger invariants. CoRR (2015)

    Google Scholar 

  23. Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 198–216. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  24. StarExec. https://www.starexec.org

  25. Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69–87. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oxford, Oxford, UK

    Cristina David, Daniel Kroening & Matt Lewis

  2. Improbable Worlds Ltd., London, UK

    Matt Lewis

Authors
  1. Cristina David
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daniel Kroening
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Matt Lewis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cristina David .

Editor information

Editors and Affiliations

  1. New York University, New York, New York, USA

    Martin Davis

  2. University of the South Pacific, Suva, Fiji

    Ansgar Fehnker

  3. Macquarie University, Sydney, New South Wales, Australia

    Annabelle McIver

  4. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

David, C., Kroening, D., Lewis, M. (2015). Using Program Synthesis for Program Analysis. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48899-7_34

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48898-0

  • Online ISBN: 978-3-662-48899-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation