Generation of Violation Witnesses by Under-Approximating Abstract Interpretation | SpringerLink
Skip to main content
Springer Nature Link
Log in

Generation of Violation Witnesses by Under-Approximating Abstract Interpretation

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14499))

Abstract

This works studies abstract backward semantics to infer sufficient program preconditions, based on an idea first proposed in previous work [38]. This analysis exploits under-approximated domain operators, demonstrated in [38] for the polyhedra domain, to under-approximate Dijkstra’s liberal precondition. The results of the analysis were implemented into a static analysis tool for a toy language. In this paper we address some limitations that hinder its applicability to C-like programs. In particular, we focus on two improvements: handling of user input and integer wrapping. For this, we extend the semantic and design sound and effective abstractions. Furthermore, to improve the precision, we explore an under-approximated version of the power-set construction. This in particular helps handling arbitrary union that is difficult to implement with under-approximated domains. The improved analysis is implemented and its performance is compared with other static analysis tools in SV-COMP23 using a selected subset of benchmarks.

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

Data Availability Statement

All the software used for the experimental part of this work was released in an artifact [35]. It includes not only the source code of the Banal static analyzer, but also the benchmarks and scripts used to produce the Tables 1, 2.

Notes

  1. 1.

    With an abuse of notation we confuse the store \([x \mapsto z]\) with z.

  2. 2.

    A lower (or dual) widening \(\underline{\nabla }^\sharp : D^\sharp \times D^\sharp \rightarrow D^\sharp \) is a binary operator such that: 1. for all \(d^\sharp _1, d^\sharp _2 \in D^\sharp \), \(\gamma ^\sharp (d^\sharp _1 \;\underline{\nabla }^\sharp \, d^\sharp _2) \subseteq \gamma ^\sharp (d^\sharp _1) \cap \gamma ^\sharp (d^\sharp _2)\); 2. for any sequence \((x_i^\sharp )_{i \in \mathbb {N}}\), the sequence defined as \(y_0^\sharp \triangleq x_0^\sharp \) and \(y_{i+1}^\sharp \triangleq y_{i}^\sharp \;\underline{\nabla }^\sharp \, x_{i+1}^\sharp \) becomes stable in a finite number of iterations.

  3. 3.

    With an abuse of notation, we confuse \(\{ x \} \rightarrow \mathbb {Z}\) with \(\mathbb {Z}\).

References

  1. The banal static analyzer prototype. http://www.di.ens.fr/~mine/banal. Accessed 11 Sep 2023

  2. Afzal, M., et al.: Veriabs: verification by abstraction and test generation. In: 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1138–1141. IEEE (2019)

    Google Scholar 

  3. Ascari, F., Bruni, R., Gori, R.: Limits and difficulties in the design of under-approximation abstract domains. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 21–39. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99253-8_2

    Chapter  Google Scholar 

  4. Bagnara, R., Hill, P.M., Zaffanella, E.: Exact join detection for convex polyhedra and other numerical abstractions. Comput. Geom. 43(5), 453–473 (2010)

    Article  MathSciNet  Google Scholar 

  5. Baldoni, R., Coppa, E., D’elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 1–39 (2018)

    Google Scholar 

  6. Bemporad, A., Fukuda, K., Torrisi, F.D.: Convexity recognition of the union of polyhedra. Comput. Geom. 18(3), 141–154 (2001)

    Article  MathSciNet  Google Scholar 

  7. Beyer, D.: Competition on software verification and witness validation: Sv-comp 2023. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 495–522. Springer (2023). https://doi.org/10.1007/978-3-031-30820-8_29

  8. Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 721–733 (2015)

    Google Scholar 

  9. Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 3–23. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92994-1_1

    Chapter  Google Scholar 

  10. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  Google Scholar 

  11. Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21, 1–29 (2019)

    Article  Google Scholar 

  12. Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, pp. 46–55 (1993)

    Google Scholar 

  13. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM (JACM) 50(5), 752–794 (2003)

    Article  MathSciNet  Google Scholar 

  14. Colóon, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67–81. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_6

    Chapter  Google Scholar 

  15. Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_37

    Chapter  Google Scholar 

  16. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 238–252 (1977)

    Google Scholar 

  17. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles Of Programming Languages, pp. 269–282 (1979)

    Google Scholar 

  18. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13(2–3), 103–179 (1992)

    Article  MathSciNet  Google Scholar 

  19. Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Softw. Eng. 6(1), 69–95 (1999)

    Article  Google Scholar 

  20. Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 150–168. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_12

    Chapter  Google Scholar 

  21. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 84–96 (1978)

    Google Scholar 

  22. Dangl, M., Löwe, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 423–425. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_34

    Chapter  Google Scholar 

  23. Darke, P., Agrawal, S., Venkatesh, R.: VeriAbs: a tool for scalable verification by abstraction (competition contribution). In: TACAS 2021. LNCS, vol. 12652, pp. 458–462. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72013-1_32

    Chapter  Google Scholar 

  24. de Vries, E., Koutavas, V.: Reverse hoare logic. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 155–171. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_12

    Chapter  Google Scholar 

  25. Delmas, D., Miné, A.: Analysis of software patches using numerical abstract interpretation. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 225–246. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32304-2_12

    Chapter  Google Scholar 

  26. Filé, G., Ranzato, F.: The powerset operator on abstract interpretations. Theoret. Comput. Sci. 222(1–2), 77–111 (1999)

    Article  MathSciNet  Google Scholar 

  27. Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Interval analysis and machine arithmetic: Why signedness ignorance is bliss. ACM Trans. Programming Lang. Syst. (TOPLAS) 37(1), 1–35 (2015)

    Article  Google Scholar 

  28. Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452–466. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_41

    Chapter  Google Scholar 

  29. Gotlieb, A., Leconte, M., Marre, B.: Constraint solving on modular integers. In: ModRef Worksop, Associated to CP 2010 (2010)

    Google Scholar 

  30. Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_2

    Chapter  Google Scholar 

  31. Journault, M., Miné, A., Ouadjaout, A.: An abstract domain for trees with numeric relations. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 724–751. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_26

    Chapter  Google Scholar 

  32. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  Google Scholar 

  33. Le, Q.L., Raad, A., Villard, J., Berdine, J., Dreyer, D., O’Hearn, P.W.: Finding real bugs in big programs with incorrectness logic. Proc. ACM Programming Lang. 6(OOPSLA1), 1–27 (2022)

    Article  Google Scholar 

  34. Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Tr-2007-12-01, Tel Aviv University (2007)

    Google Scholar 

  35. Marco, M., Miné, A.: Artifact of paper: Generation of Violation Witnesses by Under-Approximating Abstract Interpretation (Oct 2023). https://doi.org/10.5281/zenodo.8399723

  36. Miné, A.: The octagon abstract domain. Higher-Order Symbolic Comput. 19, 31–100 (2006)

    Article  Google Scholar 

  37. Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_23

    Chapter  Google Scholar 

  38. Miné, A.: Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program. 93, 154–182 (2014)

    Article  Google Scholar 

  39. Miné, A., et al.: Tutorial on static inference of numeric invariants by abstract interpretation. Foundation Trends® Programming Lang. 4(3–4), 120–372 (2017)

    Google Scholar 

  40. Moy, Y.: Sufficient preconditions for modular assertion checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 188–202. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78163-9_18

    Chapter  Google Scholar 

  41. O’Hearn, P.W.: Incorrectness logic. Proc. ACM Programming Lang. 4(POPL), 1–32 (2019)

    Google Scholar 

  42. Raad, A., Berdine, J., Dang, H.-H., Dreyer, D., O’Hearn, P., Villard, J.: Local reasoning about the presence of bugs: incorrectness separation logic. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 225–252. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_14

    Chapter  Google Scholar 

  43. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE (2002)

    Google Scholar 

  44. Schmidt, D.A.: A calculus of logical relations for over-and underapproximating static analyses. Sci. Comput. Program. 64(1), 29–53 (2007)

    Article  MathSciNet  Google Scholar 

  45. Sen, R., Srikant, Y.: Executable analysis using abstract interpretation with circular linear progressions. In: 2007 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2007), pp. 39–48. IEEE (2007)

    Google Scholar 

  46. Simon, A., King, A.: Taming the wrapping of integer arithmetic. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 121–136. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_8

  47. Urban, C., Ueltschi, S., Müller, P.: Abstract interpretation of CTL properties. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 402–422. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_24

    Chapter  Google Scholar 

  48. Xie, X., Chen, B., Liu, Y., Le, W., Li, X.: Proteus: computing disjunctive loop summary via path dependency analysis. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 61–72 (2016)

    Google Scholar 

Download references

Acknowledgments

This work was supported by the SECURVAL project. The SECUREVAL project was funded by the “France 2030” government investment plan managed by the French National Research Agency, under the reference ANR-22-PECY-0005.

Author information

Authors and Affiliations

  1. Sorbonne Université, CNRS, LIP6, 75005, Paris, France

    Marco Milanese & Antoine Miné

Authors
  1. Marco Milanese
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antoine Miné
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marco Milanese .

Editor information

Editors and Affiliations

  1. CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

    Rayna Dimitrova

  2. Tel Aviv University, Tel Aviv, Israel

    Ori Lahav

  3. New York University, New York, NY, USA

    Sebastian Wolff

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Milanese, M., Miné, A. (2024). Generation of Violation Witnesses by Under-Approximating Abstract Interpretation. In: Dimitrova, R., Lahav, O., Wolff, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2024. Lecture Notes in Computer Science, vol 14499. Springer, Cham. https://doi.org/10.1007/978-3-031-50524-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-50524-9_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-50523-2

  • Online ISBN: 978-3-031-50524-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation