Trace Abstraction-Based Verification for Uninterpreted Programs | SpringerLink
Skip to main content
Springer Nature Link
Log in

Trace Abstraction-Based Verification for Uninterpreted Programs

  • Conference paper
  • First Online:
Formal Methods (FM 2021)

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

Included in the following conference series:

Abstract

The verification of uninterpreted programs is undecidable in general. This paper proposes to employ counterexample-guided abstraction refinement (CEGAR) framework for verifying uninterpreted programs. Different from the existing interpolant-based trace abstraction, we propose a congruence-based trace abstraction method for infeasible counterexample paths to refine the program’s abstraction model, which is designed specifically for uninterpreted programs. Besides, we propose an optimization method that utilizes the decidable verification result for coherent uninterpreted programs to improve the CEGAR framework’s efficiency. We have implemented our verification method and evaluated it on two kinds of benchmark programs. Compared with the state-of-the-art, our method is more effective and efficient, and achieves 3.6x speedups on average.

Weijiang Hong and Zhenbang Chen contributed equally to this work and are cofirst authors.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 12583
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 15729
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    Our implementation and benchmark are available at the GitHub repository https://github.com/Verifier4UP/Trace-Refinement-based-Verification.

  2. 2.

    SV-COMP is one of the most popular benchmarks for software verification.

References

  1. Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, 2001, pp. 203–213. ACM (2001). https://doi.org/10.1145/378795.378846

  2. Boogie Language: www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/

  3. Cassez, F., Jensen, P.G., Larsen, K.G.: Verification and parameter synthesis for real-time programs using refinement of trace abstraction. Fundam. Informaticae 178(1–2), 31–57 (2021). https://doi.org/10.3233/FI-2021-1997

  4. Cassez, F., Ziegler, F.: Verification of concurrent programs using trace abstraction refinement. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 233–248. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_17

  5. 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). https://doi.org/10.1007/978-3-642-31759-0_19

  6. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

  7. Heizmann, M., et al.: Ultimate automizer with SMTInterpol. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 641–643. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_53

  8. Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69–85. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03237-0_7

  9. Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, pp. 471–482. ACM (2010). https://doi.org/10.1145/1706299.1706353

  10. Hoder, K., Kovács, L., Voronkov, A.: Playing in the grey area of proofs. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, pp. 259–272. ACM (2012). https://doi.org/10.1145/2103656.2103689

  11. Kozen, D.: Automata and computability. Undergraduate texts in computer science, Springer (1997)

    Google Scholar 

  12. Kroening, D., Strichman, O.: Decision procedures - an algorithmic point of view, 2nd Edn. Texts in Theoretical Computer Science. An EATCS Series, Springer (2016). https://doi.org/10.1007/978-3-662-50497-0

  13. Krogmeier, P., et al.: Decidable synthesis of programs with uninterpreted functions. In: Lahiri, S. K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 634–657. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_32

  14. Leino, K., Rustan, M..: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

  15. Mathur, U., Madhusudan, P., Viswanathan, M.: Decidable verification of uninterpreted programs. In: Proceedings ACM Programing. Language 3(POPL), pp. 1–29 (2019). https://doi.org/10.1145/3290359

  16. Mathur, U., Madhusudan, P., Viswanathan, M.: What’s decidable about program verification modulo axioms?. In: TACAS 2020. LNCS, vol. 12079, pp. 158–177. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_10

  17. Mathur, U., Murali, A., Krogmeier, P., Madhusudan, P., Viswanathan, M.: Deciding memory safety for single-pass heap-manipulating programs. In: Proceedings ACM Programming Language 4(POPL), 1–29 (2020). https://doi.org/10.1145/3371103

  18. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980). https://doi.org/10.1145/322186.322198

    Article  MathSciNet  MATH  Google Scholar 

  19. SV-benchmarks: github.com/sosy-lab/sv-benchmarks

  20. Torre, S.L., Madhusudan, P.: Reachability in concurrent uninterpreted programs. In: Chattopadhyay, A., Gastin, P. (eds.) 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, Bombay, India. LIPIcs, vol. 150, pp. 1–16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.FSTTCS.2019.46

Download references

Acknowledgments

This research was supported by National Key R&D Program of China (No. 2017YFB1001802) and the NSFC Programs (No. 62172429, 61632015, 62032024, and 61690203).

Author information

Authors and Affiliations

  1. College of Computer, National University of Defense Technology, Changsha, China

    Weijiang Hong, Zhenbang Chen, Yide Du & Ji Wang

  2. State Key Laboratory of High Performance Computing, National University of Defense Technology, Changsha, China

    Weijiang Hong & Ji Wang

Authors
  1. Weijiang Hong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhenbang Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yide Du
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ji Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Contributions

Weijiang Hong and Zhenbang Chen contributed equally to this work and are co-first authors.

Corresponding authors

Correspondence to Zhenbang Chen or Ji Wang .

Editor information

Editors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Marieke Huisman

  2. NASA Ames Research Center, Moffett Field, CA, USA

    Corina Păsăreanu

  3. Institute of Software, Chinese Academy of Sciences, Beijing, China

    Naijun Zhan

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hong, W., Chen, Z., Du, Y., Wang, J. (2021). Trace Abstraction-Based Verification for Uninterpreted Programs. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science(), vol 13047. Springer, Cham. https://doi.org/10.1007/978-3-030-90870-6_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-90870-6_29

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-90869-0

  • Online ISBN: 978-3-030-90870-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation