pubs.html

---
title: Publications
layout: default
---
{% include authors.html %}

<p>
This is a list of publications related to Vampire.
<em>This list is out of date, at the moment please refer to the team's personal or DBLP pages for related papers.</em>
Both <a href="http://www.cse.chalmers.se/~laurako/">Laura</a> and <a href="http://www.cs.man.ac.uk/~regerg/publications.html">Giles</a> maintain preprints on their personal pages.
</p>

<ol class="pubs">
<li class="year">
<h2>2017</h2>

<li class="paper">
 <ul class="authors">
  <li>{{ reger }}
  <li>{{ suda }}
 </ul>
 <cite>Set of Support for Theory Reasoning</cite>
 IWIL@LPAR 2017
<li class="paper">
 <ul class="authors">
  <li>{{ kovacs }}
  <li>{{ voronkov }}
 </ul>
 <cite>First-Order Interpolation and Interpolating Proof Systems</cite>
 LPAR 2017
<li class="paper">
 <ul class="authors">
  <li>{{ kovacs }}
  <li>{{ robillard }}
  <li>{{ voronkov }}
 </ul>
 <cite>Coming to terms with quantified reasoning</cite>
 POPL 2017
<li class="paper">
 <ul class="authors">
  <li>{{ kiesel }}
  <li>{{ suda }}
 </ul>
 <cite>A Unifying Principle for Clause Elimination in First-Order Logic</cite>
 CADE 2017
<li class="paper">
 <ul class="authors">
  <li>{{ gleiss }}
  <li>{{ kovacs }}
  <li>{{ suda }}
 </ul>
 <cite>Splitting Proofs for Interpolation</cite>
 CADE 2017 
<li class="paper">
 <ul class="authors">
  <li>{{ reger }}
  <li>{{ suda }}
  <li>{{ voronkov }}
 </ul>
 <cite>Testing a Saturation-Based Theorem Prover: Experiences and Challenges</cite>
 TAP 2017

<li class="year">
<h2>2016</h2>
(Currently Missing)

<li class="year">
<h2>2015</h2>
(Currently Missing)

<li class="year">
<h2>2014</h2>
(Currently Missing)

<li class="year">
<h2>2013</h2>
<li class="paper">
 <ul class="authors">
  <li>{{ kovacs }}
  <li>{{ voronkov }}
 </ul>
 <cite>First-Order Theorem Proving and Vampire</cite>
 <a href="http://cav2013.forsyte.at/index">CAV 2013</a>
<li class="paper">
 <ul class="authors">
  <li>{{ hoder }}
  <li>{{ voronkov }}
 </ul>
 <cite><a href="http://dx.doi.org/10.1007/978-3-642-38574-2_33">The 481 Ways to Split a Clause and Deal with Propositional Variables</a></cite>
 <a href="http://www.informatik.uni-trier.de/~ley/db/conf/cade/cade2013">CADE 2013</a>

<li class="year">
<h2>2012</h2>
<li class="paper">
 <ul class="authors">
  <li>{{ hoder }}
  <li>{{ kovacs }}
  <li>{{ voronkov }}
 </ul>
 <cite><a href="htp://doi.acm.org/10.1145/2103656.2103689">Playing in the grey area of proofs</a></cite>
 <a href="http://www.informatik.uni-trier.de/~ley/db/conf/popl/popl2012">POPL 2012</a>
<li class="paper">
 <ul class="authors">
  <li>{{ hoder }}
  <li>{{ holzer }}
  <li>{{ kovacs }}
  <li>{{ voronkov }}
 </ul>
 <cite><a href="http://dx.doi.org/10.1007/978-3-642-35182-2_11">Vinter: A Vampire-Based Tool for Interpolation</a></cite>
 <a href="http://www.informatik.uni-trier.de/~ley/db/conf/aplas/aplas2012">APLAS 2012</a>
<li class="paper">
 <ul class="authors">
  <li>{{ hoder }}
  <li>{{ khasidashvili }}
  <li>{{ korovin }}
  <li>{{ voronkov }}
 </ul>
 <cite><a href="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462554">Preprocessing techniques for first-order clausification</a></cite>
 <a href="http://www.informatik.uni-trier.de/~ley/db/conf/fmcad/fmcad2012">FMCAD 2012</a>

<li class="year">
<h2>2011</h2>
<li class="paper">
 <ul class="authors">
  <li>{{ hoder }}
  <li>{{ voronkov }}
 </ul>
 <cite><a href="http://dx.doi.org/10.1007/978-3-642-22438-6_23">Sine Qua Non for Large Theory Reasoning</a></cite>
 <a href="http://www.informatik.uni-trier.de/~%20ley/db/conf/cade/cade2011">CADE 2011</a>
<li class="paper">
 <ul class="authors">
  <li>{{ hoder }}
  <li>{{ kovacs }}
  <li>{{ voronkov }}
 </ul>
 <cite><a href="http://dx.doi.org/10.1007/978-3-642-25324-9_1">Case Studies on Invariant Generation Using a Saturation Theorem Prover</a></cite>
 <a href="http://www.informatik.uni-trier.de/~ley/db/conf/micai/micai2011-1">MICAI 2011</a>
<li class="paper">
 <ul class="authors">
  <li>{{ hoder }}
  <li>{{ kovacs }}
  <li>{{ voronkov }}
 </ul>
 <cite><a href="http://dx.doi.org/10.1007/978-3-642-19835-9_7">Invariant Generation in Vampire</a></cite>
 <a href="http://www.informatik.uni-trier.de/~ley/db/conf/tacas/tacas2011">TACAS 2011</a>

<li class="year">
<h2>Before 2011</h2>
(Currently Missing)

</ol>