accepted.txt

<h1>CADE-26 Accepted Papers</h1>

<style>.accepted {clear:right;margin-bottom:20pt;padding:3pt}</style><style>.abstract {border-left: solid black 1px;border-right: solid black 1px;border-top: solid black 1px;padding:3pt}</style><style>.paper {border-left: solid black 1px;border-right: solid black 1px;border-top: solid black 1px;padding:2pt}</style><style>.abstract:last-child {border-bottom: solid black 1px;padding:3pt}</style><style>.paper:last-child {border-bottom: solid black 1px;padding:2pt}</style><div class="paper"><span class="authors"><span><a href="https://www.mpi-sws.org/people/hbecker/">Heiko Becker</a>, <a href="http://people.mpi-inf.mpg.de/~jblanche/">Jasmin Christian Blanchette</a>, <a href="http://www.mpi-inf.mpg.de/departments/automation-of-logic/people/uwe-waldmann/">Uwe Waldmann</a> and Daniel Wand</span>. </span><span class="title">Transfinite Knuth-Bendix Orders for Lambda-Free Higher-Order Terms</span></div><div class="paper"><span class="authors"><span>Mnacho Echenim and Nicolas Peltier</span>. </span><span class="title">The binomial pricing model in finance: a formalization in Isabelle</span></div><div class="paper"><span class="authors"><span><a href="http://www.csc.liv.ac.uk/~ullrich">Ullrich Hustadt</a>, <a href="https://iccl.inf.tu-dresden.de/web/Ana_Ozaki/en">Ana Ozaki</a> and Clare Dixon</span>. </span><span class="title">Theorem Proving for Metric Temporal Logic over the Naturals</span></div><div class="paper"><span class="authors">Simon Cruanes. </span><span class="title">Satisfiability Modulo Bounded Checking</span></div><div class="paper"><span class="authors"><span><a href="https://members.loria.fr/HBarbosa/">Haniel Barbosa</a>, <a href="https://people.mpi-inf.mpg.de/~jblanche/">Jasmin Christian Blanchette</a> and <a href="https://members.loria.fr/PFontaine/">Pascal Fontaine</a></span>. </span><span class="title">An Efficient Proof-Producing Framework for Formula Processing</span></div><div class="paper"><span class="authors"><span>Yutaka Nagashima and <a href="http://ts.data61.csiro.au/people/?cn=Ramana+Kumar">Ramana Kumar</a></span>. </span><span class="title">A Proof Strategy Language and Proof Script Generation for Isabelle/HOL</span></div><div class="paper"><span class="authors"><span><a href="http://www.cs.ucl.ac.uk/staff/J.Brotherston/">James Brotherston</a>, <a href="http://ngorogiannis.bitbucket.io">Nikos Gorogiannis</a> and Max Kanovich</span>. </span><span class="title">Biabduction (and Related Problems) in Array Separation Logic</span></div><div class="paper"><span class="authors"><span><a href="http://www.cs.utexas.edu/~marijn">Marijn Heule</a>, <a href="http://www.kr.tuwien.ac.at/staff/kiesl/">Benjamin Kiesl</a> and <a href="http://fmv.jku.at/biere">Armin Biere</a></span>. </span><span class="title">Short Proofs without New Variables</span></div><div class="paper"><span class="authors"><span><a href="http://www.kr.tuwien.ac.at/staff/kiesl/">Benjamin Kiesl</a> and <a href="http://forsyte.at/people/suda/">Martin Suda</a></span>. </span><span class="title">A Unifying Principle for Clause Elimination in First-Order Logic</span></div><div class="paper"><span class="authors"><span><a href="http://cl-informatik.uibk.ac.at/users/csag8264/">Julian Nagele</a>, <a href="http://cl-informatik.uibk.ac.at/~bf3/">Bertram Felgenhauer</a> and <a href="http://cl-informatik.uibk.ac.at/~ami/">Aart Middeldorp</a></span>. </span><span class="title">CSI: New Evidence - A Progress Report</span></div><div class="paper"><span class="authors"><span><a href="http://tinyurl.com/lcfilipe">Luís Cruz-Filipe</a>, Marijn Heule, Warren Hunt, <a href="http://www.cs.utexas.edu/users/kaufmann/index.html">Matt Kaufmann</a> and <a href="http://www.imada.sdu.dk/~petersk/">Peter Schneider-Kamp</a></span>. </span><span class="title">Efficient Certified RAT Verification</span></div><div class="paper"><span class="authors"><span>Zhaowei Xu, <a href="http://www.eis.mdx.ac.uk/staffpages/taoluechen/">Taolue Chen</a> and <a href="http://lcs.ios.ac.cn/~wuzl">Zhilin Wu</a></span>. </span><span class="title">Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints</span></div><div class="paper"><span class="authors"><span><a href="http://www.kr.tuwien.ac.at/staff/lonsing/">Florian Lonsing</a> and <a href="http://www.kr.tuwien.ac.at/staff/egly/index.html">Uwe Egly</a></span>. </span><span class="title">DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL</span></div><div class="paper"><span class="authors"><span>Roberto Blanco, Zakaria Chihani and <a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller">Dale Miller</a></span>. </span><span class="title">Translating between implicit and explicit versions of proof</span></div><div class="paper"><span class="authors"><span>Serdar Erbatur, <a href="http://cs.umw.edu/~marshall/">Andrew M. Marshall</a> and <a href="http://www.loria.fr/~ringeiss/">Christophe Ringeissen</a></span>. </span><span class="title">Notions of Knowledge in Combinations of Theories Sharing Constructors</span></div><div class="paper"><span class="authors"><span><a href="http://www.fceia.unr.edu.ar/~mcristia">Maximiliano Cristia</a> and <a href="http://www.math.unipr.it/~gianfr">Gianfranco Rossi</a></span>. </span><span class="title">A Decision Procedure for Restricted Intensional Sets</span></div><div class="paper"><span class="authors"><span><a href="http://cl-informatik.uibk.ac.at/~griff/">Christian Sternagel</a> and <a href="http://cl-informatik.uibk.ac.at/tsternagel">Thomas Sternagel</a></span>. </span><span class="title">Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems</span></div><div class="paper"><span class="authors"><span>Petros Papapanagiotou and <a href="http://homepages.inf.ed.ac.uk/jdf">Jacques Fleuriot</a></span>. </span><span class="title">WorkflowFM: A logic-based formal verification framework for process specification and composition</span></div><div class="paper"><span class="authors">Peter Lammich. </span><span class="title">Efficient Verified (UN)SAT Certificate Checking</span></div><div class="paper"><span class="authors"><span>Andreas Teucke and <a href="http://www.mpi-inf.mpg.de/~weidenb/">Christoph Weidenbach</a></span>. </span><span class="title">Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints</span></div><div class="paper"><span class="authors"><span><a href="http://wwwlehre.dhbw-stuttgart.de/~sschulz/">Stephan Schulz</a>, <a href="http://www.cs.miami.edu/~geoff">Geoff Sutcliffe</a>, <a href="http://cs.ru.nl/~urban/">Josef Urban</a> and <a href="http://www.articulatesoftware.com">Adam Pease</a></span>. </span><span class="title">Detecting Inconsistencies in Large First-Order Knowledge Bases</span></div><div class="paper"><span class="authors"><span><a href="http://es.fbk.eu/people/cimatti/">Alessandro Cimatti</a>, <a href="http://es.fbk.eu/people/griggio/">Alberto Griggio</a>, Ahmed Irfan, <a href="http://es.fbk.eu/people/roveri">Marco Roveri</a> and <a href="http://disi.unitn.it/rseba/">Roberto Sebastiani</a></span>. </span><span class="title">Satisfiability Modulo Transcendental Functions via Incremental Linearization</span></div><div class="paper"><span class="authors"><span><a href="http://www.uibk.ac.at">Michael Färber</a>, <a href="http://cl-informatik.uibk.ac.at/cek/">Cezary Kaliszyk</a> and <a href="http://cs.ru.nl/~urban/">Josef Urban</a></span>. </span><span class="title">Monte Carlo Tableau Proof Search</span></div><div class="paper"><span class="authors"><span>Gadi Tellez and <a href="http://www.cs.ucl.ac.uk/staff/J.Brotherston/">James Brotherston</a></span>. </span><span class="title">Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof</span></div><div class="paper"><span class="authors"><span><a href="http://research.microsoft.com/en-us/people/mabrocks/">Marc Brockschmidt</a>, Sebastiaan Joosten, <a href="http://cl-informatik.uibk.ac.at/~thiemann/">René Thiemann</a> and <a href="http://cl-informatik.uibk.ac.at/users/ayamada/">Akihisa Yamada</a></span>. </span><span class="title">Certifying Safety and Termination Proofs for Integer Transition Systems</span></div><div class="paper"><span class="authors"><span><a href="http://paleo.woltzenlogel.org">Bruno Woltzenlogel Paleo</a>, <a href="http://users.rsise.anu.edu.au/~jks/">Daniyar Itegulov</a> and <a href="http://users.rsise.anu.edu.au/~jks/">John Slaney</a></span>. </span><span class="title">Scavenger 0.1: A Theorem Prover Based on Conflict Resolution</span></div><div class="paper"><span class="authors"><span><a href="http://people.mpi-inf.mpg.de/~mvoigt/">Marco Voigt</a>, <a href="http://people.mpi-inf.mpg.de/~weidenb/">Christoph Weidenbach</a> and <a href="http://people.mpi-inf.mpg.de/~horbach/">Matthias Horbach</a></span>. </span><span class="title">On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Linear Integer Arithmetic</span></div><div class="paper"><span class="authors"><span><a href="https://userpages.uni-koblenz.de/~mbender/">Markus Bender</a> and <a href="http://userpages.uni-koblenz.de/~sofronie/">Viorica Sofronie-Stokkermans</a></span>. </span><span class="title">Decision Procedures for Theories of Sets with Measures</span></div><div class="paper"><span class="authors"><span>Bernhard Gleiss, <a href="http://forsyte.at/people/kovacs/">Laura Kovacs</a> and <a href="http://forsyte.at/people/suda/">Martin Suda</a></span>. </span><span class="title">Splitting Proofs for Interpolation</span></div><div class="paper"><span class="authors"><span><a href="http://pmtruth.wixsite.com/baoluo-meng">Baoluo Meng</a>, <a href="http://homepage.cs.uiowa.edu/~ajreynol/">Andrew Reynolds</a>, <a href="http://www.cs.uiowa.edu/~tinelli/">Cesare Tinelli</a> and <a href="http://theory.stanford.edu/~barrett/">Clark Barrett</a></span>. </span><span class="title">Relational Constraint Solving in SMT</span></div><div class="paper"><span class="authors"><span><a href="http://profs.sci.univr.it/~bonacina/">Maria Paola Bonacina</a>, <a href="http://www.lix.polytechnique.fr/~lengrand/">Stéphane Graham-Lengrand</a> and <a href="http://www.csl.sri.com/people/shankar/">Natarajan Shankar</a></span>. </span><span class="title">Satisfiability Modulo Theories and Assignments</span></div>