International Joint Conference on Automated Reasoning

List of 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