LPAR Accepted Papers

The list of accepted papers is also available with abstracts.

• Guy Katz. On Module-Based Abstraction and Repair of Behavioral Programs (details)
• František Blahoudek, Jan Strejcek and Mojmir Kretinsky. Comparison of LTL to Deterministic Rabin Automata Translators (details)
• Stephan Schulz. System Description: E 1.8 (details)
• Tero Laitinen, Tommi Junttila and Ilkka Niemelä. Simulating Parity Reasoning (details)
• Gabriel Scherer and Jan Hoffmann. Tracking Data-Flow with Open Closure Types (details)
• George Metcalfe and Petr Cintula. Herbrand Theorems for Substructural Logics (details)
• Christoph Benzmueller and Thomas Raths. HOL based First-order Modal Logic Provers (details)
• Gudmund Grov, Aleks Kissinger and Yuhui Lin. A Graphical Language for Proof Strategies (details)
• Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon and Denis Poitrenaud. Three SCC-based Emptiness Checks for Generalized Büchi Automata (details)
• Giovanni Casini and Umberto Straccia. Towards Rational Closure for Fuzzy Logic: The Case of Propositional G\"odel Logic (details)
• David Harel, Amir Kantor and Guy Katz. Relaxing Synchronization Constraints in Behavioral Programs (details)
• Bernhard Heinemann. Characterizing Subset Spaces as Bi-Topological Structures (details)
• Riku Nortje, Arina Britz and Thomas Meyer. Reachability modules for the Description Logic SRIQ (details)
• Luca Aceto, Dario Della Monica, Anna Ingolfsdottir, Angelo Montanari and Guido Sciavicco. An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics (details)
• Filipe Casal and João Rasga. Revisiting the equivalence of shininess and politeness (details)
• Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson and Ewen MacLean. Proof-Pattern Recognition in ACL2 (details)
• Patrick Blackburn, Thomas Bolander, Torben Braüner and Klaus Frovin Joergensen. A Seligman-style Tableau System (details)
• Josh Berdine, Nikolaj Bjorner, Samin Ishtiaq, Jael Kriener and Christoph Wintersteiger. Resourceful Reachability as HORN-LRA (details)
• Alessandro Artale, Roman Kontchakov, Vladiaslav Ryzhikov and Michael Zakharyaschev. The Complexity of Clausal Fragments of LTL (details)
• Mélanie Boudard and Olivier Hermant. Polarizing Double Negation Translations (details)
• Marijn Heule and Armin Biere. Blocked Clause Decomposition (details)
• Szymon Klarman and Thomas Meyer. Prediction and Explanation over DL-Lite Data Streams (details)
• Elvira Albert, Samir Genaim and Enrique Martin-Martin. May-Happen-in-Parallel Analysis for Priority-based Scheduling (details)
• Belaïd Benhamou. Dynamic symmetry breaking in answer set programming (details)
• Chuan Jiang and Ting Zhang. Partial Backtracking in CDCL Solvers (details)
• Cezary Kaliszyk and Josef Urban. Lemma Mining over HOL Light (details)
• Tim French, John Mccabe-Dansted and Mark Reynolds. Verifying Temporal Properties in Real Models (details)
• Iain Whiteside, Dominik Dietrich and David Aspinall. Polar: A Framework for Proof Refactoring (details)
• Tahiry Rabehaja, Annabelle McIver and Georg Struth. An Event Structure Model for Probabilistic Concurrent Kleene Algebra (details)
• David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand and Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo (details)
• Peter Baumgartner and Joshua Bax. Proving Infinite Satisfiability (details)
• Régis Blanc, Ashutosh Gupta, Laura Kovacs and Bernhard Kragl. Tree Interpolation in Vampire (details)
• Uwe Egly, Florian Lonsing and Magdalena Widl. Long-distance Resolution: Proof Generation and Strategy Extraction in Search-based QBF Solving (details)
• Fabio Mogavero, Aniello Murano and Loredana Sorrentino. On Promptness in Parity Games (details)
• Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Hyvaerinen and Natasha Sharygina. PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification (details)
• Olivier Hermant and Allali Lisa. Semantic A-Translations and Super-Consistency entail Classical Cut Elimination (details)
• Sebastian A. Mödersheim, Thomas Gross and Luca Viganò. Defining Privacy is Supposed to be Easy (details)
• Pablo Barceló, Gaelle Fontaine and Anthony Widjaja Lin. Expressive Path Queries on Graphs with Data (details)
• Ari Saptawijaya and Luís Moniz Pereira. Incremental Tabling for Query-Driven Propagation of Logic Program Updates (details)
• David Aspinall, Ewen Denney and Christoph Lüth. A Semantic Basis for Proof Queries and Transformations (details)
• Maximilian Schlund, Michal Terepeta and Michael Luttenberger. Putting Newton into Practice: A Solver for Polynomial Equations over Semirings (details)
• Mikolas Janota, Radu Grigore and Joao Marques-Silva. On QBF Proofs and Preprocessing (details)
• Alexey Ignatiev, Antonio Morgado, Jordi Planes and Joao Marques-Silva. Maximal Falsifiability: Definitions, Algorithms, and Applications (details)
• Calin-Rares Turliuc, Nataly Maimari, Alessandra Russo and Krysia Broda. On Minimality and Integrity Constraints in Probabilistic Abduction (details)
• Ugo Dal Lago and Giulio Pellitta. Complexity Analysis in Presence of Control Operators and Higher-Order Functions (details)
• Tom Gundersen, Willem Heijltjes and Michel Parigot. A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus (details)
• Patrick Koopmann and Renate A. Schmidt. Forgetting Concept and Role Symbols in ALCH-Ontologies (details)
• Anton Belov, António Morgado and Joao Marques-Silva. SAT Preprocessing for MaxSAT (details)
• Hira Taqdees and Osman Hasan. Formalization of Laplace Transform using the Multivariable Calculus Theory of HOL-Light (details)
• Krishnendu Chatterjee, Vojtech Forejt and Dominik Wojtczak. Multi-objective discounted reward verification in graphs and MDPs (details)
• Luís Cruz-Filipe, Rita Henriques and Isabel Nunes. Description logics, rules and multi-context systems (details)
• Shachar Itzhaky, Sumit Gulwani, Neil Immerman and Mooly Sagiv. Solving Geometry Problems using a Combination of Symbolic and Numerical Reasoning (details)
• Szymon Klarman. Practical Querying of Temporal Data via OWL 2 QL and SQL:2011 (details)
• Manuel Lamotte-Schubert and Christoph Weidenbach. BDI: A New Decidable First-order Clause Class (details)
• Francesco Alberti, Silvio Ghilardi and Natasha Sharygina. Acceleration-based safety decision procedure for programs with arrays (details)
• Patrick Doherty, Fredrik Heintz and Jonas Kvarnström. Robotics, Temporal Logic and Stream Reasoning (details)
• Abhijeet Mohapatra and Michael Genesereth. An Incremental Algorithm to Optimally Maintain Aggregate Views (details)
• Gabriel Aranda, Susana Nieva, Fernando Saenz-Perez and Jaime Sánchez-Hernández. Incorporating Hypothetical Views and Extended Recursion into SQL Database Systems (details)
• Martin Baláž, Jozef Frtús and Martin Homola. Conflict Resolution in Structured Argumentation (details)
• Jiefei Ma, Rob Miller, Leora Morgenstern and Theodore Patkos. An Epistemic Event Calculus for ASP-based Reasoning About Knowledge of the Past, Present and Future (details)
• Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg. Effectively Monadic Predicates (details)
• Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav. Instantiations, Zippers and EPR Interpolation (details)