Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
95
References
1. Albarghouthi, A., McMillan, K.L.: Beautiful Interpolants. In: Computer Aided
Verification. Lecture Notes in Computer Science, vol. 8044, pp. 313–329. Springer
(2013)
2. Backeman, P., R¨ ummer, P., Zeljic, A.: Bit-Vector Interpolation and Quantifier
Elimination by Lazy Reduction. In: Formal Methods in Computer Aided Design.
pp. 1–10. IEEE (2018)
3. Barrett, C., Dill, D., Levitt, J.: A Decision Procedure for Bit-Vector Arithmetic.
In: Design and Automation Conference. pp. 522–527 (1998)
4. Besson, F., Cornilleau, P.E., Jensen, T.: Result Certification of Static Program
Analysers with Automated Theorem Provers. In: Verified Software: Theories,
Tools, Experiments. Lecture Notes in Computer Science, vol. 8164, pp. 304–325.
Springer (2014)
5. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker
BLAST. International Journal on Software Tools for Technology Transfer 9(5-6),
505–525 (2007)
6. Beyer, D., Wendler, P.: Algorithms for software model checking: Predicate abstraction vs. Impact. In: Formal Methods in Computer-Aided Design. pp. 106–113. IEEE
(2012)
7. Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.:
Deciding Bit-Vector Arithmetic with Abstraction. In: Tools and Algorithms for
the Construction and Analysis of Systems. Lecture Notes in Computer Science,
vol. 4424, pp. 358–372. Springer (2007)
8. Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos – a Software Model Checker for SystemC. In: Computer Aided Verification. Lecture Notes
in Computer Science, vol. 6808, pp. 123–136. Springer (2011)
9. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT
Solver. In: Tools and Algorithms for the Construction and Analysis of Systems.
Lecture Notes in Computer Science, vol. 7795, pp. 93–107. Springer (2013)
10. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Tools and Algorithms for the Construction and
Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 397–412.
Springer (2008)
11. Cimatti, A., Griggio, A., Sebastiani, R.: Interpolant Generation for UTVPI. In:
CADE. pp. 167–182 (2009)
12. Demyanova, Y., R¨ ummer, P., Zuleger, F.: Systematic Predicate Abstraction Using
Variable Roles. In: NASA Formal Methods. Lecture Notes in Computer Science,
vol. 10227, pp. 265–281. Springer (2017)
13. Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.: Abstract Domains of Affine
Relations. ACM Transactions on Programming Languages and Systems 36 (2014)
14. Fouilh´ e, A., Monniaux, D., P´ erin, M.: Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. In: Static Analysis Symposium.
Lecture Notes in Computer Science, vol. 7935, pp. 345–365. Springer (2013)
15. Graf, S., Sa¨ ıdi, H.: Construction of Abstract State Graphs with PVS. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254, pp. 72–83.
Springer (1997)
16. Griggio, A.: Effective Word-Level Interpolation for Software Verification. In: Formal Methods in Computer-Aided Design. pp. 28–36. IEEE (2011)
95
References
1. Albarghouthi, A., McMillan, K.L.: Beautiful Interpolants. In: Computer Aided
Verification. Lecture Notes in Computer Science, vol. 8044, pp. 313–329. Springer
(2013)
2. Backeman, P., R¨ ummer, P., Zeljic, A.: Bit-Vector Interpolation and Quantifier
Elimination by Lazy Reduction. In: Formal Methods in Computer Aided Design.
pp. 1–10. IEEE (2018)
3. Barrett, C., Dill, D., Levitt, J.: A Decision Procedure for Bit-Vector Arithmetic.
In: Design and Automation Conference. pp. 522–527 (1998)
4. Besson, F., Cornilleau, P.E., Jensen, T.: Result Certification of Static Program
Analysers with Automated Theorem Provers. In: Verified Software: Theories,
Tools, Experiments. Lecture Notes in Computer Science, vol. 8164, pp. 304–325.
Springer (2014)
5. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker
BLAST. International Journal on Software Tools for Technology Transfer 9(5-6),
505–525 (2007)
6. Beyer, D., Wendler, P.: Algorithms for software model checking: Predicate abstraction vs. Impact. In: Formal Methods in Computer-Aided Design. pp. 106–113. IEEE
(2012)
7. Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.:
Deciding Bit-Vector Arithmetic with Abstraction. In: Tools and Algorithms for
the Construction and Analysis of Systems. Lecture Notes in Computer Science,
vol. 4424, pp. 358–372. Springer (2007)
8. Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos – a Software Model Checker for SystemC. In: Computer Aided Verification. Lecture Notes
in Computer Science, vol. 6808, pp. 123–136. Springer (2011)
9. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT
Solver. In: Tools and Algorithms for the Construction and Analysis of Systems.
Lecture Notes in Computer Science, vol. 7795, pp. 93–107. Springer (2013)
10. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Tools and Algorithms for the Construction and
Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 397–412.
Springer (2008)
11. Cimatti, A., Griggio, A., Sebastiani, R.: Interpolant Generation for UTVPI. In:
CADE. pp. 167–182 (2009)
12. Demyanova, Y., R¨ ummer, P., Zuleger, F.: Systematic Predicate Abstraction Using
Variable Roles. In: NASA Formal Methods. Lecture Notes in Computer Science,
vol. 10227, pp. 265–281. Springer (2017)
13. Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.: Abstract Domains of Affine
Relations. ACM Transactions on Programming Languages and Systems 36 (2014)
14. Fouilh´ e, A., Monniaux, D., P´ erin, M.: Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. In: Static Analysis Symposium.
Lecture Notes in Computer Science, vol. 7935, pp. 345–365. Springer (2013)
15. Graf, S., Sa¨ ıdi, H.: Construction of Abstract State Graphs with PVS. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254, pp. 72–83.
Springer (1997)
16. Griggio, A.: Effective Word-Level Interpolation for Software Verification. In: Formal Methods in Computer-Aided Design. pp. 28–36. IEEE (2011)