Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2019: Automated Deduction – CADE 27 pp 385–405Cite as

On Invariant Synthesis for Parametric Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11716))

Abstract

We study possibilities for automated invariant generation in parametric systems. We use (a refinement of) an algorithm for symbol elimination in theory extensions to devise a method for iteratively strengthening certain classes of safety properties to obtain invariants of the system. We identify conditions under which the method is correct and complete, and situations in which the method is guaranteed to terminate. We illustrate the ideas on various examples.

This is a preview of subscription content, 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   69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   89.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

Learn about institutional subscriptions

Notes

  1. 1.

    We use the following abbreviations: \({\overline{x}}\) for \(x_1, \dots , x_n\); \({\overline{f}}({\overline{x}})\) for \(f_1({\overline{x}}), \dots , f_n({\overline{x}})\).

  2. 2.

    \(\varPi ^C\) is the extension of \(\varPi \) with constants in a countable set C of fresh constants.

  3. 3.

    We here regard every finite set G of ground clauses as the ground formula \(\bigwedge _{K \in G} K\).

  4. 4.

    We use the index f in \((\mathsf{Comp}_{f})\) in order to emphasize that the property refers to completability of partial functions with a finite domain of definition.

  5. 5.

    Variables are 0-ary functions. Ground formulae are, in particular, also universal formulae.

  6. 6.

    In particular we can consider definition updates of the form \(\mathsf{D}_{f'}\) or updates of the form \(\mathsf{Bound}_{f'}\) as discussed in Example 2.

  7. 7.

    To simplify the notation, we assume that the functions in \(\varSigma \) have arity \(\le 1\). Similar arguments can be used for n-ary functions.

References

  1. Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014)

    Article  Google Scholar 

  2. Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)

    Article  MathSciNet  Google Scholar 

  3. Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69738-1_27

    Chapter  Google Scholar 

  4. Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 4–4. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_4

    Chapter  Google Scholar 

  5. Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20(4–5), 379–405 (2008)

    Article  Google Scholar 

  6. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_28

    Chapter  Google Scholar 

  7. Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1), 5:1–5:34 (2014)

    Article  MathSciNet  Google Scholar 

  8. Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_55

    Chapter  Google Scholar 

  9. Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Hosking, A.L., Eugster, P.T., Lopes, C.V., (eds.) Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, pp. 443–456. ACM (2013)

    Google Scholar 

  10. Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2–9 (1997)

    Article  Google Scholar 

  11. Faber, J., Jacobs, S., Sofronie-Stokkermans, V.: Verifying CSP-OZ-DC specifications with complex data types and timing parameters. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 233–252. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73210-5_13

    Chapter  Google Scholar 

  12. Falke, S., Kapur, D.: When is a formula a loop invariant? In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 264–286. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23165-5_13

    Chapter  Google Scholar 

  13. Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with weak equality. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 168–182. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25984-8_10

    Chapter  Google Scholar 

  14. Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 204(10), 1453–1492 (2006)

    Article  MathSciNet  Google Scholar 

  15. Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods Comput. Sci. 6(4), 1–48 (2010)

    Article  MathSciNet  Google Scholar 

  16. Gleiss, B., Kovács, L., Robillard, S.: Loop analysis by quantification over iterations. In: Barthe, G., Sutcliffe, G., Veanes, M., (eds.) 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, LPAR-22, pp. 381–399 (2018). EasyChair

    Google Scholar 

  17. Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 248–266. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_15

    Chapter  Google Scholar 

  18. Hoder, K., Kovács, L., Voronkov, A.: Interpolation and symbol elimination in Vampire. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 188–195. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_16

    Chapter  Google Scholar 

  19. Horbach, M., Sofronie-Stokkermans, V.: Obtaining finite local theory axiomatizations via saturation. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 198–213. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40885-4_14

    Chapter  Google Scholar 

  20. Horbach, M., Sofronie-Stokkermans, V.: Locality transfer: From constrained axiomatizations to reachability predicates. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 192–207. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_14

    Chapter  Google Scholar 

  21. Horbach, M., Weidenbach, C.: Deciding the inductive validity of \(\forall \exists \)* queries. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 332–347. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04027-6_25

    Chapter  Google Scholar 

  22. Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265–281. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_19

    Chapter  Google Scholar 

  23. Ihlemann, C., Sofronie-Stokkermans, V.: System description: H-PILoT. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 131–139. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_9

    Chapter  Google Scholar 

  24. Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 30–45. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_4

    Chapter  MATH  Google Scholar 

  25. Jacobs, S., Kuncak, V.: Towards complete reasoning about axiomatic specifications. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 278–293. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_20

    Chapter  Google Scholar 

  26. Kapur, D.: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs. J. Syst. Sci. Complexity 19(3), 307–330 (2006)

    Article  MathSciNet  Google Scholar 

  27. Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Young, M., Devanbu, P.T., (eds.) Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, pp. 105–116. ACM (2006)

    Google Scholar 

  28. Karbyshev, A., Bjørner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1), 7:1–7:33 (2017)

    Article  MathSciNet  Google Scholar 

  29. Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–485. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00593-0_33

    Chapter  Google Scholar 

  30. Kovács, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 199–213. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_17

    Chapter  Google Scholar 

  31. Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Bodík, R., Majumdar, R., (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 217–231. ACM (2016)

    Google Scholar 

  32. Peuter, D., Sofronie-Stokkermans, V.: On invariant synthesis for parametric systems. CoRR http://arxiv.org/abs/1905.12524 (2019)

  33. Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_16

    Chapter  Google Scholar 

  34. Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 235–250. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_21

    Chapter  Google Scholar 

  35. Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods Comput. Sci. 4(4), 1–31 (2008)

    Article  MathSciNet  Google Scholar 

  36. Sofronie-Stokkermans, V.: Hierarchical reasoning for the verification of parametric systems. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 171–187. Springer, Berlin (2010). https://doi.org/10.1007/978-3-642-14203-1_15

    Chapter  MATH  Google Scholar 

  37. Sofronie-Stokkermans, V.: Hierarchical reasoning and model generation for the verification of parametric hybrid systems. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 360–376. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_25

    Chapter  Google Scholar 

  38. Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 273–289. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_19

    Chapter  Google Scholar 

  39. Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Logical Methods Comput. Sci. 14(3), 1–41 (2018)

    MathSciNet  MATH  Google Scholar 

  40. Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_26

    Chapter  Google Scholar 

Download references

Acknowledgments

We thank the reviewers for their helpful comments.

Author information

Authors and Affiliations

  1. Universität Koblenz-Landau, Koblenz, Germany

    Dennis Peuter & Viorica Sofronie-Stokkermans

Authors
  1. Dennis Peuter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viorica Sofronie-Stokkermans
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Viorica Sofronie-Stokkermans .

Editor information

Editors and Affiliations

  1. University of Lorraine, Villers-lès-Nancy, France

    Pascal Fontaine

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Peuter, D., Sofronie-Stokkermans, V. (2019). On Invariant Synthesis for Parametric Systems. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29436-6_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29435-9

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation