logo Région Lorraine

Publications

last update: 26.10.2016

  1. Thomas Sturm, Marco Voigt, and Christoph Weidenbach. Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. In Symposium on Logic in Computer Science (LICS), pages 86-95. IEEE Computer Society, 2016. [ http ]

  2. Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm. SC^2: Satisfiability checking meets symbolic computation - (project paper). In Michael Kohlhase, Moa Johansson, Bruce R. Miller, Leonardo de de Moura, and Frank Wm. Tompa, editors, Intelligent Computer Mathematics (CICM), volume 9791 of Lecture Notes in Computer Science, pages 28-43. Springer, 2016. [ pdf ]

  3. Marek Kosta, Thomas Sturm, and Andreas Dolzmann. Better answers to real questions. J. Symb. Comput., 74:255-275, 2016.

  4. Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A polite non-disjoint combination method: Theories with bridging functions revisited. In Amy P. Felty and Aart Middeldorp, editors, Proc. Conference on Automated Deduction (CADE), volume 9195 of Lecture Notes in Computer Science, pages 419-433. Springer, 2015. [ pdf ]

  5. Maximilian Jaroschek, Pablo Federico Dobal, and Pascal Fontaine. Adapting real quantifier elimination methods for conflict set computation. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems (FroCoS), volume 9322 of Lecture Notes in Computer Science, pages 151-166. Springer, 2015. [ pdf ]

  6. Richard Bonichon, David Déharbe, Pablo Federico Dobal, and Cláudia Tavares. SMTpp: preprocessors and analyzers for SMT-LIB. In Vijay Ganesh and Dejan Jovanović, editors, International Workshop on Satisfiability Modulo Theories (SMT), 2015. [ pdf ]

  7. Andreas Fellner, Pascal Fontaine, Georg Hofferek, and Bruno Woltzenlogel Paleo. Np-completeness of small conflict set generation for congruence closure. In Vijay Ganesh and Dejan Jovanović, editors, International Workshop on Satisfiability Modulo Theories (SMT), 2015. [ pdf ]

  8. Carlos Areces, Pascal Fontaine, and Stephan Merz. Modal satisfiability via SMT solving. In Rocco De Nicola and Rolf Hennicker, editors, Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, volume 8950 of Lecture Notes in Computer Science, pages 30-45. Springer, 2015. [ pdf ]

  9. Martin Bromberger, Thomas Sturm, and Christoph Weidenbach. Linear integer arithmetic revisited. In Amy P. Felty and Aart Middeldorp, editors, Proc. Conference on Automated Deduction (CADE), volume 9195 of Lecture Notes in Computer Science, pages 623-637. Springer, 2015. [ http ]

  10. Stephan Merz and Hernán Vanzetto. Encoding TLA+ set theory into many-sorted first-order logic. In Workshop SETS, 2015. CoRR abs/1508.03838. [ pdf ]

  11. Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A rewriting approach to the combination of data structures with bridging theories. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pages 275-290. Springer, 2015. [ pdf ]

  12. Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber. Detection of hopf bifurcations in chemical reaction networks using convex coordinates. J. Comput. Physics, 291:279-302, 2015. [ http ]

  13. Marek Kosta and Thomas Sturm. A generalized framework for virtual substitution. CoRR, abs/1501.05826, 2015. [ http ]

  14. Marek Kosta, Thomas Sturm, and Andreas Dolzmann. Better answers to real questions. CoRR, abs/1501.05098, 2015. Extended version accepted at Journal of Symbolic Computation, 2015. [ http ]

  15. Thomas Sturm. Subtropical real root finding. In Kazuhiro Yokoyama, Steve Linton, and Daniel Robertz, editors, International Symposium on Symbolic and Algebraic Computation (ISSAC), pages 347-354. ACM, 2015. [ http ]

  16. Marek Kosta, Thomas Sturm, and Andreas Dolzmann. Better answers to real questions. In Philipp Rümmer and Christoph M. Wintersteiger, editors, International Workshop on Satisfiability Modulo Theories (SMT), volume 1163 of CEUR Workshop Proceedings, page 69. CEUR-WS.org, 2014. [ pdf ]

  17. Stephan Merz and Hernán Vanzetto. Refinement types for TLA+. In Julia M. Badger and Kristin Yvonne Rozier, editors, NASA Formal Methods (NFM), volume 8430 of Lecture Notes in Computer Science, pages 143-157. Springer, 2014. [ http ]

  18. Konstantin Korovin, Marek Kosta, and Thomas Sturm. Towards conflict-driven learning for virtual substitution. In Vladimir P. Gerdt, Wolfram Koepf, Werner M. Seiler, and Evgenii V. Vorozhtsov, editors, Computer Algebra in Scientific Computing (CASC), volume 8660 of Lecture Notes in Computer Science, pages 256-270. Springer, 2014. [ http ]

  19. Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A gentle non-disjoint combination of satisfiability procedures. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, International Joint Conference on Automated Reasoning (IJCAR), volume 8562 of Lecture Notes in Computer Science, pages 122-136. Springer, 2014. [ pdf ]

  20. David Déharbe, Pascal Fontaine, Yoann Guyot, and Laurent Voisin. Integrating SMT solvers in Rodin. Science of Computer Programming, 94:130-143, 2014. [ pdf ]

  21. Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. Satisfiability modulo non-disjoint combinations of theories connected via bridging functions. In Silvio Ghilardi, Ulrike Sattler, and Viorica Sofronie-Stokkermans, editors, Automated Deduction: Decidability, Complexity, Tractability (ADDCT), 2014. [ pdf ]

  22. Clark Barrett, Leonardo de Moura, and Pascal Fontaine. Proofs in satisfiability modulo theories. In All about Proofs, Proofs for All (APPA), 2014. [ pdf ]


This file was generated by bibtex2html 1.97.