Advertisement

Journal of Automated Reasoning

, Volume 57, Issue 1, pp 1–2 | Cite as

Preface: Special Issue on Interpolation

  • Daniel Kroening
  • Andrey Rybalchenko
Article
  • 126 Downloads

Keywords

Proof Tree Linear Arithmetic Extension Axiom Loop Invariant Resolution Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Craig, W.: Linear reasoning. A new form of the Herbrand–Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)MathSciNetCrossRefMATHGoogle Scholar
  2. 2.
    McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005)MathSciNetCrossRefMATHGoogle Scholar
  3. 3.
    Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) Computer Aided Verification, vol. 5123 of LNCS, pp. 304–308. Springer, Heidelberg (2008)Google Scholar
  4. 4.
    Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Proceedings of VMCAI, volume 4349 of LNCS, pp. 346–362. Springer (2007)Google Scholar
  5. 5.
    Lynch, C., Tang, Y.: Interpolants for linear arithmetic in SMT. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) Automated Technology for Verification and Analysis, vol. 5311, pp. 156–170. Springer, Heidelberg (2008)Google Scholar
  6. 6.
    Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Proceedings of International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of LNCS, pp. 384–399. Springer (2010)Google Scholar
  7. 7.
    Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. J. Autom. Reason. 47(4), 341–367 (2011)MathSciNetCrossRefMATHGoogle Scholar
  8. 8.
    Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: SIGSOFT ’06/FSE-14, pp. 105–116. ACM (2006)Google Scholar
  9. 9.
    D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M.V. (eds.) Verification, Model Checking, and Abstract Interpretation, 11th International Conference (VMCAI). Lecture Notes in Computer Science, vol. 5944, pp. 129–145. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2016

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of OxfordOxfordUK
  2. 2.Microsoft Research CambridgeCambridgeUK

Personalised recommendations