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
