Accepted Papers

for IJCAR 2012 (in no particular order)

Full Papers (32)

Roberto Bruttomesso, Silvio Ghilardi and Silvio Ranise: From Strong Amalgamability to Modularity of Quantifier-Free Interpolation

Pierre-Cyrille Heam, Vincent Hugot and Olga Kouchnarenko: From Linear Temporal Logic Properties to Rewrite Propositions

François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout and Guillaume Melquiond: A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic

Matthias Baaz, Ori Lahav and Anna Zamansky: Effective Finite-valued Semantics for Labelled Calculi

Stephan Falke and Deepak Kapur: Rewriting Induction + Linear Arithmetic = Decision Procedure

Markus Latte and Martin Lange: Branching Time? Pruning Time!

Mnacho Echenim and Nicolas Peltier: A Calculus for Generating Ground Explanations

ńźurica Nikolińá and Fausto Spoto: Reachability Analysis of Program Variables

Taus Brock-Nannestad and Carsten Schuermann: Truthful Monadic Abstractions

Dejan Jovanovińá and Leonardo De Moura: Solving Non-Linear Arithmetic

Andrew Marshall and Paliath Narendran: A New Algorithm for Unification Modulo One-Sided Distributivity

Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran and Michael Rusinowitch: Unification modulo Synchronous Distributivity

Rajeev Gore and Jimmy Thomson: BDD-based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics

Alwen Tiu: Stratification in Logics of Definitions

Sicun Gao, Jeremy Avigad and Edmund Clarke: Delta-Complete Decision Procedures for Satisfiability over the Reals

Simon Foster and Georg Struth: Automated Analysis of Regular Algebra

Stephanie Delaune, Steve Kremer and Daniel Pasaila: Security protocols, constraint systems, and group theories

Franz Baader, Stefan Borgwardt and Barbara Morawska: SAT-Encoding of Unification in ELHR+ w.r.t. Cycle-Restricted Ontologies

Andrej Spielmann and Viktor Kuncak: Synthesis for Unbounded Bitvector Arithmetic

Matti Järvisalo, Marijn Heule and Armin Biere: Inprocessing Rules

Conrad Rau, David Sabel and Manfred Schmidt-Schauss: Correctness of Program Transformations as a Termination Problem

Melisachew Wudage Chekol, J√©r√īme Euzenat, Pierre Geneves and Nabil Laya√Įda:¬†SPARQL Query Containment under RDFS Entailment Regime

Stéphane Demri, Amit Kumar Dhar and Arnaud Sangnier: Taming Past LTL and Flat Counter Systems

Pascal Fontaine, Stephan Merz and Christoph Weidenbach: Combination of disjoint theories: beyond decidability

Fabian Emmes, Tim Enger and J√ľrgen Giesl: Proving Non-Looping Non-Termination Automatically

Stefan Borgwardt, Felix Distel and Rafael Pe√Īaloza: How Fuzzy is my Fuzzy Description Logic?

Daniel Kuehlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban and Tom Heskes: Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics

Roberto Sebastiani and Silvia Tomasi: Optimization in SMT with LA(Q) Cost Functions

Andreas Steigmiller, Thorsten Liebig and Birte Glimm: Extended Caching, Backjumping and Merging for Expressive Description Logics

Jan-David Quesel and Andre Platzer: Playing Hybrid Games with KeYmaera

Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel and Andrei Voronkov: EPR-based bounded model checking at word level

Frank de Boer, Marcello Bonsangue and Jurriaan Rot: Automated Verification of Recursive Programs with Pointers

System Description Papers (9)

Mélanie Jacquel, Karim Berkani, David Delahaye and Catherine Dubois: Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover

Thomas Sternagel and Harald Zankl: KBCV – Knuth-Bendix Completion Visualizer

Boris Konev, Michel Ludwig and Frank Wolter: Logical Difference Computation with CEX 2.5

Matej Urbas and Mateja Jamnik: Diabelli: A heterogeneous reasoning framework

Martin Suda and Christoph Weidenbach: A PLTL-prover based on labelled superposition with partial model guidance

Franz Baader, Julian Mendez and Barbara Morawska: UEL: Unification Solver for the Description Logic EL, System Description

Thomas Raths and Jens Otten: The QMLTP Problem Library for First-order Modal Logics

Chad Brown: Satallax: An Automated Higher-Order Prover

Stephan Schulz: Fingerprint Indexing for Paramodulation and Rewriting

  • Calendar of Events

     June 2014