The list of accepted papers is also available with abstracts. Slides for the talks are linked at the bottom of this page.
- Krzysztof Apt and Dominik Wojtczak. Decidability of Fair Termination of Gossip Protocols (details)
- Matthias Baaz and Norbert Preining. Gödel logics and the fully boxed fragment of LTL (details)
- Gilles Barthe, Thomas Espitau, Benjamin Gregoire, Justin Hsu and Pierre-Yves Strub. Proving uniformity and independence by self-composition and coupling (details)
- Sabine Bauer and Martin Hofmann. Decidable linear list constraints (details)
- Stefano Bistarelli, Fabio Martinelli, Ilaria Matteucci and Francesco Santini. A Quantitative Partial Model-Checking Function and Its Optimisation (details)
- František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmir Kretinsky and Jan Strejcek. Seminator: A Tool for Semi-Determinization of Omega-Automata (details)
- Bart Bogaerts, Evgenia Ternovska and David Mitchell. Propagators and Solvers for the Algebra of Modular Systems (details)
- Yazid Boumarafi, Lakhdar Sais and Yakoub Salhi. From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes (details)
- Agata Ciabattoni and Revantha Ramanayake. Bunched Hypersequent Calculi for Distributive Substructural Logics (details)
- Luís Cruz-Filipe and Peter Schneider-Kamp. Formally Proving the Boolean Pythagorean Triples Conjecture (details)
- Rachid Echahed and Aude Maignan. On Simultaneous Transformations with Overlapping Graph Rewrite Systems (details)
- Florian Frohn and Jürgen Giesl. Analyzing Runtime Complexity via Innermost Runtime Complexity (details)
- Thibault Gauthier, Cezary Kaliszyk and Josef Urban. TacticToe: Learning to Reason with HOL4 Tactics (details)
- Nicola Gigante, Angelo Montanari and Mark Reynolds. A One-Pass Tree-Shaped Tableau for LTL+Past (details)
- Tobias Gleißner, Alexander Steen and Christoph Benzmüller. Theorem Provers For Every Normal Modal Logic (details)
- Emmanuel Hainry and Romain Péchoux. Higher order interpretation for higher order complexity (details)
- Miika Hannula, Juha Kontinen and Sebastian Link. On the Interaction of Inclusion Dependencies with Independence Atoms (details)
- Nicholas Hollingum and Bernhard Scholz. Cauliflower: a Solver Generator for Context-Free Language Reachability (details)
- Jean-Pierre Jouannaud and Pierre-Yves Strub. A complete proof of Coq modulo Theory (details)
- Ozan Kahramanogullari. Deep Proof Search in MELL (details)
- Temesghen Kahsai, Rody Kersten, Philipp Ruemmer and Martin Schäf. Quantified Heap Invariants for Object-Oriented Programs (details)
- Temesghen Kahsai, Xavier Thirioux, Pierre-Loic Garoche, Arie Gurfinkel, Hamza Bourbouh and Christophe Garion. Automated analysis of Stateflow models (details)
- Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits and Armin Biere. Blocked Clauses in First-Order Logic (details)
- Laura Kovacs and Andrei Voronkov. First-Order Interpolation and Interpolating Proofs Systems (details)
- Bjoern Lellmann, Carlos Olarte and Elaine Pimentel. A uniform framework for substructural logics with modalities (details)
- Josef Lindsberger, Alexander Maringele and Georg Moser. Quantified Boolean Formulas: Call the Plumber! (details)
- Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk. Deep Network Guided Proof Search (details)
- Dimas Melo Filho, Fred Freitas and Jens Otten. RACCOON: A Connection Reasoner for the Description Logic ALC (details)
- Dmitry Mordvinov and Grigory Fedyukovich. Synchronizing Constrained Horn Clauses (details)
- Adrian Rebola-Pardo and Tobias Philipp. Towards a Semantics of Unsatisfiability Proofs with Inprocessing (details)
- Hira Syeda and Gerwin Klein. Reasoning about Translation Lookaside Buffers (details)
- David Toman and Grant Weddell. An Interpolation-based Compiler and Optimizer for Relational Queries (System Implementation Report) (details)
IWIL-2017-4-RegerSuda.pdf
IWIL-2017-s1-RegerSudaVoronkov.pdf
LPAR-21-s1-Muggleton.pdf
LPAR-21-s3-Visser.pdf LPAR-21-s4-Majumdar.pdf
LPAR-21-4-CiabattomiRamanayake.pdf
LPAR-21-8-FilhoFreitasOtten.pdf
LPAR-21-14-BauerHofman.pdf
LPAR-21-19-BistarelliMartinelliEtal.pdf
LPAR-21-20-BogaertsTernovskaMitchell.pdf
LPAR-21-21-JouannaudStrub.pdf
LPAR-21-22-HollingumScholz.pdf
LPAR-21-24-BartheEspitauGregoireHsuStrub.pdf
LPAR-21-25-LoosIrvingSzegedyKaliszyk.pdf
LPAR-21-26-GleissnerSteenBenzmueller.pdf
LPAR-21-32-CruzFilipeSchneiderKamp.pdf
LPAR-21-34-KieslSudaSeidlTompitsBiere.pdf
LPAR-21-39-KahsaiKerstenPuemmerSchaef.pdf
LPAR-21-41-FrohnGiesl.pdf
LPAR-21-42-HainryPechoux.pdf
LPAR-21-46-LindsbergerMaringeleMoser.pdf
LPAR-21-47-GauthierKaliszykUrban.pdf
LPAR-21-50-BoumarafiSaisSalhi.pdf
LPAR-21-54-Kahramanogullari.pdf
LPAR-21-60-BlahoudekDuretEtal.pdf
LPAR-21-63-BourbouhGarocheEtal.pdf
LPAR-21-65-EchahedMaignan.pdf
LPAR-21-66-GiganteMontanariReynolds.pdf
LPAR-21-77-BjornerJovanovicLepointRuemmerSchaf.pdf