IJCAR 2016 Accepted Papers

Lars Hupel and Viktor Kuncak. Translating Scala Programs to Isabelle/HOL
Jasmin Christian Blanchette, Mathias Fleury and Christoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes and Cesare Tinelli. Model Finding for Recursive Functions in SMT
Joseph Boudou. Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition
Yoni Zohar and Anna Zamansky. Gen2sat: an Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi
David Cerna and Alexander Leitsch. Schematic Cut elimination and the Ordered Pigeonhole Principle
Francesco Alberti, Silvio Ghilardi and Elena Pagani. Counting Constraints in Flat Array Fragments
Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai and Noriko Arai. Race against the Teens -- Benchmarking Mechanized Math on Pre-university Problems
Benjamin Aminof and Sasha Rubin. Model Checking Parameterised Multi-Token Systems via the Composition Method
Vu Xuan Tung, To Van Khanh and Mizuhito Ogawa. raSAT : SMT Solver for Polynomial Constraints
Leonardo de Moura and Daniel Selsam. Congruence Closure in Intensional Type Theory
Taolue Chen, Xincai Gu and Zhilin Wu. A complete decision procedure for linearly compositional separation logic with data constraints
Giles Reger, Martin Suda, Andrei Voronkov and Krystof Hoder. Selecting the Selection
Jeremy Dawson, James Brotherston and Rajeev Gore. Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi
Michael Färber and Chad Brown. Internal guidance for Satallax
Cláudia Nalon, Ullrich Hustadt and Clare Dixon. KSP: A resolution-based prover for multimodal K
Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner and Sebastian Zivota. System Description: GAPT 2.0
Benjamin Kiesl, Martina Seidl, Hans Tompits and Armin Biere. Super-Blocked Clauses
Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur and Mingshuai Chen. Interpolation synthesis for quadratic polynomial inequalities and combination with EUF
Martin Bromberger and Christoph Weidenbach. Fast Cube Tests for LIA Constraint Solving
Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt and Jürgen Giesl. Lower Runtime Bounds for Integer Programs
Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron and Pietro Sala. Interval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments
Stephan Schulz and Martin Möhrmann. Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
Simon Docherty and David Pym. Intuitionistic layered graph logic
Revantha Ramanayake. Inducing syntactic cut-elimination for indexed nested sequents
Hans De Nivelle. Subsumption Algorithms for Three-Valued Geometric Resolution
Francisco Durán, Steven Eker, Santiago Escobar, Narciso Marti-Oliet, Jose Meseguer and Carolyn Talcott. Built-in Variant Generation and Unification, and their Applications in Maude 2.7 (System Description)
Konstantinos Athanasiou, Peizun Liu and Thomas Wahl. Unbounded-Thread Program Verification using Thread-State Equations
Kshitij Bansal, Clark Barrett, Andrew Reynolds and Cesare Tinelli. A new decision procedure for finite sets and cardinality in SMT
Max Wisniewski, Alexander Steen, Kim Kern and Christoph Benzmüller. Effective Normalization Techniques for HOL
Diana Costa and Manuel A. Martins. A Tableau System for Quasi-Hybrid Logic
Viorica Sofronie-Stokkermans. On Interpolation and Symbol Elimination in Theory Extensions
Takahito Aoto and Kentaro Kikuchi. Nominal Confluence Tool
Jens Otten. NanoCoP: A Non-clausal Connection Prover
Roberto Sebastiani. Colors Make Theories Hard