96
T. Okudono and A. King
17. Griggio, A., Le, T.T.H., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. Logical Methods in Computer Science
8(3) (2010)
18. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Principles of Programming Languages. pp. 58–70 (2002)
19. Jain, H., Clarke, E.M., Grumberg, O.: Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods in System
Design 35(1), 6–39 (2009)
20. Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for Data Structures. In:
Foundations of Software Engineering. pp. 105–116 (2006)
21. Karr, M.: Affine Relationships among Variables of a Program. Acta Informatica 6,
133–151 (1976)
22. King, A., Søndergaard, H.: Automatic Abstraction for Congruences. In: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer
Science, vol. 9583, pp. 197–213. Springer (2010)
23. Kroening, D., Weissenbacher, G.: Lifting Propositional Interpolants to the WordLevel. In: Formal Methods in Computer-Aided Design. pp. 85–89. IEEE (2007)
24. McMillan, K.: An Interpolating Theorem Prover. Theoretical Computer Science
345(1), 101–121 (2005)
25. McMillan, K.L.: Lazy Abstraction with Interpolants. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 4144, pp. 123–136. Springer (2006)
26. McMillan, K.L.: Interpolation and Model Checking. In: Handbook of Model Checking. pp. 421–446. Springer (2018)
27. M¨ oller, M., Rue, H.: Solving Bit-Vector Equations. In: Formal Methods in
Computer-Aided Design. Lecture Notes in Computer Science, vol. 1522, pp. 36–48
(1998)
28. M¨ uller-Olm, M., Seidl, H.: Analysis of Modular Arithmetic. ACM Transactions on
Programming Languages and Systems 29(5), 29 (2007)
29. Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The Small Model Property: How
small can it be? Information and Computation 178(1), 279–293 (2002)
30. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation.
Journal of Symbolic Computation 45(11), 1212–1233 (2010)
31. Services, A.W.: Amazon EC2 FAQs (2019), https://aws.amazon.com/ec2/faqs/
32. Simon, A., King, A.: Taming the Wrapping of Integer Arithmetic. In: Static Analysis Symposium. Lecture Notes in Computer Science, vol. 4634, pp. 121–136.
Springer (2007)
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.
T. Okudono and A. King
17. Griggio, A., Le, T.T.H., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. Logical Methods in Computer Science
8(3) (2010)
18. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Principles of Programming Languages. pp. 58–70 (2002)
19. Jain, H., Clarke, E.M., Grumberg, O.: Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods in System
Design 35(1), 6–39 (2009)
20. Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for Data Structures. In:
Foundations of Software Engineering. pp. 105–116 (2006)
21. Karr, M.: Affine Relationships among Variables of a Program. Acta Informatica 6,
133–151 (1976)
22. King, A., Søndergaard, H.: Automatic Abstraction for Congruences. In: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer
Science, vol. 9583, pp. 197–213. Springer (2010)
23. Kroening, D., Weissenbacher, G.: Lifting Propositional Interpolants to the WordLevel. In: Formal Methods in Computer-Aided Design. pp. 85–89. IEEE (2007)
24. McMillan, K.: An Interpolating Theorem Prover. Theoretical Computer Science
345(1), 101–121 (2005)
25. McMillan, K.L.: Lazy Abstraction with Interpolants. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 4144, pp. 123–136. Springer (2006)
26. McMillan, K.L.: Interpolation and Model Checking. In: Handbook of Model Checking. pp. 421–446. Springer (2018)
27. M¨ oller, M., Rue, H.: Solving Bit-Vector Equations. In: Formal Methods in
Computer-Aided Design. Lecture Notes in Computer Science, vol. 1522, pp. 36–48
(1998)
28. M¨ uller-Olm, M., Seidl, H.: Analysis of Modular Arithmetic. ACM Transactions on
Programming Languages and Systems 29(5), 29 (2007)
29. Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The Small Model Property: How
small can it be? Information and Computation 178(1), 279–293 (2002)
30. Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation.
Journal of Symbolic Computation 45(11), 1212–1233 (2010)
31. Services, A.W.: Amazon EC2 FAQs (2019), https://aws.amazon.com/ec2/faqs/
32. Simon, A., King, A.: Taming the Wrapping of Integer Arithmetic. In: Static Analysis Symposium. Lecture Notes in Computer Science, vol. 4634, pp. 121–136.
Springer (2007)
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.