SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. The solver is developed at the Chair of Software Engineering at the University of Freiburg. The solver is written in Java and can be used on any operating system that supports Java Version 6. The solver reads input in SMTLIB Version 2 format.

References in zbMATH (referenced in 22 articles )

Showing results 1 to 20 of 22.
Sorted by year (citations)

1 2 next

  1. Devillers, Raymond: Articulations and products of transition systems and their applications to Petri net synthesis (2021)
  2. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  3. Hajdu, Ákos; Micskei, Zoltán: Efficient strategies for CEGAR-based model checking (2020)
  4. Dietsch, Daniel; Heizmann, Matthias; Hoenicke, Jochen; Nutz, Alexander; Podelski, Andreas: Ultimate TreeAutomizer (CHC-COMP tool description) (2019)
  5. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  6. Best, Eike; Devillers, Raymond; Schlachter, Uli: Bounded choice-free Petri net synthesis: algorithmic issues (2018)
  7. Bromberger, Martin: A reduction from unbounded linear mixed arithmetic problems into bounded problems (2018)
  8. Hoenicke, Jochen; Schindler, Tanja: Efficient interpolation for the theory of arrays (2018)
  9. Lvov, M.; Peschanenko, V.; Letychevskyi, O.; Tarasich, Y.; Baiev, A.: Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (2018)
  10. Niewiadomski, Artur; Switalski, Piotr; Sidoruk, Teofil; Penczek, Wojciech: SMT-solvers in action: encoding and solving selected problems in NP and EXPTIME (2018)
  11. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \textsfAProVE (2017)
  12. Greitschus, Marius; Dietsch, Daniel; Podelski, Andreas: Loop invariants from counterexamples (2017)
  13. Ábrahám, Erika; Kremer, Gereon: Satisfiability checking: theory and applications (2016)
  14. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  15. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  16. Koskinen, Eric; Yang, Junfeng: Reducing crash recoverability to reachability (2016)
  17. Christ, Jürgen; Hoenicke, Jochen: Weakly equivalent arrays (2015)
  18. Christ, Jürgen; Hoenicke, Jochen: Cutting the mix (2015)
  19. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  20. Christ, Jürgen; Ermis, Evren; Schäf, Martin; Wies, Thomas: Flow-sensitive fault localization (2013) ioport

1 2 next