| Authors | Title | Conference | Paper | Talk |
|---|
| Beniamino Accattoli | On the Formalization of Lambda-Calculus Confluence and Residuals | IWC |  | Jul 13 09:25 |
| Samuel Mimram | An Introduction to Higher-Dimensional Rewriting Theory | IWC | | |
| Yves Guiraud, Eric Hoffbeck and Philippe Malbos | Confluence of linear rewriting and homology of algebras | IWC | | Jul 13 15:30 |
| Lars Hellström | Critical Pairs in Network Rewriting | IWC | | Jul 13 12:00 |
| Nao Hirokawa, Aart Middeldorp and Christian Sternagel | Normalization Equivalence of Rewrite Systems | IWC | | Jul 13 16:30 |
| Julian Nagele and René Thiemann | Certification of Confluence Proofs using CeTA | IWC | | Jul 13 10:45 |
| Naoki Nishida, Makishi Yanagisawa and Karl Gmeiner | On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation | IWC | | Jul 13 12:30 |
| Michio Oyamaguchi and Nao Hirokawa | Confluence and Critical-Pair-Closing Systems | IWC | | Jul 13 11:15 |
| Masahiko Sakai, Michio Oyamaguchi and Mizuhito Ogawa | Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract) | IWC | | Jul 13 17:00 |
| Anna Slobodova, Jared Davis and Sol Swords | Microcode Verification - Another Piece of the Microprocessor Verification Puzzle | ITP | | Jul 14 15:00 |
| Peter Sewell | Retrofitting Rigour | ITP | | Jul 16 15:00 |
| Rod Chapman and Florian Schanda | Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK | ITP | | Jul 15 15:00 |
| Abhishek Anand and Vincent Rahli | Towards a Formally Verified Proof Assistant | ITP | | Jul 14 10:45 |
| Vincent Aravantinos and Sofiene Tahar | Implicational Rewriting Tactics in HOL | ITP | | Jul 17 15:30 |
| Jeremy Avigad, Robert Y. Lewis and Cody Roux | A heuristic prover for real inequalities | ITP | | Jul 16 16:30 |
| Evmorfia-Iro Bartzia and Pierre-Yves Strub | A Formal Library for Elliptic Curves in the Coq Proof Assistant | ITP | | Jul 15 10:45 |
| Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu and Dmitriy Traytel | Truly Modular (Co)datatypes for Isabelle/HOL | ITP | | Jul 14 16:30 |
| Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel | Cardinals in Isabelle/HOL | ITP | | Jul 15 12:15 |
| Sandrine Blazy, Vincent Laporte and David Pichardie | Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code | ITP | | Jul 16 17:30 |
| Timothy Bourke, Rob Van Glabbeek and Peter Höfner | Showing invariance compositionally for a process algebra for network protocols | ITP | | Jul 16 14:30 |
| Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote and Enrico Tassi | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) | ITP | | Jul 16 10:45 |
| David Cock | From Operational Models to Information Theory - Side Channels in pGCL with Isabelle | ITP | | Jul 14 14:30 |
| Cyril Cohen and Anders Mörtberg | A Coq Formalization of Finitely Presented Modules | ITP | | Jul 16 11:15 |
| Robert Dockins | Formalized, effective domain theory in Coq | ITP | | Jul 17 10:45 |
| Christian Doczkal and Gert Smolka | Completeness and Decidability Results for CTL in Coq | ITP | | Jul 17 11:15 |
| Jean-François Dufourd | Hypermap Specification and Certified Linked Implementation using Orbits | ITP | | Jul 17 15:00 |
| Kento Emoto, Frédéric Loulergue and Julien Tesson | A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction | ITP | | Jul 15 11:15 |
| Jason Gross, Adam Chlipala and David Spivak | Experience Implementing a Performant Category-Theory Library in Coq | ITP | | Jul 14 17:30 |
| Nao Hirokawa, Aart Middeldorp and Christian Sternagel | A New and Formalized Proof of Abstract Completion | ITP | | Jul 17 14:30 |
| Ramana Kumar, Rob Arthan, Magnus O. Myreen and Scott Owens | HOL with Definitions: Semantics, Soundness, and a Verified Implementation | ITP | | Jul 14 11:45 |
| Peter Lammich | Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm | ITP | | Jul 15 11:45 |
| Andreas Lochbihler and Johannes Hölzl | Recursive Functions on Lazy Lists via Domains and Topologies | ITP | | Jul 14 17:00 |
| Mohamed Yousri Mahmoud, Vincent Aravantinos and Sofiene Tahar | Formal Verification of Optical Quantum Flip Gate | ITP | | Jul 16 11:45 |
| Gregory Malecha, Adam Chlipala and Thomas Braibant | Compositional Computational Reflection | ITP | | Jul 17 12:15 |
| Daniel Matichuk, Toby Murray and Makarius Wenzel | An Isabelle Proof Method Language | ITP | | Jul 15 16:30 |
| J Strother Moore | Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete | ITP | | Jul 14 12:15 |
| Magnus O. Myreen and Jared Davis | The reflective Milawa theorem prover is sound (down to the machine code that runs it) | ITP | | Jul 14 11:15 |
| Guyslain Naves and Arnaud Spiwack | Balancing lists: a proof pearl | ITP | | Jul 15 14:30 |
| Tobias Nipkow and Dmitriy Traytel | Unified Decision Procedures for Regular Expression Equivalence | ITP | | Jul 16 17:00 |
| Martin Ring and Christoph Lüth | Collaborative Interactive Theorem Proving with Clide | ITP | | Jul 15 17:30 |
| Umair Siddique, Mohamed Yousri Mahmoud and Sofiene Tahar | On the Formalization of Z-Transform in HOL | ITP | | Jul 16 12:15 |
| Matthieu Sozeau and Nicolas Tabareau | Universe Polymorphism in Coq | ITP | | Jul 17 11:45 |
| Makarius Wenzel | Asynchronous User Interaction and Tool Integration in Isabelle/PIDE | ITP | | Jul 15 17:00 |
| Rob Arthan | HOL Constant Definitions Done Right | ITP | | Jul 15 12:45 |
| Matt Kaufmann and J Strother Moore | Rough Diamond: An Extension of Equivalence-based Rewriting | ITP | | Jul 14 12:45 |
| Robbert Krebbers, Xavier Leroy and Freek Wiedijk | Formal C semantics: CompCert and the C standard | ITP | | Jul 17 12:45 |
| Disha Puri, Sandip Ray, Kecheng Hao and Fei Xie | Mechanical Certification of Loop Pipelining Transformations: A Preview | ITP | | Jul 16 12:45 |
| Gergei Bana and Hubert Comon-Lundh | Protocol Indistinguishability and the Computationally Complete Symbolic Attacker | FCS-FCC | | Jul 18 16:30 |
| Abhishek Bichhawat, Vineet Rajani, Deepak Garg and Christian Hammer | Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis | FCS-FCC | | Jul 18 15:00 |
| Gergei Bana and Mitsuhiro Okada | Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model | FCS-FCC | | Jul 18 17:10 |
| Sibylle Froeschle | On Well-Founded Security Protocols (Extended Abstract) | FCS-FCC | | Jul 18 16:50 |
| Hubert Comon-Lundh, Veronique Cortier and Guillaume Scerri | A tool for automating the computationally complete symbolic attacker | FCS-FCC | | Jul 18 12:00 |
| Catalin Hritcu | Micro-Policies: Formally Verified Tagging Schemes for Safety and Security (Extended Abstract) | FCS-FCC | | Jul 18 15:30 |
| Piotr Mardziel, Mario Alvim and Michael Hicks | Adversary Gain vs. Defender Loss in Quantified Information Flow | FCS-FCC | | Jul 18 14:30 |
| Alberto Cappai and Ugo Dal Lago | Towards a Coinductive Characterization of Computational Indistinguishability | FCS-FCC | | Jul 18 12:20 |
| Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott | Towards Timed Models for Cyber-Physical Security Protocols | FCS-FCC | | Jul 18 17:30 |
| Anupam Datta, Dilsun Kaynar, Divya Sharma and Arunesh Sinha | Actual Causes of Security Violations (Short Paper) | FCS-FCC | | Jul 18 12:40 |
| John D Ramsdell, Daniel Dougherty, Joshua Guttman and Paul D Rowe | A Hybrid Analysis for Security Protocols with State | FCS-FCC | | Jul 18 09:45 |
| Marc Bezem | Coherent Logic and Applications | CHR | | Jul 18 09:00 |
| Ralf Gerlich | Automated Test Case Generation and Model Checking with CHR | CHR | | Jul 18 10:45 |
| Falco Nogatz and Thom Fruehwirth | From XML Schema to JSON Schema: Translation with CHR | CHR | | Jul 18 11:15 |
| Edmund Soon Lee Lam and Iliano Cervesato | Constraint Handling Rules with Multiset Comprehension Patterns | CHR | | Jul 18 11:45 |
| Jean-Raymond Abrial | Program Verification (B Method) | APPA | | Jul 18 16:30 |
| Clark Barrett, Pascal Fontaine and Leonardo De Moura | SMT-Solvers | APPA | | Jul 18 09:30 |
| Gilles Barthe, François Dupressoir, Benjamin Grégoire, Benedikt Schmidt and Pierre-Yves Strub | Security | APPA | | Jul 18 17:00 |
| Christoph Benzmüller | Higher-Order Automated Theorem Provers | APPA | | Jul 18 11:15 |
| Gilles Dowek | Deduction Modulo Theory | APPA | | Jul 18 15:00 |
| Alessio Guglielmi | Deep Inference | APPA | | Jul 18 17:30 |
| Marijn Heule and Armin Biere | Satisfiability Solvers | APPA | | Jul 18 09:00 |
| Alexander Leitsch | Mathematical Proof Analysis | APPA | | Jul 18 15:30 |
| Dale Miller | Foundational Proof Certificates | APPA | | Jul 18 14:30 |
| Christine Paulin-Mohring | Calculus of Inductive Constructions | APPA | | Jul 18 12:30 |
| Stephan Schulz and Geoff Sutcliffe | Proof Generation for Saturating First-Order Theorem Provers | APPA | | Jul 18 10:45 |
| Makarius Wenzel | Interactive Theorem Provers from the perspective of Isabelle/Isar | APPA | | Jul 18 12:00 |
| Andrew Reynolds, Cesare Tinelli and Leonardo De Moura | Finding Conflicting Instances of Quantified Formulas in SMT | QUANTIFY | | Jul 18 17:30 |
| Michael Cashmore, Maria Fox and Enrico Giunchiglia | Encoding Reachability with Quantification | QUANTIFY | | Jul 18 11:30 |
| Javier Álvez, Montserrat Hermo and Paqui Lucio | Projective Quantifier Elimination for Equational Constraint Solving | QUANTIFY | | Jul 18 15:30 |
| Aarne Ranta | Machine Translation: Green, Yellow, and Red (abstract) | NLSR | | Jul 18 09:00 |
| Cleo Condoravdi, Kyle Richardson, Vishal Sikka, Asuman Suenbuel and Richard Waldinger | Natural Language Access to Data | NLSR | | Jul 18 11:15 |
| Jeroen Van Grondelle, Christina Unger and Frank Smit | Exposing Predictive Analytics through Natural Language | NLSR | | Jul 18 10:45 |
| Ulrich Berger, Alison Jones and Monika Seisenberger | Program Extraction Applied to Monadic Parsing | NLCS | | Jul 18 16:30 |
| Heather Burnett | Mereological Comparatives in Delineation Semantics | NLCS | | Jul 17 11:15 |
| Claudia Casadio and Aleksandra Kislak-Malinowska | Computing Italian clitic and relative clauses with tupled pregroups | NLCS | | Jul 17 15:30 |
| Robin Cooper | How to do things with types | NLCS | | Jul 17 10:45 |
| Marcos Cramer | Modelling implicit dynamic introduction of function symbols in mathematical texts | NLCS | | Jul 18 15:30 |
| Richard Crouch | Transfer Semantics for the Clear Parser | NLCS | | Jul 18 11:45 |
| Tim Fernando | Signatures as open-ended types | NLCS | | |
| Christophe Fouquere and Myriam Quatrini | Divergence in Dialogues | NLCS | | Jul 18 15:00 |
| Nissim Francez | Proof-Theoretic Semantics for intensional transitive verbs | NLCS | | Jul 17 11:45 |
| Makoto Kanazawa and Junri Shimada | Toward a Logic of Cumulative Quantification | NLCS | | Jul 17 17:30 |
| Juyeon Kang and Saint Dizier Patrick | Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts | NLCS | | Jul 18 12:15 |
| Stepan Kuznetsov | On Translating Context-Free Grammars into Lambek Categorial Grammars | NLCS | | Jul 18 17:00 |
| Kristina Liefke | Solving Partee's Temperature Puzzle in an EFL-Ontology | NLCS | | Jul 17 17:00 |
| Jiří Maršík and Maxime Amblard | Algebraic Effects and Handlers in Natural Language Interpretation | NLCS | | Jul 17 16:30 |
| Rohit Parikh | Grice, Hoare and Nash: some comments on conversational implicature | NLCS | | Jul 17 12:15 |
| Ondrej Rypacek and Mehrnoosh Sadrzadeh | A low-level treatment of quantifiers in categorical compositional distributional semantics | NLCS | | Jul 18 14:30 |
| Josep Silva | Automatic Detection of Webpage Candidates for Site-Level Web Template Extraction | WWV | | Jul 18 14:30 |
| R. Ramanujam and S. Sheerazuddin | A local logic for realizability in web service choreographies | WWV | | Jul 18 17:00 |
| Asad Ali and Maribel Fernandez | Static Enforcement of Role-Based Access Control | WWV | | Jul 18 16:30 |
| Jasmin Christian Blanchette | My Life with an Automatic Theorem Prover | Vampire | | Jul 23 14:30 |
| Laura Kovacs and Andrei Voronkov | First-Order Theorem Proving with Vampire | Vampire | | Jul 23 10:45 |
| Ashutosh Gupta | Proofs in Vampire | Vampire | | Jul 23 12:00 |
| Giles Reger, Martin Suda and Andrei Voronkov | Playing with AVATAR | Vampire | | Jul 23 12:30 |
| Armin Biere, Ioan Dragan, Laura Kovacs and Andrei Voronkov | SAT solving experiments in Vampire | Vampire | | Jul 23 16:30 |
| Evgeny Kotelnikov, Laura Kovacs and Andrei Voronkov | First Class Boolean Type in First-Order Theorem Proving and TPTP | Vampire | | Jul 23 17:00 |
| Ashutosh Gupta, Laura Kovacs, Bernhard Kragl and Andrei Voronkov | Reasoning in First-Order Theories with Extensionality | Vampire | | Jul 23 17:30 |
| Nicola Gambino | A unified approach to Univalent Foundations and Homotopical Algebra | RTA-TLCA | | |
| Kohei Honda, Nobuko Yoshida and Martin Berger | Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus | RTA-TLCA | | |
| Manfred Schmidt-Schauss | Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk) | RTA-TLCA | | |
| Andreas Abel, Brigitte Pientka, Anton Setzer and David Thibodeau | Unnesting of Copatterns | RTA-TLCA | | Jul 15 17:30 |
| Takahito Aoto, Yoshihito Toyama and Kazumasa Uchida | Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams | RTA-TLCA | | Jul 14 17:30 |
| Kyungmin Bae and Jose Meseguer | Predicate Abstraction of Rewrite Theories | RTA-TLCA | | Jul 16 11:15 |
| Marc Bagnol and Clément Aubert | Unification and Logarithmic Space | RTA-TLCA | | Jul 14 11:45 |
| Stefano Berardi and Silvia Steila | Ramsey Theorem as an intuitionistic property of well founded relations | RTA-TLCA | | Jul 15 10:45 |
| Aleš Bizjak, Lars Birkedal and Marino Miculan | A Model of Countable Nondeterminism in Guarded Type Theory | RTA-TLCA | | Jul 16 15:30 |
| Guillaume Burel | Cut Admissibility by Saturation | RTA-TLCA | | Jul 16 10:45 |
| Carles Creus and Guillem Godoy | Automatic Evaluation of Context-Free Grammars (System Description) | RTA-TLCA | | Jul 14 12:45 |
| Carles Creus and Guillem Godoy | Tree Automata with Height Constraints between Brothers | RTA-TLCA | | Jul 17 10:45 |
| Łukasz Czajka | A Coinductive Confluence Proof for Infinitary Lambda-Calculus. | RTA-TLCA | | Jul 14 16:30 |
| Daniel de Carvalho and Jakob Grue Simonsen | An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting | RTA-TLCA | | Jul 14 11:15 |
| Mariangiola Dezani-Ciancaglini and Silvia Ghilezan | Preciseness of subtyping on intersection and union types | RTA-TLCA | | Jul 16 17:30 |
| Martin Escardo and Alex Simpson | Abstract datatypes for real numbers in type theory | RTA-TLCA | | Jul 16 16:30 |
| Peng Fu and Aaron Stump | Self Types for Dependently Typed Lambda Encodings | RTA-TLCA | | Jul 15 16:30 |
| Carsten Fuhs and Cynthia Kop | First-Order Formative Rules | RTA-TLCA | | Jul 15 11:45 |
| Nao Hirokawa and Georg Moser | Automated Complexity Analysis Based on Context-Sensitive Rewriting | RTA-TLCA | | Jul 14 12:15 |
| Martin Hofmann and Georg Moser | Amortised Resource Analysis and Typed Polynomial Interpretations | RTA-TLCA | | Jul 15 15:30 |
| Jiaxiang Liu, Nachum Dershowitz and Jean-Pierre Jouannaud | Confluence by Critical Pair Analysis | RTA-TLCA | | Jul 14 17:00 |
| Carlos Lombardi, Alejandro Rios and Roel de Vrijer | Proof terms for infinitary rewriting | RTA-TLCA | | Jul 17 11:45 |
| Roberto Maieli | Construction of retractile proof structures | RTA-TLCA | | Jul 16 12:15 |
| Paul-André Melliès | Local states in string diagrams | RTA-TLCA | | Jul 16 17:00 |
| Koji Nakazawa and Tomoharu Nagai | Reduction System for Extensional Lambda-mu Calculus | RTA-TLCA | | Jul 17 11:15 |
| Cody Roux and Floris van Doorn | The Structural Theory of Pure Type Systems | RTA-TLCA | | Jul 15 17:00 |
| Manfred Schmidt-Schauss and David Sabel | Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB | RTA-TLCA | | Jul 14 15:30 |
| Sylvain Schmitz | Implicational Relevance Logic is 2-ExpTime-Complete | RTA-TLCA | | Jul 14 10:45 |
| Richard Statman | Near semi-rings and lambda calculus | RTA-TLCA | | Jul 17 12:15 |
| Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon Moore, Traian Florin Serbanuta and Grigore Rosu | All-Path Reachability Logic | RTA-TLCA | | Jul 16 11:45 |
| Christian Sternagel and René Thiemann | Formalizing monotone algebras for certification of termination- and complexity proofs | RTA-TLCA | | Jul 15 12:15 |
| Thomas Sternagel and Aart Middeldorp | Conditional Confluence (System Description) | RTA-TLCA | | Jul 14 18:00 |
| Akihisa Yamada, Keiichirou Kusakari and Toshiki Sakabe | Nagoya Termination Tool | RTA-TLCA | | Jul 15 12:45 |
| Hans Zantema, Barbara Koenig and Sander Bruggink | Termination of Cycle Rewriting | RTA-TLCA | | Jul 15 11:15 |
| Marcin Benke, Viviana Bono and Aleksy Schubert | Lucretia — intersection type polymorphism for scripting languages | ITRS | | Jul 18 14:30 |
| Jan Bessai, Boris Düdder, Andrej Dudenhefner and Moritz Martens | Delegation-based Mixin Composition Synthesis | ITRS | | Jul 18 17:00 |
| Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria and Maddalena Zacchi | On Isomorphism of "Functional'' Intersection and Union Types | ITRS | | Jul 18 11:15 |
| Ugo De Liguoro and Tzu-Chun Chen | Semantic Types for Classes and Mixins | ITRS | | Jul 18 16:30 |
| Charles Grellois and Paul-André Melliès | Indexed linear logic and higher-order model checking | ITRS | | Jul 18 12:30 |
| Kentaro Kikuchi | Uniform Proofs of Normalisation and Approximation for Intersection Types | ITRS | | Jul 18 12:00 |
| Mário Pereira, Sandra Alves and Mário Florido | Liquid Intersection Types | ITRS | | Jul 18 15:00 |
| Richard Statman | A Finite Model Property for Intersection Types | ITRS | | Jul 18 10:45 |
| Uwe Waldmann | Hierarchic Superposition Revisited | PAAR | | Jul 23 09:15 |
| Negin Arhami and Geoff Sutcliffe | The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics | PAAR | | Jul 23 11:15 |
| Joshua Bax | A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories | PAAR | | Jul 23 14:30 |
| Maria Paola Bonacina and David Plaisted | SGGS Theorem Proving: an Exposition | PAAR | | Jul 23 17:30 |
| Simon Cruanes | Logtk : A Logic ToolKit for Automated Reasoning and its Implementation | PAAR | | Jul 23 15:00 |
| Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish | Beagle as a HOL4 external ATP method | PAAR | | Jul 23 16:30 |
| Cezary Kaliszyk, Josef Urban and Jiri Vyskocil | Machine Learner for Automated Reasoning 0.4 and 0.5 | PAAR | | Jul 23 11:45 |
| Muhammad Nassar and Geoff Sutcliffe | Automated Theorem Proving using the TPTP Process Instruction Language | PAAR | | Jul 23 10:45 |
| Salman Saghafi and Daniel Dougherty | Razor: Provenance and Exploration in Model-Finding | PAAR | | Jul 23 17:00 |
| Sophie Tourret, Mnacho Echenim and Nicolas Peltier | A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses | PAAR | | Jul 23 08:45 |
| Josef Urban | BliStr: The Blind Strategymaker | PAAR | | Jul 23 12:15 |
| Daniel Wand | Polymorphic+Typeclass Superposition | PAAR | | Jul 23 15:30 |
| Alex Simpson | Cyclic Proof for Quantitative Logics | GSB | | Jul 13 14:30 |
| Anna Zamansky | Semantics and Proof Theory in Team Play: The Case of Paraconsistent Logics | GSB | | Jul 13 09:05 |
| Rob Arthan and Paulo Oliva | On Affine Logic and Łukasiewicz Logic | GSB | | Jul 13 17:20 |
| Paolo Baldi | A Proof Theoretic Approach to Standard Completeness | GSB | | Jul 13 16:55 |
| Roy Dyckhoff and Sara Negri | Coherentisation of Accessibility Conditions in Labelled Sequent Calculi | GSB | | |
| Giuseppe Greco, Sabine Frittella, Alexander Kurz, Alessandra Palmigiano and Vlasta Sikimić | Display-Type Calculi and Their Cut Elimination Metatheorem | GSB | | Jul 13 12:25 |
| Dominic Hughes | Simpler Proof Net Quantifiers: Unification Nets (Work in Progress) | GSB | | Jul 13 17:45 |
| Tomasz Kowalski | Link Formulas in Implication Fragments of Substructural Logics | GSB | | Jul 13 16:30 |
| Ori Lahav and Yoni Zohar | On the Construction of Analytic Sequent Calculi for Sub-Classical Logics | GSB | | Jul 13 09:50 |
| Björn Lellmann | Comparing Sequent Calculi via Hilbert-Style Axioms | GSB | | Jul 13 10:45 |
| Paolo Maffezioli and David Gilbert | Sequent Systems for Classical Modal Logics | GSB | | Jul 13 11:10 |
| Sonia Marin and Lutz Straßburger | Modular Systems for Intuitionistic Modal Logics in Nested Sequents | GSB | | Jul 13 15:15 |
| Alexandre Rademaker and Hermann Haeusler | An Intuitionisticaly Based Description Logic | GSB | | Jul 13 15:40 |
| Daniyar Shamkanov | Lyndon Interpolation for the Modal mu-Calculus | GSB | | Jul 13 11:35 |
| Thomas Studer | On Cuts and Cut-Elimination in Modal Fixed Point Logics | GSB | | Jul 13 12:00 |
| Jose Meseguer | Extensible Symbolic System Analysis | UNIF | | Jul 13 09:15 |
| Jordi Levy | On the Limits of Second-Order Unification | UNIF | | Jul 13 14:30 |
| Peter Hibbs, Paliath Narendran and Shweta Mehto | Unification Modulo Common List Functions | UNIF | | Jul 13 10:45 |
| Franz Baader and Barbara Morawska | Matching with respect to general concept inclusions in the Description Logic EL | UNIF | | Jul 13 11:15 |
| Philippe Balbiani and Tinko Tinchev | Unification in the normal modal logic Alt1 | UNIF | | Jul 13 11:45 |
| Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Catherine Meadows, Paliath Narendran and Christophe Ringeissen | On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract) | UNIF | | Jul 13 12:15 |
| Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran and Christophe Ringeissen | Hierarchical Combination of Matching Algorithms (Extended Abstract) | UNIF | | Jul 13 12:35 |
| Leonardo Manuel Cabrer and George Mectalfe | From Admissibility to a New Hierarchy of Unification Types | UNIF | | Jul 13 15:30 |
| Maria Paola Bonacina and David Plaisted | Constraint Manipulation in SGGS | UNIF | | Jul 13 16:30 |
| Tatyana Novikova and Vladimir Zakharov | Two-sided unification is NP-complete | UNIF | | Jul 13 17:00 |
| Alexander Baumgartner, Temur Kutsia, Jordi Levy and Mateu Villaret | Nominal Anti-Unification | UNIF | | Jul 13 17:30 |
| Andrea Vezzosi and Andreas Abel | A Categorical Perspective on Pattern Unification (Extended Abstract) | UNIF | | Jul 13 18:00 |
| Beta Ziliani and Matthieu Sozeau | Towards a better-behaved unification algorithm for Coq | UNIF | | Jul 13 18:30 |
| Juan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser and Andreas Zeller | Loop Invariants by Mutation, Dynamic Validation, and Static Checking | WING | | Jul 23 15:30 |
| Vivien Maisonneuve, Olivier Hermant and François Irigoin | ALICe: A Framework to Improve Affine Loop Invariant Computation | WING | | Jul 23 15:00 |
| Nathan Wasser and Richard Bubel | A Theorem Prover Backed Approach to Array Abstraction | WING | | Jul 23 14:30 |
| Nicos Angelopoulos | Perspectives Session | PLP | | |
| James Cussens | First-order representations for integer programming | PLP | | Jul 17 08:55 |
| Samer Abdallah and Nicolas Gold | Exploring probabilistic grammars of symbolic music using PRISM | PLP | | Jul 17 14:30 |
| Ryosuke Kojima and Taisuke Sato | Prefix and infix probability computation in PRISM | PLP | | Jul 17 10:45 |
| Wannes Meert, Guy Van den Broeck and Adnan Darwiche | Lifted Inference for Probabilistic Logic Programs | PLP | | Jul 17 15:30 |
| Eduardo Menezes de Morais | Approximated Probabilistic Answer Set Programming | PLP | | Jul 17 12:15 |
| Dimitar Shterionov and Gerda Janssens | cProbLog: Restricting the Possible Worlds of Probabilistic Logic Programs | PLP | | Jul 17 11:45 |
| Dries Van Daele, Angelika Kimmig and Luc De Raedt | PageRank, ProPPR and Stochastic Logic Programs | PLP | | Jul 17 09:50 |
| Wiebe Van Ranst and Joost Vennekens | An OpenCL implementation of a forward sampling algorithm for CP-logic | PLP | | Jul 17 15:00 |
| Jonas Vlasselaer, Joris Renkens, Guy Van den Broeck and Luc De Raedt | Compiling Probabilistic Logic Programs into Sentential Decision Diagrams | PLP | | Jul 17 11:15 |
| Ian Mackie | Continuations, closed reduction and process networks | Linearity | | Jul 13 14:30 |
| Elaine Pimentel | On modalities and linearity | Linearity | | Jul 13 08:45 |
| Michele Basaldella | Ludics without Designs I: Triads | Linearity | | Jul 13 16:30 |
| Taus Brock-Nannestad and Nicolas Guenot | Cut Elimination in Multifocused Linear Logic | Linearity | | Jul 13 12:15 |
| Kaustuv Chaudhuri | Undecidability of Multiplicative Subexponential Logic | Linearity | | Jul 13 10:45 |
| Ugo Dal Lago and Margherita Zorzi | Wave-Style Token Machines and Quantum Lambda Calculi | Linearity | | Jul 13 17:00 |
| Edward Gan, Jesse A. Tov and Greg Morrisett | Type Classes for Lightweight Substructural Types | Linearity | | Jul 13 15:30 |
| Giulio Guerrieri and Lorenzo Tortora De Falco | A new point of view on the Taylor expansion of proof-nets and uniformity | Linearity | | Jul 13 18:00 |
| Jennifer Paykin and Steve Zdancewic | A Linear/Producer/Consumer model of Classical Linear Logic | Linearity | | Jul 13 11:45 |
| Simona Ronchi Della Rocca, Antonio Bucciarelli and Delia Kesner | The inhabitation problem for non-idempotent intersection | Linearity | | Jul 13 09:45 |
| Marco Solieri | Geometry of Resource Interaction – A Minimalist Approach | Linearity | | Jul 13 17:30 |
| Zachary Sparks and Amr Sabry | Superstructural Reversible Logic | Linearity | | Jul 13 11:15 |
| Sarah Grebing, Bernhard Beckert and Florian Böhl | Towards Evaluating the Usability of Interactive Theorem Provers | ARW-DT | | Jul 23 16:30 |
| Markus Bender | Combined Reasoning with Sets and Aggregation Functions | ARW-DT | | Jul 23 17:00 |
| Marco B. Caminati, Manfred Kerber, Christoph Lange and Colin Rowat | Reasoning about Auctions | ARW-DT | | Jul 23 12:15 |
| Dennis Felsing, Sarah Grebing, Vladimir Klebanov and Mattias Ulbrich | Automating Regression Verification | ARW-DT | | Jul 23 12:45 |
| Claudia Schon, Ulrich Furbach and Frieder Stolzenburg | Automated Reasoning in Deontic Logic | ARW-DT | | Jul 24 11:15 |
| Matthias Horbach and Viorica Sofronie-Stokkermans | Modular Verification of Interconnected Families of Uniform Linear Hybrid Automata | ARW-DT | | Jul 24 17:30 |
| Mark Judge | (AI) Planning to Reconfigure your Robot? | ARW-DT | | Jul 24 11:45 |
| Mark Judge | Using CSP Meta Variables in AI Planning | ARW-DT | | Jul 24 10:45 |
| Patrick Koopmann and Renate A. Schmidt | Computing Uniform Interpolants of ALCH-Ontologies with Background Knowledge | ARW-DT | | Jul 24 15:30 |
| Alexander Lyaletski | On Herbrand theorems for classical and non-classical logics | ARW-DT | | Jul 24 12:45 |
| Norbert Manthey | Extended Resolution in Modern SAT Solving | ARW-DT | | Jul 24 09:45 |
| Cláudia Nalon and George Bezerra Silva | A Resolution-Based Prover for Normal Modal Logics | ARW-DT | | Jul 24 15:00 |
| Fabio Papacchini and Renate A. Schmidt | Models Minimal Modulo Subset-Simulation for Expressive Propositional Modal Logics | ARW-DT | | Jul 24 14:30 |
| John Stell, Renate A. Schmidt and David Rydeheard | Tableau Development for a Bi-Intuitionistic Tense Logic | ARW-DT | | Jul 23 17:30 |
| Alexander Bolotov, Vasilyi Shangin, Oleg Grigoriev and Mariusz Urbanski | Socratic Proofs for Propositional Linear-Time Logic | ARW-DT | | Jul 24 17:00 |
| Christoph Wernhard | Second-Order Characterizations of Definientia in Formula Classes | ARW-DT | | Jul 24 12:15 |
| Max Wisniewski, Alexander Steen and Christoph Benzmüller | The Leo-III Project | ARW-DT | | Jul 24 16:30 |
| Uwe Egly | On the Relation between Resolution Calculi for QBFs and First-order Formulas | QBF | | Jul 13 10:45 |
| Valeriy Balabanov, Jie-Hong Roland Jiang, Mikoláš Janota and Magdalena Widl | Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs | QBF | | Jul 13 11:45 |
| Ankush Desai, Pranav Garg and P. Madhusudan | A new reduction for event-driven distributed programs | EC2 | | Jul 18 11:45 |
| Azadeh Farzan, Andreas Holzer, Niloofar Razavi and Helmut Veith | Concolic Testing of Concurrent Programs | EC2 | | Jul 17 09:45 |
| Felix Hargreaves, Daniel Merkle and Peter Schneider-Kamp | Group Communication Patterns for High Performance Computing in Scala | EC2 | | Jul 17 15:30 |
| Sidi Mohamed Beillahi, Umair Siddique and Sofiene Tahar | Towards the Application of Formal Methods in Process Engineering | FWFM | | Jul 13 14:30 |
| Tomer Kotek | Explaining the decompositionality of MSO using applications to combinatorics | FWFM | | Jul 13 12:30 |
| David Lawrence, Dimitri Racordon, Maximilien Colange, Steve Hostettler, Alban Linard, Edmundo López Bóbeda, Alexis Marechal, Matteo Risoldi, Nicolas Sedlmajer and Didier Buchs | Introducing Formal Verification with Lego | FWFM | | Jul 13 12:00 |
| Heather Logas, Florent Kirchner, John Murray, Martin Schäf and Jim Whitehead | Chekofv: Crowd-sourced Formal Verification | FWFM | | Jul 13 11:00 |
| Pratima K. Shah | An Example Demonstrating the Requirement of Fully Formal Verification Method | FWFM | | Jul 13 15:00 |
| Nikolay Shilov | Using Esoteric Language for Teaching Formal Semantics | FWFM | | Jul 13 11:30 |
| Lynne Coventry | Tackling the Awareness-Behaviour Divide in Security: (step 1) Understand the User | STAST | | Jul 18 09:00 |
| Debora Jeske, Lynne Coventry and Pam Briggs | Decision justifications for wireless network selection | STAST | | Jul 18 10:45 |
| Oliver Buckley, Jason Nurse, Philip Legg, Michael Goldsmith and Sadie Creese | Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat | STAST | | Jul 18 11:30 |
| Taciane Martimiano, Jean Everson Martina, Maina Olembo and Marcelo Carlos | Modelling User Devices in Security Ceremonies | STAST | | Jul 18 12:15 |
| Sven Uebelacker and Susanne Quiel | The Social Engineering Personality Framework | STAST | | Jul 18 14:30 |
| Jaap Boender, Marieta Georgieva Ivanova, Florian Kammueller and Giuseppe Primiero | Modeling Human Behaviour with Higher Order Logic: Insider Threats | STAST | | Jul 18 15:15 |
| Sven Kiljan, Harald Vranken and Marko van Eekelen | What You Enter Is What You Sign: input integrity in an online banking environment | STAST | | Jul 18 16:30 |
| Lydia Kraus, Ina Wechsung and Sebastian Möller | Using Statistical Information to Communicate Android Permission Risks to Users | STAST | | Jul 18 17:15 |
| Ian Mackie | Numeral Systems in the Lambda Calculus | TermGraph | | Jul 13 09:15 |
| Samuel Mimram | An Introduction to Higher-Dimensional Rewriting Theory | TermGraph | | Jul 13 14:30 |
| Susumu Yamasaki | Fixed Point Theory for Consistent Rewriting in Logic of Action with Reverse | TermGraph | | Jul 13 17:00 |
| Sergio Antoy, Jacob Johannsen and Steven Libby | Needed Computations Shortcutting Needed Steps | TermGraph | | Jul 13 10:45 |
| Giulio Guerrieri, Luc Pellissier and Lorenzo Tortora De Falco | Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion | TermGraph | | Jul 13 15:30 |
| Naohi Eguchi | Proving Termination of Unfolding Graph Rewriting for General Safe Recursion | TermGraph | | Jul 13 11:15 |
| Clemens Grabmayer and Vincent van Oostrom | Nested Term Graphs | TermGraph | | Jul 13 11:45 |
| Ian Mackie and Shinya Sato | An Implementation Model for Interaction Nets | TermGraph | | Jul 13 16:30 |
| Tim Kelly and Ibrahim Habli | Balancing the Formal and Informal in Safety Case Arguments | VeriSure | | Jul 23 08:45 |
| Stephan Arlt, John Murray, Philipp Ruemmer and Martin Schäf | Quantification of Verification Progress | VeriSure | | Jul 23 09:15 |
| Hardi Hungar and Michael Meyer Zu Hörste | Introducing Semi-Formal Specifications into a Distributed Development Process | VeriSure | | Jul 23 10:45 |
| Kedar Namjoshi | Witnessing an SSA Transformation | VeriSure | | Jul 23 11:15 |
| Paul Curzon, Paolo Masci, Patrick Oladimeji, Rimvydas Rukšėnas, Harold Thimbleby and Enrico D'Urso | Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project | VeriSure | | Jul 23 12:15 |
| Freek Verbeek, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum and Oto Havle | Implicit Assumptions in a Model for Separation Kernels | VeriSure | | Jul 23 14:30 |
| Constance Heitmeyer | Assurance and Verification of Security Properties | VeriSure | | Jul 23 15:00 |
| Sebastian Nielebock, Tim Gonschorek and Frank Ortmeier | A Graphical Notation for Probabilistic Specifications | VeriSure | | Jul 23 16:30 |
| Sergey Frenkel | Assurance of some system reliability characteristics in formal design verification | VeriSure | | Jul 23 17:00 |
| Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian Emmes and Carsten Fuhs | Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs | CICLOPS-WLPE | | Jul 18 14:30 |
| Michael Codish, Luís Cruz-Filipe, Michael Frank and Peter Schneider-Kamp | Proofs for Optimality of Sorting Networks by Logic Programming | CICLOPS-WLPE | | Jul 17 08:45 |
| Joachim Jansen and Gerda Janssens | Refining definitions with unknown opens using XSB for IDP3 | CICLOPS-WLPE | | Jul 17 10:45 |
| Alexei A. Morozov and Alexander F. Polupanov | Intelligent Visual Surveillance Logic Programming: Implementation Issues | CICLOPS-WLPE | | Jul 18 16:30 |
| Vincent Bloemen, Daniel Diaz, Machiel van der Bijl and Salvador Abreu | Extending the Finite Domain Solver of GNU Prolog | CICLOPS-WLPE | | Jul 17 14:30 |
| Gopalan Nadathur and Mary Southern | A Lambda Prolog Based Animation of Twelf Specifications | CICLOPS-WLPE | | Jul 17 11:15 |
| Jose F. Morales and Manuel V. Hermenegildo | Towards Pre-Indexed Terms | CICLOPS-WLPE | | Jul 17 12:15 |
| Md Solimul Chowdhury and Jia-Huai You | A System for Embedding Global Constraints into SAT | CICLOPS-WLPE | | Jul 17 11:45 |
| Jan Wielemaker | SWI-Prolog version 7 extensions | CICLOPS-WLPE | | Jul 17 15:00 |
| Flavio Cruz, Ricardo Rocha and Seth Goldstein | A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs | CICLOPS-WLPE | | Jul 18 17:00 |
| Theofrastos Mantadelis and Ricardo Rocha | A Portable Prolog Predicate for Printing Rational Terms | CICLOPS-WLPE | | Jul 17 15:30 |
| Luca Cardelli | Morphisms of reaction networks that couple structure to function | VEMDP | | Jul 17 14:30 |
| Masami Hagiya | Molecular computers for molecular robots as hybrid systems | VEMDP | | Jul 17 10:45 |
| Andrew Phillips | Computational design of DNA strand displacement systems | VEMDP | | Jul 17 09:00 |
| Vincent Danos | Formal mean field theories for graph rewriting | VEMDP | | Jul 17 16:55 |
| Aadithya V. Karthik | NINJA: Boolean Modelling and Formal Verification of Tiered-Rate Chemical Reaction Networks | VEMDP | | Jul 17 16:30 |
| Jean Krivine | Rule-Based modeling of DNA repair | VEMDP | | Jul 17 17:20 |
| Lulu Qian | DNA-based circuits in well-mixed and spatially-organized systems | VEMDP | | Jul 17 11:40 |
| Philip Boeing | An Aspect Oriented Design and Modelling Framework for Synthetic Biology | VEMDP | | Jul 17 17:45 |
| Neil Dalchau | Software tools for analysing the chemical master equation | VEMDP | | Jul 17 17:45 |
| Frits Dannenberg | Guiding the development of DNA walker systems to guarantee reliability and performance | VEMDP | | Jul 17 17:45 |
| Casey Grun | DyNAMiC Workbench: Automated design and verification of dynamic DNA nanosystems | VEMDP | | Jul 17 17:45 |
| Paolo Milazzo | Identification of Components and Modular Verification of Biochemical Pathways | VEMDP | | Jul 17 17:45 |
| Savas Konur, Christophe Ladroue, Harold Fellermann, Daven Sanassy, Laurentiu Mierla, Florentin Ipate, Sara Kalvala, Marian Gheorghe and Natalio Krasnogor | Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench | VEMDP | | Jul 17 12:35 |
| Casey Grun, Karthik Sarma, Brian Wolfe, Seung Woo Shin and Erik Winfree | A domain-level DNA strand displacement reaction enumerator allowing arbitrary non-pseudoknotted secondary structures | VEMDP | | Jul 17 09:50 |
| Seung Woo Shin, Chris Thachuk and Erik Winfree | Verifying CRN Implementations: A Pathway Decomposition Approach | VEMDP | | Jul 17 15:20 |
| Robert F. Johnson and Erik Winfree | Verifying Polymer Reaction Networks using Bisimulation | VEMDP | | Jul 17 12:10 |
| Geoff Sutcliffe | The TPTP Process Instruction Language, with Applications | UITP | | Jul 17 09:15 |
| Enrico Tassi | Asynchronous Processing of Formal Documents in Coq | UITP | | Jul 17 14:30 |
| Andrew Butterfield | UTP2: Higher-Order Equational Reasoning by Pointing | UITP | | Jul 17 17:30 |
| Sarah Grebing, Bernhard Beckert and Florian Böhl | How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers | UITP | | Jul 17 11:15 |
| Gudmund Grov, Aleks Kissinger and Yuhui Lin | Tinker, tailor, solver, proof | UITP | | Jul 17 10:45 |
| Tomer Libal, Martin Riener and Mikheil Rukhaia | Advanced Proof Viewing in PROOFTOOL | UITP | | Jul 17 11:45 |
| Florian Rabe | A Logic-Independent IDE | UITP | | Jul 17 17:00 |
| Christian Sternagel and René Thiemann | The Certification Problem Format | UITP | | Jul 17 12:15 |
| Carst Tankink | PIDE for Asynchronous Interaction with Coq | UITP | | Jul 17 15:30 |
| Makarius Wenzel | System description: Isabelle/jEdit in 2014 | UITP | | Jul 17 16:30 |
| Tommaso Dreossi, Thao Dang and Carla Piazza | Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models | HSB | | Jul 23 15:30 |
| Anatoly Sorokin, Oksana Sorokina and J. Douglas Armstrong | RKappa: Statistical sampling suite for Kappa models. | HSB | | Jul 24 14:55 |
| Alvis Brazma, Karlis Cerans, Dace Ruklisa, Thomas Schlitt and Juris Viksna | Modeling and analysis of qualitative behavior of gene regulatory networks | HSB | | Jul 24 09:45 |
| Claudio Angione, Ezio Bartocci, Luca Bortolussi, Pietro Lio', Annalisa Occhipinti and Guido Sanguinetti | Bayesian Design for Whole Cell Synthetic Biology Models | HSB | | Jul 24 14:30 |
| Alexandre Rocca, Thao Dang and Eric Fanchon | Exploiting the eigenstructures of linear systems to speed up reachability computation | HSB | | Jul 24 12:30 |
| David C Sterratt, Oksana Sorokina and J Douglas Armstrong | Integration of rule-based models and compartmental models of neurons | HSB | | Jul 24 11:30 |
| Charalampos Kyriakopoulos and Verena Wolf | Optimal Observation Time Points in Stochastic Chemical Kinetics | HSB | | Jul 24 12:00 |
| Donal Stewart, Stephen Gilmore and Michael Cousin | FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference | HSB | | Jul 23 09:45 |
| Vernon Asuncion, Yan Zhang and Heng Zhang | Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness | KR | | Jul 24 10:45 |
| Angelos Charalambidis and Panos Rondogiannis | Constructive Negation in Extensional Higher-Order Logic Programming | KR | | Jul 24 11:15 |
| Marc Denecker and Joost Vennekens | The Well-Founded Semantics Is the Principle of Inductive Definition, Revisited | KR | | Jul 24 11:45 |
| Amelia Harrison, Vladimir Lifschitz and Fangkai Yang | The Semantics of Gringo and Infinitary Propositional Formulas | KR | | Jul 24 12:15 |
| Federico Cerutti, Massimiliano Giacomin, Mauro Vallati and Marina Zanella | An SCC Recursive Meta-Algorithm for Computing Preferred Labellings in Abstract Argumentation | KR | | Jul 21 11:45 |
| Sylvie Coste-Marquis, Sébastien Konieczny, Jean-Guy Mailly and Pierre Marquis | On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses | KR | | Jul 21 11:15 |
| Sylvie Doutre, Andreas Herzig and Laurent Perrussel | A Dynamic Logic Framework for Abstract Argumentation | KR | | Jul 21 12:15 |
| Paul E. Dunne, Wolfgang Dvořák, Thomas Linsbichler and Stefan Woltran | Characteristics of Multiple Viewpoints in Abstract Argumentation | KR | | Jul 21 10:45 |
| Ronald De Haan and Stefan Szeider | The Parameterized Complexity of Reasoning Problems Beyond NP | KR | | Jul 22 15:30 |
| Igor Razgon | On OBDDs for CNFs of Bounded Treewidth | KR | | Jul 21 16:30 |
| Hannes Strass and Johannes Peter Wallner | Analyzing the Computational Complexity of Abstract Dialectical Frameworks via Approximation Fixpoint Theory | KR | | Jul 22 15:00 |
| Guy Van den Broeck, Wannes Meert and Adnan Darwiche | Skolemization for Weighted First-Order Model Counting | KR | | Jul 22 14:30 |
| Patricia Everaere, Sébastien Konieczny and Pierre Marquis | On Egalitarian Belief Merging | KR | | Jul 21 15:00 |
| Davide Grossi and Wiebe Van Der Hoek | Justified Beliefs by Justified Arguments | KR | | Jul 22 11:15 |
| Andreas Herzig | Belief Change Operations: A Short History of Nearly Everything, Told in Dynamic Logic of Propositional Assignments | KR | | Jul 22 11:45 |
| Mehrdad Oveisi, James P. Delgrande, Francis Jeffry Pelletier and Fred Popowich | Belief Change and Base Dependence | KR | | Jul 22 10:45 |
| Pavlos Peppas and Mary-Anne Williams | Belief Change and Semiorders | KR | | Jul 21 14:30 |
| Claus-Peter Wirth and Frieder Stolzenburg | David Poole’s Specificity Revised | KR | | Jul 21 15:30 |
| Adam Bjorndahl, Joseph Halpern and Rafael Pass | Axiomatizing Rationality | KR | | Jul 24 11:45 |
| Alexander Bochman | Dynamic Causal Calculus | KR | | Jul 24 10:45 |
| Joseph Halpern | Appropriate Causal Models and Stability of Causation | KR | | Jul 24 11:15 |
| Egor Ianovski and Luke Ong | GuaranteeNash for Boolean games is NEXP-hard | KR | | Jul 24 12:15 |
| Meghyn Bienvenu, Diego Calvanese, Magdalena Ortiz and Mantas Simkus | Nested Regular Path Queries in Description Logics | KR | | Jul 21 11:15 |
| Stefan Borgwardt, Felix Distel and Rafael Peñaloza | Decidable Gödel Description Logics without the Finitely-Valued Model Property | KR | | Jul 23 12:15 |
| Elena Botoeva, Roman Kontchakov, Vladislav Ryzhikov, Frank Wolter and Michael Zakharyaschev | Query Inseparability for Description Logic Knowledge Bases | KR | | Jul 21 11:45 |
| Andreas Ecke, Rafael Peñaloza and Anni-Yasmin Turhan | Answering Instance Queries Relaxed by Concept Similarity | KR | | Jul 21 12:15 |
| Georg Gottlob, André Hernich, Clemens Kupke and Thomas Lukasiewicz | Stable Model Semantics for Guarded Existential Rules and Description Logics | KR | | Jul 23 10:45 |
| Georg Gottlob, Marco Manna and Andreas Pieris | Polynomial Combined Rewritings for Existential Rules | KR | | Jul 21 10:45 |
| Víctor Gutiérrez Basulto, Jean Christoph Jung and Thomas Schneider | Lightweight Description Logics and Branching Time: a Troublesome Marriage | KR | | Jul 22 11:45 |
| Yazmin Ibanez-Garcia, Carsten Lutz and Thomas Schneider | Finite Model Reasoning in Horn Description Logics | KR | | Jul 22 11:15 |
| Boris Konev, Carsten Lutz, Ana Ozaki Rivera Castillo and Frank Wolter | Exact Learning of Lightweight Description Logic Ontologies | KR | | Jul 22 10:45 |
| Markus Krötzsch and Sebastian Rudolph | Nominal Schemas in Description Logics: Complexities Clarified | KR | | Jul 23 11:45 |
| Michel Ludwig and Boris Konev | Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference | KR | | Jul 23 11:15 |
| Leonid Libkin | Certain Answers as Objects and Knowledge | KR | | Jul 23 14:30 |
| Fangzhen Lin | A Formalization of Programs in First-Order Logic with a Discrete Linear Order | KR | | Jul 23 17:00 |
| Loizos Michael | Simultaneous Learning and Prediction | KR | | Jul 23 15:30 |
| Peter Schüller | Tackling Winograd Schemas by Formalizing Relevance Theory in Knowledge Graphs | KR | | Jul 23 15:00 |
| Shahab Tasharrofi and Eugenia Ternovska | Generalized Multi-Context Systems | KR | | Jul 21 16:30 |
| Peng Zhang and Jochen Renz | Qualitative Spatial Representation and Reasoning in Angry Bird: the Extended Rectangle Algebra | KR | | Jul 21 17:00 |
| Jorge Baier, Brent Mombourquette and Sheila McIlraith | Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals | KR | | Jul 23 16:30 |
| Francesco Belardinelli | Satisfiability of Alternating-Time Temporal Epistemic Logic through Tableaux | KR | | Jul 23 17:30 |
| Julian Gutierrez, Paul Harrenstein and Michael Wooldridge | Reasoning about Equilibria in Game-Like Concurrent Systems | KR | | Jul 21 15:00 |
| Xiaowei Huang and Ron Van Der Meyden | A Temporal Logic of Strategic Knowledge | KR | | Jul 21 15:30 |
| Alessio Lomuscio and Jakub Michaliszyn | An Abstraction Technique for the Verification of Multi-Agent Systems against ATL Specifications | KR | | Jul 21 14:30 |
| Vaishak Belle and Hector Levesque | How To Progress Beliefs in Continuous Domains | KR | | Jul 23 11:15 |
| Christopher Ewin, Adrian Pearce and Stavros Vassos | Transforming Situation Calculus Action Theories for Optimised Reasoning | KR | | Jul 23 11:45 |
| Babak Bagheri Hariri, Diego Calvanese, Alin Deutsch and Marco Montali | State-Boundedness in Data-Aware Dynamic Systems | KR | | Jul 22 15:30 |
| Gerhard Lakemeyer and Hector J. Levesque | Decidable Reasoning in a Fragment of the Epistemic Situation Calculus | KR | | Jul 22 14:30 |
| Fangzhen Lin | A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations | KR | | Jul 23 10:45 |
| Alessio Lomuscio and Jakub Michaliszyn | Model Checking Unbounded Artifact-Centric Systems | KR | | Jul 22 15:00 |
| David Rajaratnam, Hector Levesque, Maurice Pagnucco and Michael Thielscher | Forgetting in Action | KR | | Jul 23 12:15 |
| Mehul Bhatt, Carl Schultz and Madhura Thosar | Computing Narratives of Cognitive User Experience for Building Design Analysis: KR for Industry Scale Computer Aided Architecture Design | KR | | Jul 23 14:30 |
| Andrea Marrella, Massimo Mecella and Sebastian Sardina | SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical Planning | KR | | Jul 23 15:30 |
| Matthias Thimm | Tweety: A Comprehensive Collection of Java Libraries for Logical Aspects of Artificial Intelligence and Knowledge Representation | KR | | Jul 23 15:00 |
| Salem Benferhat and Karim Tabia | Reasoning with Uncertain Inputs in Possibilistic Networks | KR | | Jul 23 17:00 |
| Seyed Mehran Kazemi, David Buchman, Kristian Kersting, Sriraam Natarajan and David Poole | Relational Logistic Regression | KR | | Jul 23 17:30 |
| Doga Kisa, Guy Van den Broeck, Arthur Choi and Adnan Darwiche | Probabilistic Sentential Decision Diagrams | KR | | Jul 21 17:00 |
| Nico Potyka | Linear Programs for Measuring Inconsistency in Probabilistic Logics | KR | | Jul 23 16:30 |
| Guillaume Aucher | Axioms .2 and .4 as Interaction Axioms | KR | | Jul 22 12:50 |
| Michael Bartholomew and Joohyung Lee | Stable Models of Multi-Valued Formulas: Partial versus Total Functions | KR | | Jul 22 13:00 |
| Wouter Beek, Stefan Schlobach and Frank van Harmelen | Rough Set Semantics for Identity on the Web | KR | | Jul 21 12:45 |
| Vaishak Belle and Gerhard Lakemeyer | On the Progression of Knowledge in Multiagent Systems | KR | | Jul 22 12:25 |
| Richard Booth, Edmond Awad and Iyad Rahwan | Interval Methods for Judgment Aggregation in Argumentation | KR | | Jul 21 12:45 |
| Pedro Cabalar and Martín Diéguez | Strong Equivalence of Non-Monotonic Temporal Theories | KR | | Jul 22 12:20 |
| Sofie De Clercq, Kim Bauters, Steven Schockaert, Martine De Cock and Ann Nowé | Using Answer Set Programming for Solving Boolean Games | KR | | Jul 22 12:50 |
| James Delgrande | Toward a Knowledge Level Analysis of Forgetting | KR | | Jul 22 12:35 |
| Irene-Anna Diakidoy, Antonis Kakas, Loizos Michael and Rob Miller | A Psychology-Inspired Approach to Automated Narrative Text Comprehension | KR | | Jul 21 12:55 |
| Felix Distel, Jamal Atif and Isabelle Bloch | Concept Dissimilarity with Triangle Inequality | KR | | Jul 21 12:55 |
| Matt Duckham, Sanjiang Li, Weiming Liu and Zhiguo Long | On Redundant Topological Constraints (Extended Abstract) | KR | | Jul 22 12:15 |
| Valmi Dufour-Lussier, Alice Hermann, Florence Le Ber and Jean Lieber | Belief Revision in the Propositional Closure of a Qualitative Algebra | KR | | Jul 22 12:25 |
| Sjur Kristoffer Dyrkolbotn | How to Argue for Anything: Enforcing Arbitrary Sets of Labellings using AFs | KR | | Jul 21 12:50 |
| Valeria Fionda, Claudio Gutierrez and Giuseppe Pirró | Knowledge Maps of Web Graphs | KR | | Jul 22 12:20 |
| Martin Gebser, Tomi Janhunen and Jussi Rintanen | ASP Encodings of Acyclicity Properties | KR | | Jul 22 12:55 |
| Codruta Girlea, Eyal Amir and Roxana Girju | Tracking Beliefs and Intentions in the Werewolf Game | KR | | Jul 22 12:45 |
| Leora Morgenstern | Representing and Reasoning About Time Travel Narratives: Foundational Concepts | KR | | Jul 22 12:40 |
| Xavier Parent and Leon van der Torre | Aggregative Deontic Detachment for Normative Reasoning | KR | | Jul 22 12:55 |
| Fabio Patrizi and Stavros Vassos | Action Theories over Generalized Databases with Equality Constraints (Extended Abstract) | KR | | Jul 22 12:35 |
| Luis Moniz Pereira, Emmanuelle-Anna Dietz and Steffen Hölldobler | An Abductive Reasoning Approach to the Belief-Bias Effect | KR | | Jul 22 12:40 |
| Márcio Ribeiro and Renata Wassermann | Minimal Change in AGM Revision for Non-Classical Logics | KR | | Jul 22 12:30 |
| Viachaslau Sazonau, Uli Sattler and Gavin Brown | Predicting Performance of OWL Reasoners: Locally or Globally? | KR | | Jul 21 12:50 |
| Yuping Shen and Xishun Zhao | Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas | KR | | Jul 22 12:45 |
| Andreas Sideris and Yannis Dimopoulos | Heuristic Guided Optimization for Propositional Planning | KR | | Jul 22 12:30 |
| Yi Zhou | First-Order Default Logic Revisited | KR | | Jul 22 12:15 |
| Franz Baader | Ontology-Based Monitoring of Dynamic Systems | KR | | |
| Georg Gottlob, Thomas Lukasiewicz and Andreas Pieris | Datalog+/–: Questions and Answers | KR | | Jul 24 09:00 |
| Alejandro Arbelaez, Deepak Mehta, Barry O'Sullivan and Luis Quesada | A Constraint-based Parallel Local Search for Disjoint Rooted Distance-Constrained Minimum Spanning Tree Problem | ParSearchOpt | | Jul 18 12:15 |
| Alejandro Arbelaez, Charlotte Truchet and Philippe Codognet | On the Parallelization of Randomized Propagation-based Constraint Solving | ParSearchOpt | | Jul 18 11:45 |
| Salvador Abreu, Danny Munera and Daniel Diaz | Towards a Parallel Hierarchical Adaptive Solver Tool | ParSearchOpt | | Jul 18 11:15 |
| Federico Campeotto, Alessandro Dal Palù, Agostino Dovier, Ferdinando Fioretto and Enrico Pontelli | Towards a complete constraint solver on GPU | ParSearchOpt | | Jul 18 15:30 |
| Long Guo, Said Jabbour, Jerry Lonlac and Lakhdar Sais | A Portfolio Based Parallel SAT Solver with Multiple Deletion Strategies | ParSearchOpt | | Jul 18 10:45 |
| Michele Basaldella | Infinitary Classical Logic: Recursive Equations and Interactive Semantics | CLC | | Jul 13 14:30 |
| Emmanuel Beffara | A proof-theoretic view on scheduling in concurrency | CLC | | Jul 13 11:30 |
| David Cerna and Alexander Leitsch | Cut-Elimination in Schematic Proofs and Herbrand Sequents | CLC | | Jul 13 15:20 |
| Harley Eades Iii, Aaron Stump and Ryan McCleeary | Dualized Type Theory | CLC | | Jul 13 11:10 |
| José Espírito Santo, Ralph Matthes, Koji Nakazawa and Luís Pinto | Confluence for classical logic through the distinction between values and computations | CLC | | Jul 13 12:30 |
| Herman Geuvers, Wouter Geraedts, Bram Geron and Judith van Stegeren | A type system for Continuation Calculus | CLC | | Jul 13 12:00 |
| Dominic Hughes | Separable Sequent Calculus for First-order Classical Logic (Work in Progress) | CLC | | Jul 13 15:00 |
| Kentaro Kikuchi and Takafumi Sakurai | A Translation of Intersection and Union Types for the lambda-mu Calculus | CLC | | Jul 13 10:50 |
| Bassel Mannaa and Thierry Coquand | A sheaf model of the algebraic closure | CLC | | Jul 13 16:30 |
| Koji Nakazawa | Extensional Models of Typed Lambda-mu Calculus | CLC | | Jul 13 10:00 |
| Matthieu Perrinel | Stratified Nested Linear Logic | CLC | | Jul 13 15:40 |
| Steffen van Bakel and Maria Grazia Vigliotti | A fully-abstract semantics of lambda-mu in the pi-calculus | CLC | | |
| Jeremy Avigad, Johannes Hölzl and Luke Serafin | A formally verified proof of the Central Limit Theorem | Isabelle | | Jul 13 08:45 |
| Holger Blasum, Oto Havle, Bruno Langenstein, Yakoub Nemouchi, Julien Schmaltz, Werner Stephan, Sergey Tverdyshev, Freek Verbeek and Burkhart Wolff | Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract) | Isabelle | | Jul 13 16:30 |
| Florian Haftmann, Andreas Lochbihler and Wolfgang Schreiner | Towards abstract and executable multivariate polynomials in Isabelle | Isabelle | | Jul 13 11:45 |
| Ondřej Kunčar and Andrei Popescu | From types to sets in Isabelle/HOL | Isabelle | | Jul 13 11:20 |
| Peter Lammich | The CAVA Automata Library | Isabelle | | Jul 13 10:55 |
| Andreas Lochbihler and Marc Züst | Programming TLS in Isabelle/HOL | Isabelle | | Jul 13 15:30 |
| Tobias Nipkow | Amortized Complexity Verified | Isabelle | | Jul 13 17:40 |
| Lars Noschinski | Towards Structured Proofs for Program Verification (Ongoing Work) | Isabelle | | Jul 13 17:20 |
| Lars Noschinski and Christoph Traut | Pattern-based Subterm Selection In Isabelle | Isabelle | | Jul 13 09:45 |
| Lorenz Panny, Jasmin Christian Blanchette and Dmitriy Traytel | Primitively (Co)recursive Definitions for Isabelle/HOL | Isabelle | | Jul 13 09:15 |
| Lawrence Paulson | Proving Gödel’s Incompleteness Theorems | Isabelle | | Jul 13 14:30 |
| Christine Rizkallah | A Simpl Shortest Path Checker Verification | Isabelle | | Jul 13 17:00 |
| Makarius Wenzel | Isabelle/jEdit NEWS | Isabelle | | Jul 13 15:00 |
| Martin Avanzini and Bertram Felgenhauer | Type Introduction for Runtime Complexity Analysis | WST | | Jul 17 15:30 |
| Alexander Bau, Rene Thiemann and Johannes Waldmann | Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling | WST | | Jul 18 11:45 |
| Byron Cook, Heidy Khlaaf and Nir Piterman | Abstract: Fairness for Infinite-State Systems | WST | | Jul 18 08:45 |
| Byron Cook, Stephen Magill, Matthew Parkinson and Thomas Stroeder | Reducing Deadlock and Livelock Freedom to Termination | WST | | Jul 18 09:15 |
| Nachum Dershowitz | Another Proof for the Recursive Path Ordering | WST | | Jul 18 15:30 |
| Joerg Endrullis and Hans Zantema | Non-termination using Regular Languages | WST | | Jul 17 09:45 |
| Alfons Geser | A Solution to Endrullis-08 and Similar Problems | WST | | Jul 18 12:15 |
| Alfons Geser | Kurth's Criterion H Revisited | WST | | Jul 18 15:00 |
| Lars Hellström | Ordering Networks | WST | | Jul 17 16:30 |
| Dieter Hofbauer | On the derivational complexity of Kachinuki orderings | WST | | Jul 18 14:30 |
| Jeroen Ketema and Alastair Donaldson | Automatic Termination Analysis for GPU Kernels | WST | | Jul 17 12:15 |
| Jan Leike and Matthias Heizmann | Geometric Series as Nontermination Arguments for Linear Lasso Programs | WST | | Jul 17 09:15 |
| Naoki Nishida and Takumi Kataoka | On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants | WST | | Jul 17 11:45 |
| Étienne Payet and Fred Mesnard | Non-termination of Dalvik bytecode via compilation to CLP | WST | | Jul 17 08:45 |
| Norbert Preining, Kazuhiro Ogata and Kokichi Futatsugi | Specifying and verifying liveness properties of QLOCK in CafeOBJ | WST | | Jul 18 09:45 |
| Raphael Rodrigues, Péricles Alves, Fernando Pereira and Laure Gonnord | Real-world loops are easy to predict : a case study | WST | | Jul 17 15:00 |
| Haruhiko Sato and Sarah Winkler | A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion | WST | | Jul 18 11:15 |
| Caterina Urban and Antoine Miné | To Infinity... and Beyond! | WST | | Jul 17 14:30 |
| Harald Zankl, Sarah Winkler and Aart Middeldorp | Automating Elementary Interpretations | WST | | Jul 18 10:45 |
| Slimane Abou-Msabah | An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem | RCRA | | Jul 18 12:40 |
| Mario Alviano, Bernardo Cuteri and Francesco Ricca | Declarative Specification of Benchmark Sessions via ASP | RCRA | | Jul 17 12:40 |
| Kerstin Bunte, Matti Järvisalo, Jeremias Berg, Petri Myllymäki, Jaakko Peltonen and Samuel Kaski | Optimal Neighborhood Preserving Visualization by Maximum Satisfiability | RCRA | | Jul 17 10:50 |
| Esra Erdem, Volkan Patoglu and Peter Schüller | A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks | RCRA | | Jul 17 14:30 |
| Eugene Freuder, Diarmuid Grimes and Richard Wallace | Dispensable Instantiations in Constraint Satisfaction Problems | RCRA | | Jul 18 09:45 |
| Alexey Ignatiev, Antonio Morgado, Jordi Planes and Joao Marques-Silva | Maximal Falsifiability: Definitions, Algorithms, and Applications | RCRA | | Jul 17 11:20 |
| Amroun Kamal, Habbas Zineb and Aggoune-Mtalaa Wassila | A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary CSP | RCRA | | Jul 18 09:15 |
| Luca Mancini, Alfredo Milani, Valentina Poggioni and Andrea Chiancone | Self Regulating Mechanisms for Network Immunization | RCRA | | Jul 18 12:20 |
| Shashank Pathak, Luca Pulina and Armando Tacchella | Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies | RCRA | | Jul 18 11:50 |
| Regis Riveret, Pascal Caianiello, Stefania Constantini and Moez Draief | Concept Learning by a Monte-Carlo Tree Search of Argumentations | RCRA | | Jul 18 11:20 |
| Valentino Santucci, Marco Baioletti and Alfedo Milani | A Discrete Differential Evolution Algorithm for the Total Flowtime Flowshop Scheduling Problem | RCRA | | Jul 17 15:00 |
| Ilias Tachmazidis, Grigoris Antoniou and Wolfgang Faber | Efficient Computation of the Well-Founded Semantics over Big Data | RCRA | | Jul 17 12:10 |
| Richard Wallace | Neighbourhood SAC for Preprocessing and Search | RCRA | | Jul 18 10:45 |
| Hans Zantema | Latin Squares with Graph Properties | RCRA | | Jul 17 11:50 |
| Albert Atserias | Weak Pigeonhole Principles, Circuits for Approximate Counting, and Bounded-Depth Proofs | PC | | Jul 13 10:45 |
| Fu Li and Iddo Tzameret | Generating Matrix Identities and Hard Instances for Strong Proof Systems | PC | | Jul 13 14:30 |
| Jakob Nordström | A (Biased) Survey of Space Complexity and Time-Space Trade-offs in Proof Complexity | PC | | Jul 12 14:30 |
| Pavel Pudlák | On Some Conjectures in Proof Complexity | PC | | Jul 12 11:00 |
| James Aisenberg, Maria Bonet and Sam Buss | Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets | PC | | Jul 13 09:15 |
| Albert Atserias, Massimo Lauria and Jakob Nordström | Narrow Proofs May Be Maximally Long | PC | | Jul 13 16:30 |
| Ilario Bonacina, Nicola Galesi and Neil Thapen | Total Space in Resolution | PC | | Jul 13 12:00 |
| Hubie Chen | Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction | PC | | Jul 12 12:30 |
| Anupam Das | $n^{O(\log \log n)}$ size monotone proofs of the weak pigeonhole principle | PC | | Jul 13 09:45 |
| Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström and Marc Vinyals | From Small Space to Small Width in Resolution | PC | | Jul 13 12:30 |
| Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström and Marc Vinyals | Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds | PC | | Jul 12 15:30 |
| Dmitry Itsykson and Dmitry Sokolov | Lower bounds for splittings by linear combinations | PC | | Jul 13 15:30 |
| Emil Jeřábek | Parameter-free induction in bounded arithmetic | PC | | Jul 12 17:00 |
| Jan Johannsen, Massimo Lauria, Jakob Nordstrom and Marc Vinyals | Size-Space Bounds and Trade-offs for CDCL Proofs | PC | | Jul 12 12:00 |
| Ján Pich | Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic | PC | | Jul 12 17:30 |
| Jean-Jose Razafindrakoto and Arnold Beckmann | Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time | PC | | Jul 12 16:30 |
| Neil Thapen, Arnold Beckmann and Pavel Pudlák | Parity games and propositional proofs | PC | | Jul 13 17:00 |
| Joerg Endrullis, Dimitri Hendriks, Jan Willem Klop and Andrew Polonsky | An Introduction to the Clocked Lambda Calculus | WIR | | Jul 12 16:30 |
| Fanny He and Alexis Saurin | From the finite to the transfinite: Λμ-terms and streams. | WIR | | Jul 12 15:00 |
| Stefan Kahrs and Connor Smith | Normal Forms and Infinity | WIR | | |
| Jakob Grue Simonsen | Dynamical systems, attractors and well-behaved infinitary rewriting | WIR | | Jul 12 14:30 |
| Benoît Valiron and Michele Pagani | Work in Progress: Algebraic Abstract Reduction Systems | WIR | | Jul 12 17:00 |
| Hans Zantema | Turtle graphics of morphic streams | WIR | | Jul 12 17:30 |
| Carlos Bobed, Fernando Bobillo, Roberto Yus, Guillermo Esteban and Eduardo Mena | Android Went Semantic: Time for Evaluation | ORE | | Jul 13 12:40 |
| Michel Ludwig | Just: a Tool for Computing Justifications w.r.t. ELH Ontologies | ORE | | Jul 13 12:20 |
| Jean-Rémi Bourguet and Luca Pulina | TROvE: a Graphical Tool to Evaluate OWL Reasoners | ORE | | Jul 13 11:00 |
| José Antonio Minarro-Giménez and Matthias Samwald | An update on Genomic CDS, a complex ontology for pharmacogenomics and clinical decision support | ORE | | Jul 13 14:50 |
| Diego Calvanese, Davide Lanti, Martin Rezk, Mindaugas Slusnys and Guohui Xiao | A Scalable Benchmark for OBDA Systems: Preliminary Report | ORE | | Jul 13 11:40 |
| Michele Ruta, Floriano Scioscia, Giuseppe Loseto, Filippo Gramegna, Saverio Ieva and Eugenio Di Sciascio | Mini-ME 2.0: powering the Semantic Web of Things | ORE | | Jul 13 16:30 |
| Dmitry Tsarkov | Incremental and Persistent Reasoning in FaCT++ | ORE | | Jul 13 16:50 |
| Alexander Kropotin | Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software Development | ORE | | Jul 13 12:00 |
| C. Maria Keet, Claudia D'Amato, Zubeida Khan and Agnieszka Lawrynowicz | Exploring Reasoning with the DMOP Ontology | ORE | | Jul 13 14:30 |
| Thomas Eiter, Patrik Schneider, Mantas Simkus and Guohui Xiao | Using OpenStreetMap Data to Create Benchmarks for Description Logic Reasoners | ORE | | Jul 13 11:20 |
| Robert Stevens, Nicolas Matentzoglu and Uli Sattler | A Family History Knowledge Base in OWL 2 | ORE | | Jul 13 15:10 |
| Riccardo Zese | Reasoning with Probabilistic Logics | ICLP | | Jul 20 12:35 |
| Grzegorz Jaśkiewicz | Logic Programming as Scripting Language for Bots in Computer Games – Research Overview | ICLP | | Jul 20 16:55 |
| Aya Saad | CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty | ICLP | | Jul 20 15:20 |
| Heike Stephan | Application of Methods for Syntax Analysis of Context-Free Languages to Query Evaluation of Logic Programs | ICLP | | Jul 20 14:30 |
| Nada Sharaf, Slim Abdennadher and Thom Fr¨uhwirth | Visualization of Constraint Handling Rules | ICLP | | Jul 20 12:10 |
| Rehan Abdul Aziz | Bound Founded Answer Set Programming | ICLP | | Jul 20 14:55 |
| Joachim Jansen | Model revision inference for extensions of first order logic | ICLP | | Jul 20 16:30 |
| Michael Morak | The Impact of Disjunction on Reasoning under Existential Rules: Research Summary | ICLP | | Jul 20 11:45 |
| Ulrich Berger and Tie Hou | Program extraction in Church's simple theory of types (invited talk) | PSC | | Jul 18 09:15 |
| Henning Basold and Helle Hvid Hansen | Observational Equivalence for Behavioural Differential Equations | PSC | | Jul 17 16:30 |
| Stefano Berardi, Paulo Oliva and Silvia Steila | Effective Bounds on the Podelski-Rybalchenko Termination Theorem | PSC | | Jul 17 15:15 |
| Ulrich Berger, Alison Jones and Monika Seisenberger | Extracting Monadic Parsers from Proofs | PSC | | Jul 18 10:45 |
| Liron Cohen and Robert Constable | Intuitionistic Ancestral Logic | PSC | | Jul 18 11:30 |
| Christian Espindola and Henrik Forssell | Constructive completeness and exploding models | PSC | | Jul 17 10:45 |
| Mauro Ferrari and Camillo Fiorentini | Proof-search in natural deduction calculi for IPL | PSC | | Jul 18 14:30 |
| Herman Geuvers | A typed lambda-calculus with call-by-name and call-by-value iteration | PSC | | Jul 17 14:30 |
| Hugo Herbelin and Danko Ilik | Computing with Gödel’s completeness theorem | PSC | | Jul 17 11:30 |
| Sergey Melikhov | A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic | PSC | | Jul 18 15:15 |
| Tatiana Yavorskaya and Nadezhda Ruhlyadko | Multi-agent justification logic | PSC | | Jul 17 17:15 |
| Andrew Gill | HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell | WPTE | | Jul 13 09:15 |
| William Mansky and Elsa Gunter | Verifying Optimizations for Concurrent Programs | WPTE | | Jul 13 10:45 |
| Masanori Nagashima, Tomofumi Kato, Masahiko Sakai and Naoki Nishida | Inverse Unfold Problem and Its Heuristic Solving | WPTE | | Jul 13 11:15 |
| David Sabel | Structural Rewriting in the Pi-Calculus | WPTE | | Jul 13 12:00 |
| Guillaume Madelaine, Cedric Lhoussaine and Joachim Niehren | Attractor Equivalence: An Observational Semantics for Reaction Networks | WPTE | | Jul 13 12:30 |
| Naoki Nishida, Makishi Yanagisawa and Karl Gmeiner | On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings | WPTE | | Jul 13 14:30 |
| Manfred Schmidt-Schauss and David Sabel | Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report) | WPTE | | Jul 13 15:00 |
| Yuki Chiba | Verifying the Correctness of Tupling Transformations based on Conditional Rewriting | WPTE | | Jul 13 15:30 |
| Karl Gmeiner and Naoki Nishida | Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems | WPTE | | Jul 13 16:30 |
| Georg Moser and Michael Schaper | A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems | WPTE | | Jul 13 17:00 |
| Michael Benedikt | New Perspectives on Query Reformulation | DL | | Jul 17 10:45 |
| Patrick Blackburn | Fragments of Logic, Language, and Computation | DL | | Jul 18 08:45 |
| Alon Halevy | Structured Data on the Web (or, a Personal Journey Away From and Back To Ontologies) | DL | | Jul 19 10:45 |
| Shqiponja Ahmetaj, Diego Calvanese, Magdalena Ortiz and Mantas Simkus | Planning Problems for Graph Structured Data in Description Logics | DL | | Jul 19 18:05 |
| Albin Ahmeti, Diego Calvanese and Axel Polleres | SPARQL Update for Materialized Triple Stores under DL-Lite_RDFS Entailment | DL | | Jul 20 12:00 |
| Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter and Michael Zakharyaschev | Temporal OBDA with LTL and DL-Lite | DL | | Jul 18 12:00 |
| Franz Baader and Barbara Morawska | Matching with respect to general concept inclusions in the Description Logic EL | DL | | Jul 17 17:40 |
| Meghyn Bienvenu, Stanislav Kikot and Vladimir Podolskii | Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries | DL | | Jul 18 17:05 |
| Stefan Borgwardt | Fuzzy DLs over Finite Lattices with Nominals | DL | | Jul 18 14:55 |
| Stefan Borgwardt, José A. Leyva Galano and Rafael Peñaloza | Gödel FL_0 with Greatest Fixed-Point Semantics | DL | | Jul 18 14:30 |
| Elena Botoeva, Roman Kontchakov, Vladislav Ryzhikov, Frank Wolter and Michael Zakharyaschev | Query Inseparability by Games | DL | | Jul 19 14:30 |
| Camille Bourgaux, Meghyn Bienvenu and François Goasdoué | Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics | DL | | Jul 18 11:35 |
| Pierre Bourhis, Michael Morak and Andreas Pieris | Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs | DL | | Jul 17 11:45 |
| Loris Bozzato, Thomas Eiter and Luciano Serafini | Contextualized Knowledge Repositories with Justifiable Exceptions | DL | | Jul 17 18:05 |
| Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith and Florian Zuleger | Shape and Content: Incorporating Domain Knowledge into Shape Analysis | DL | | Jul 17 15:20 |
| David Carral, Cristina Feier, Ana Armas Romero, Bernardo Cuenca-Grau, Pascal Hitzler and Ian Horrocks | Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs | DL | | Jul 17 14:30 |
| Bernardo Cuenca Grau, Evgeny Kharlamov, Egor Kostylev and Dmitriy Zheleznyakov | Controlled Query Evaluation over Lightweight Ontologies | DL | | Jul 20 10:45 |
| Bernardo Cuenca Grau, Evgeny Kharlamov, Dmitriy Zheleznyakov, Marcelo Arenas and Sarunas Marciuska | On Faceted Search over Knowledge Bases | DL | | Jul 19 11:45 |
| Chiara Del Vescovo and Rafael Peñaloza | DeaLing with Ontologies using CODs | DL | | Jul 20 09:50 |
| Thomas Eiter, Michael Fink and Daria Stepanova | Towards Practical Deletion Repair of Inconsistent DL-programs | DL | | Jul 18 10:45 |
| William Gatens, Boris Konev and Frank Wolter | Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies | DL | | Jul 20 09:00 |
| Birte Glimm, Yevgeny Kazakov, Thorsten Liebig, Trung-Kien Tran and Vincent Vialard | Abstraction Refinement for Ontology Materialization | DL | | Jul 17 14:55 |
| Peter Hansen, Carsten Lutz, Inanc Seylan and Frank Wolter | Query Rewriting under EL TBoxes: Efficient Algorithms | DL | | Jul 20 11:10 |
| Mark Kaminski, Yavor Nenov and Bernardo Cuenca Grau | Datalog Rewriting Techniques for Non-Horn Ontologies | DL | | Jul 18 16:40 |
| Yevgeny Kazakov and Pavel Klinov | Goal-Directed Tracing of Inferences in EL Ontologies | DL | | Jul 17 16:50 |
| Szymon Klarman and Thomas Meyer | Complexity of Temporal Query Abduction in DL-Lite | DL | | Jul 18 12:25 |
| Patrick Koopmann and Renate A. Schmidt | Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes | DL | | Jul 19 15:20 |
| Egor V. Kostylev, Juan L. Reutter and Domagoj Vrgoc | XPath for DL-Lite Ontologies | DL | | Jul 20 12:25 |
| Markus Krötzsch and Sebastian Rudolph | Complexities of Nominal Schemas | DL | | Jul 17 12:10 |
| Michel Ludwig and Rafael Peñaloza | Brave and Cautious Reasoning in EL | DL | | Jul 17 17:15 |
| Michel Ludwig and Dirk Walther | Detecting Conjunctive Query Differences between ELHr-Terminologies using Hypergraphs | DL | | Jul 19 14:55 |
| Francisco Martin-Recuerda and Dirk Walther | Axiom Dependency Hypergraphs for fast Atomic Decomposition of Ontologies | DL | | Jul 20 09:25 |
| Boris Motik, Yavor Nenov, Robert Piro, Ian Horrocks and Dan Olteanu | Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems | DL | | Jul 20 11:35 |
| Andreas Steigmiller, Birte Glimm and Thorsten Liebig | Optimised Absorption for Expressive Description Logics | DL | | Jul 19 17:40 |
| Giorgos Stoilos and Giorgos Stamou | Hybrid Query Answering Over DL Ontologies | DL | | Jul 19 17:15 |
| David Toman and Grant Weddell | Pushing the CFDnc Envelope | DL | | Jul 19 12:10 |
| Yujiao Zhou, Yavor Nenov, Bernardo Cuenca Grau and Ian Horrocks | Pay-as-you-go Ontology Query Answering Using a Datalog Reasoner | DL | | Jul 19 16:50 |
| Tahani Alsubait, Bijan Parsia and Uli Sattler | Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure? | DL | | Jul 18 15:41 |
| Fernando Bobillo and Umberto Straccia | A MILP-based decision procedure for the (Fuzzy) Description Logic ALCB | DL | | Jul 18 15:20 |
| Stefan Borgwardt, Felix Distel and Rafael Peñaloza | Gödel Description Logics with General Models | DL | | Jul 18 15:26 |
| Pierre Bourhis, Markus Krötzsch and Sebastian Rudolph | How to Best Nest Regular Path Queries | DL | | Jul 17 12:50 |
| Diego Calvanese, Wolfgang Fischl, Reinhard Pichler, Emanuel Sallinger and Mantas Simkus | Expressive Identification Constraints to Capture Functional Dependencies in Description Logics | DL | | Jul 19 12:47 |
| Marco Cerami and Umberto Straccia | Complexity sources in FDL | DL | | Jul 18 15:23 |
| Federico Cerutti, Geeth de Mel, Timothy Norman, Nir Oren, Artemis Parvizi, Paul Sullivan and Alice Toniolo | Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information | DL | | Jul 18 15:38 |
| Ismail Ilkan Ceylan and Rafael Peñaloza | Bayesian Description Logics | DL | | Jul 18 15:32 |
| Liang Chang, Uli Sattler and Tianlong Gu | An ABox Revision Algorithm for the Description Logic $\mathcal{EL_{\bot}}$ | DL | | Jul 17 15:45 |
| Jieying Chen, Michel Ludwig, Yue Ma and Dirk Walther | Evaluation of Extraction Techniques for Ontology Excerpts | DL | | Jul 19 12:56 |
| Marco Console, Domenico Lembo, Valerio Santarelli and Domenico Fabio Savo | Graphol: Ontology representation through diagrams | DL | | Jul 19 12:41 |
| Marco Console and Maurizio Lenzerini | Reducing Global Consistency to Local Consistency in Ontology-based Data Access - Extended Abstract | DL | | Jul 19 12:44 |
| Ali Rezaei Divroodi | Comparing the Expressiveness of Description Logics | DL | | Jul 17 12:35 |
| Ala Djeddai, Hassina Seridi and Tarek Khadir | Reasoning about Belief Uncertainty in DL Lite N bool | DL | | Jul 18 15:35 |
| Andreas Ecke, Rafael Peñaloza and Anni-Yasmin Turhan | Mary, What's Like All Cats? | DL | | Jul 18 15:44 |
| Fredrik Engström, Abdul Rahim Nizamani and Claes Strannegård | Generating Comprehensible Explanations in Description Logic | DL | | Jul 19 15:48 |
| Laura Giordano, Valentina Gliozzi, Nicola Olivetti and Gian Luca Pozzato | Rational closure in SHIQ | DL | | Jul 17 15:54 |
| Ken Halland, Arina Britz and Szymon Klarman | TBox abduction in ALC using a DL tableau | DL | | Jul 19 15:45 |
| Martin Homola, Jan Kluka, Vojtěch Svátek and Miroslav Vacura | Typed Higher-Order Variant of SROIQ - Why Not? | DL | | Jul 17 12:53 |
| Yevgeny Kazakov and Pavel Klinov | Bridging the Gap between Tableau and Consequence-Based Reasoning | DL | | Jul 17 12:44 |
| Tomer Kotek, Mantas Simkus, Helmut Veith and Florian Zuleger | Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability | DL | | Jul 17 12:47 |
| Domenico Lembo, Riccardo Rosati, Marco Ruzzi, Domenico Fabio Savo and Emanuele Tocci | Visualization and management of mappings in ontology-based data access (progress report) | DL | | Jul 19 12:38 |
| Maurizio Lenzerini, Lorenzo Lepore and Antonella Poggi | Practical query answering over Hi (DL-LiteR) knowledge bases | DL | | Jul 17 12:56 |
| Jared Leo, Ulrike Sattler and Bijan Parsia | Temporalising EL Concepts with Time Intervals | DL | | Jul 18 12:50 |
| Yue Ma and Rafael Peñaloza | Towards Parallel Repair: An Ontology Decomposition-based Approach | DL | | Jul 19 15:54 |
| Yuri Malheiros and Fred Freitas | A Method to Develop Description Logic Ontologies Iteratively with Automatic Requirement Traceability | DL | | Jul 19 12:53 |
| Nicolas Matentzoglu, Bijan Parsia and Uli Sattler | An Empirical Investigation of Difficulty of Subsets of Description Logic Ontologies | DL | | Jul 17 12:38 |
| Kody Moodley, Thomas Meyer and Uli Sattler | DIP: A Defeasible-Inference Platform for OWL Ontologies | DL | | Jul 17 15:57 |
| E. A. Nasubo Ongoma, C. Maria Keet and Thomas Meyer | Transition Constraints for Temporal Attributes | DL | | Jul 18 12:53 |
| Özgür Lütfü Özcep, Ralf Möller and Christian Neuenstadt | A Stream-Temporal Query Language for Ontology Based Data Access | DL | | Jul 18 12:56 |
| Rafael Peñaloza, Veronika Thost and Anni-Yasmin Turhan | Certain Answers in a Rough World | DL | | Jul 18 15:29 |
| Viachaslau Sazonau, Uli Sattler and Gavin Brown | Predicting OWL Reasoners: Locally or Globally? | DL | | Jul 17 12:41 |
| Ahmet Soylu, Evgeny Kharlamov, Dmitriy Zheleznyakov, Ernesto Jimenez-Ruiz, Martin Giese and Ian Horrocks | OptiqueVQS: Visual Query Formulation for OBDA | DL | | Jul 19 12:35 |
| Giorgos Stoilos | OBDA Using RL Reasoners and Repairing | DL | | Jul 19 12:50 |
| Zhe Wang, Kewen Wang, Guilin Qi, Zhiqiang Zhuang and Yuefeng Li | Instance-driven TBox Revision in DL-Lite | DL | | Jul 17 15:48 |
| Zhiqiang Zhuang, Zhe Wang, Kewen Wang and Grigoris Antoniou | Rational Elimination of DL-Lite TBox Axioms | DL | | Jul 17 15:51 |
| Bruno Buchberger | The Theorema Approach to Mathematics | PAS | | Jul 17 14:30 |
| Hoon Hong | Test-Input Generation using Computational Real Algebraic Geometry | PAS | | Jul 18 09:15 |
| Michael Rusinowitch | Automated verification of security protocols and services | PAS | | Jul 18 14:30 |
| Viorica Sofronie-Stokkermans | Hierarchical reasoning and quantifier elimination for the verification of parametric reactive and hybrid systems | PAS | | Jul 17 09:00 |
| Sandra Alves, Besik Dundua, Mario Florido and Temur Kutsia | Confluence of Pattern-Based Calculi with Finitary Matching | PAS | | Jul 17 17:00 |
| Xiaoyu Chen and Jie Luo | RCK: A Software Toolkit for R-calculus | PAS | | Jul 17 12:00 |
| Stefan Ciobaca, Dorel Lucanu, Vlad Rusu and Grigore Rosu | Programming Language Aggregation with Applications in Equivalence Checking | PAS | | Jul 18 17:30 |
| Isabela Dramnesc | Synthesis of Algorithms on Sets Represented as Monotone Lists | PAS | | Jul 18 10:45 |
| Xiaomei Hou, Mengxiang Lin and Tahir Jameel | A hybrid path constraint solver combined with meta-heuristic search | PAS | | Jul 18 16:30 |
| Hao Huang, Fangmin Song, Zhengjiang Qian, Kangjie Li, Jiang Chen, Shuiwang Guan and Wei Huang | VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel | PAS | | Jul 18 11:45 |
| Dongchen Jiang | The Verification of Conversion Algorithms between Finite Automata | PAS | | Jul 17 17:30 |
| Jens Knoop, Laura Kovacs and Jakob Zwirchmayr | Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis | PAS | | Jul 17 16:30 |
| Alexander Letichevsky, Oleksandr Letychevskyi, Vladimir Peschanenko and Thomas Weigert | New predicate transformer for symbolic modeling | PAS | | Jul 18 11:15 |
| Wei Li | An Attempt to Formalize Popper's Logic of Scientific Discovery | PAS | | Jul 17 10:45 |
| Kristjan Liiva, Grant Passmore and Paul Jackson | A note on real quantifier elimination by virtual term substitution of unbounded degree | PAS | | Jul 17 15:00 |
| Jie Luo and Wei Li | A Model Theory for R-calculus without Cut | PAS | | Jul 17 11:30 |
| Jakob Praher | Symbolic Problem Solving With Bidirectional Executable Representations | PAS | | Jul 18 12:15 |
| George Stergiopoulos, Panagiotis Katsaros and Dimitris Gritzalis | Source code profiling and classification for automated detection of logical errors | PAS | | Jul 17 18:00 |
| Sorin Stratulat | Building explicit induction schemas for cyclic induction reasoning | PAS | | Jul 18 15:30 |
| Farn Wang, Pin Hsiuan Chen and Wen-Hong Chiang | Automatic App Testing of LTL Properties | PAS | | Jul 18 17:00 |
| Erman Acar and Christian Meilicke | Multi-Attribute Decision Making using Weighted Description Logics | PRUV | | Jul 23 17:30 |
| Eva Armengol | Learning Preferences for Collaboration | PRUV | | Jul 23 16:30 |
| Libor Behounek | In Which Sense Is Fuzzy Logic a Logic for Vagueness? | PRUV | | Jul 23 10:45 |
| Christoph Beierle, Markus Höhnerbach and Marcus Marto | Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics | PRUV | | Jul 24 11:45 |
| Stefan Borgwardt, Marco Cerami and Rafael Peñaloza | Many-valued Horn Logic is Hard | PRUV | | Jul 23 15:30 |
| Arina Britz and Ivan Varzinczak | Towards a Logic of Dilation | PRUV | | Jul 23 11:45 |
| Tommaso Di Noia, Thomas Lukasiewicz, Maria Vanina Martinez, Gerardo Simari and Oana Tifrea-Marciuska | Computing k-Rank Answers with Ontological CP-Nets | PRUV | | Jul 23 17:00 |
| Andreas Ecke | Similarity-based Relaxed Instance Queries in EL++ | PRUV | | Jul 23 14:30 |
| Joohyung Lee and Yi Wang | Stable Models of Fuzzy Propositional Formulas | PRUV | | Jul 23 11:15 |
| Thomas Lukasiewicz, Maria Vanina Martinez, Cristian Molinaro, Livia Predoiu and Gerardo Simari | Answering Ontological Ranking Queries Based on Subjective Reports | PRUV | | Jul 24 10:45 |
| David Mitchell | Resolution and Clause Learning for Multi-Valued CNF Formulas | PRUV | | Jul 23 15:00 |
| Matt Kaufmann and J Moore | Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 | ACL2 | | Jul 12 09:30 |
| Jared Davis and Matt Kaufmann | Industrial-Strength Documentation for ACL2 | ACL2 | | Jul 12 09:00 |
| Harsh Raju Chamarthi, Peter Dillinger and Panagiotis Manolios | Data Definitions in ACL2 Sedan | ACL2 | | Jul 12 11:45 |
| Benjamin Selfridge and Eric Smith | Polymorphic Types In ACL2 | ACL2 | | Jul 12 11:15 |
| Jónathan Heras and Ekaterina Komendantskaya | ACL2(ml): Machine-Learning for ACL2 | ACL2 | | Jul 12 12:15 |
| Sebastiaan Joosten, Cezary Kaliszyk and Josef Urban | Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems | ACL2 | | Jul 12 10:45 |
| Ruben Gamboa and John Cowles | On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics | ACL2 | | Jul 12 16:30 |
| John Cowles and Ruben Gamboa | Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis | ACL2 | | Jul 13 09:30 |
| Ruben Gamboa and John Cowles | Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent | ACL2 | | Jul 13 09:00 |
| Disha Puri, Sandip Ray, Kecheng Hao and Fei Xie | Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis | ACL2 | | Jul 13 12:15 |
| Benjamin Selfridge | An ACL2 Mechanization of an Axiomatic Framework for Weak Memory | ACL2 | | Jul 13 11:45 |
| David Russinoff and John O'Leary | Modeling Algorithms in SystemC and ACL2 | ACL2 | | Jul 13 10:45 |
| David Hardin, Jennifer Davis, David Greve and Jedidiah McClurg | Development of a Translator from LLVM to ACL2 | ACL2 | | Jul 13 11:15 |
| Mnacho Echenim, Nicolas Peltier and Sophie Tourret | A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic | ADDCT | | Jul 18 10:45 |
| Paula Chocron, Pascal Fontaine and Christophe Ringeissen | Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions | ADDCT | | Jul 18 12:00 |
| Zvonimir Pavlinovic, Tim King and Thomas Wies | Finding Minimum Type Error Sources | ADDCT | | Jul 18 12:30 |
| Joseph Boudou and Philippe Balbiani | Decidability of Iteration-free PDL with Parallel Composition | ADDCT | | Jul 18 14:30 |
| Renate A. Schmidt, John Stell and David Rydeheard | Axiomatic and Tableau-Based Reasoning for Kt(H,R) | ADDCT | | Jul 18 15:00 |
| Domenico Cantone, Joanna Golinska-Pilarek and Marianna Nicolosi-Asmundo | On Dual Tableau-Based Decision Procedures for Relational Fragments | ADDCT | | Jul 18 15:30 |
| Vincent van Oostrom and Femke van Raamsdonk | The dynamic pattern calculus as a higher-order pattern rewriting system | HOR | | Jul 12 08:45 |
| Beniamino Accattoli, Pablo Barenbaum and Damiano Mazza | Distilling Abstract Machines (Extended Abstract) | HOR | | Jul 12 09:15 |
| Kristoffer Rose | Experience with Higher Order Rewriting from the Compiler Teaching Trenches | HOR | | Jul 12 09:45 |
| Cynthia Kop | The Higher-Order Dependency Pair Framework | HOR | | Jul 12 10:45 |
| Vincent Van Oostrom | Feebly not weakly | HOR | | Jul 12 11:15 |
| Leonardo De Moura and Dejan Jovanović | A Model-Constructing Satisfiability Calculus | SAT | | Jul 16 14:30 |
| Jakob Nordstrom | A (Biased) Proof Complexity Survey for SAT Practitioners | SAT | | Jul 15 14:30 |
| Nina Narodytska and Fahiem Bacchus | Cores in Core based MaxSat Algorithms: an Analysis | SAT | | Jul 14 11:45 |
| Jan Arne Telle, Sigve Hortemo Sæther and Martin Vatshelle | Solving MaxSAT and #SAT on structured CNF formulas | SAT | | Jul 14 11:15 |
| Takayuki Sakai, Kazuhisa Seto and Suguru Tamaki | Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction | SAT | | Jul 14 10:45 |
| Anton Belov, Marijn Heule and Joao Marques-Silva | MUS Extraction using Clausal Proofs | SAT | | Jul 14 12:40 |
| Joao Marques-Silva and Alessandro Previti | On Computing Preferred MUSes and MCSes | SAT | | Jul 14 12:10 |
| Matti Järvisalo and Janne H. Korhonen | Conditional Lower Bounds for Failed Literals and Related Techniques | SAT | | Jul 14 15:30 |
| Ronald de Haan and Stefan Szeider | Fixed-Parameter Tractable Reductions to SAT | SAT | | Jul 14 14:30 |
| Alexey Ignatiev, Antonio Morgado and Joao Marques-Silva | On Reducing Maximum Independent Set to Minimum Satisfiability | SAT | | Jul 14 15:00 |
| Mladen Miksa and Jakob Nordstrom | Long Proofs of (Seemingly) Simple Formulas | SAT | | Jul 15 10:45 |
| Gabriel Istrate and Adrian Crăciun | Proof complexity and the Lovasz-Kneser Theorem (I) | SAT | | Jul 15 11:15 |
| Valeriy Balabanov, Magdalena Widl and Jie-Hong Roland Jiang | QBF Resolution Systems and their Proof Complexities | SAT | | Jul 15 16:30 |
| Oliver Kullmann and Olaf Beyersdorff | Unified characterisations of resolution hardness measures | SAT | | Jul 15 15:30 |
| Tomohiro Sonobe, Shuya Kondoh and Mary Inaba | Community Branching for Parallel Portfolio SAT Solvers | SAT | | Jul 15 12:20 |
| Laurent Simon and Gilles Audemard | Lazy clause exchange policy for parallel SAT solvers | SAT | | Jul 15 12:40 |
| Alexander Nadel, Ofer Strichman and Vadim Ryvchin | Ultimately Incremental SAT | SAT | | Jul 15 11:50 |
| Boris Konev and Alexei Lisitsa | A SAT Attack on the Erdos Discrepancy Conjecture | SAT | | Jul 16 10:45 |
| Tamir Heyman, Dan Smith, Lance Leong, Husam Abu-Haimed and Yogesh Mahajan | Dominant Controllability Check Using QBF-Solver and Netlist Optimizer | SAT | | Jul 16 11:05 |
| Bernd Finkbeiner and Leander Tentrup | Fast DQBF Refutation | SAT | | Jul 16 11:35 |
| Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard and Laurent Simon | Impact of Community Structure on SAT Solver Performance | SAT | | Jul 16 12:30 |
| Friedrich Slivovsky and Stefan Szeider | Variable Dependencies and Q-Resolution | SAT | | Jul 16 12:00 |
| Armin Biere, Daniel Le Berre, Emmanuel Lonca and Norbert Manthey | Detecting cardinality constraints in CNF | SAT | | Jul 16 17:30 |
| Adrian Balint, Armin Biere, Andreas Fröhlich and Uwe Schöning | Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses | SAT | | Jul 16 15:30 |
| Tomáš Balyo, Andreas Fröhlich, Marijn Heule and Armin Biere | Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask) | SAT | | Jul 16 16:30 |
| Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio | Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions | SAT | | Jul 17 10:45 |
| Yoav Fekete and Michael Codish | Simplifying Pseudo-Boolean Constraints in Residual Number Systems | SAT | | Jul 16 17:00 |
| Oliver Gableske | An Ising Model inspired Extension of the Product-based MP Framework for SAT | SAT | | Jul 17 11:15 |
| Andrei Bulatov and Cong Wang | Approximating highly satisfiable random 2-SAT | SAT | | Jul 17 11:45 |
| Florent Capelli, Arnaud Durand and Stefan Mengel | Hypergraph Acyclicity and Propositional Model Counting | SAT | | Jul 17 12:15 |
| Carles Creus, Pau Fernández and Guillem Godoy | Automatic Evaluation of Reductions between NP-complete Problems | SAT | | Jul 14 17:10 |
| Nathan Wetzler, Marijn Heule and Warren Hunt | DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs | SAT | | Jul 14 16:50 |
| Charles Jordan, Lukasz Kaiser, Florian Lonsing and Martina Seidl | MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing | SAT | | Jul 14 16:30 |
| Ruben Martins, Vasco Manquinho and Ines Lynce | Open-WBO: a Modular MaxSAT Solver | SAT | | Jul 14 17:30 |
| Konstantin Korovin | Instantiation-based reasoning, EPR encodings and all that | LaSh | | Jul 18 09:00 |
| Peter Stuckey | Laziness is next to Godliness | LaSh | | Jul 18 14:30 |
| Michael Abseher, Bernhard Bliem, Günther Charwat, Frederico Dusberger, Markus Hecher and Stefan Woltran | The D-FLAT System for Dynamic Programming on Tree Decompositions | LaSh | | Jul 18 16:30 |
| Broes De Cat, Marc Denecker, Peter Stuckey, Maurice Bruynooghe and Bart Bogaerts | Lazy Model Expansion: Interleaving Grounding with Search | LaSh | | Jul 18 15:30 |
| Tomi Janhunen | Cross-Translating Answer Set Programs | LaSh | | Jul 18 17:10 |
| Jeremias Berg, Matti Järvisalo and Brandon Malone | Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability | LaSh | | Jul 18 12:15 |
| Bart Bogaerts, Joachim Jansen, Broes De Cat, Gerda Janssens, Maurice Bruynooghe and Marc Denecker | Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development | LaSh | | Jul 18 10:45 |
| Emir Demirović and Nysret Musliu | Modeling High School Timetabling as PartialWeighted maxSAT | LaSh | | Jul 18 11:45 |
| Shahab Tasharrofi and Eugenia Ternovska | Logical Machinery of Heuristics (Preliminary Report) | LaSh | | Jul 18 11:15 |
| Gilles Dowek | Simply Typed Lambda-Calculus Modulo Type Isomorphisms | SD | | Jul 12 09:15 |
| Rosalie Iemhoff | Completions and the Schuette method | SD | | Jul 12 10:45 |
| Kazushige Terui | Proof theory for ordered algebra: amalgamation and densification | SD | | Jul 12 14:30 |
| Marc Bagnol, Amina Doumane and Alexis Saurin | A Correctness Criterion Free from Switchings | SD | | Jul 12 11:45 |
| Taus Brock-Nannestad | Substructural Cut Elimination | SD | | Jul 12 16:30 |
| Christophe Fouqueré and Myriam Quatrini | Multiplicative Decomposition of Behaviours in Ludics | SD | | Jul 12 17:00 |
| Dominic Hughes | First-order Proofs Without Syntax: Summary of Work in Progress | SD | | Jul 12 12:15 |
| Marie Kerjean | Weak topologies for Linear Logic | SD | | Jul 12 15:30 |
| Orna Grumberg | SAT-Based Model Checking with Interpolation | iPRA | | Jul 17 10:45 |
| Pavel Pudlak | Feasible Interpolation in Proof Systems based on Integer Linear Programming | iPRA | | Jul 17 14:30 |
| Frank Wolter | Interpolation in Description Logic: A Survey | iPRA | | Jul 18 09:00 |
| Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk | Interpolants in Two-Player Games | iPRA | | Jul 17 12:00 |
| Chanseok Oh, Martin Schäf, Daniel Schwartz-Narbonne and Thomas Wies | Fault Localization using Interpolation | iPRA | | Jul 17 12:30 |
| David Toman and Grant Weddell | On Enumerating Query Plans via Interpolants from Tableau Proofs (abstract) | iPRA | | Jul 17 16:30 |
| Christoph Wernhard | Application Patterns of Projection/Forgetting | iPRA | | Jul 17 17:00 |
| Ahmed Mahdi and Martin Fränzle | Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theories Problems | iPRA | | Jul 17 17:30 |
| Patrick Koopmann and Renate A. Schmidt | Resolution Based Uniform Interpolation for Expressive Description Logics | iPRA | | Jul 18 10:45 |
| Alexander Legg, Nina Narodytska and Leonid Ryzhyk | Practical CNF Interpolants Via BDDs | iPRA | | Jul 18 11:15 |
| Enrico Franconi, Paolo Guagliardo, Volha Kerhet and Nhung Ngo | Interpolation and Domain Independence applied to Databases | iPRA | | Jul 18 11:45 |
| Georg Schadler and Georg Hofferek | Tree-based Modular SMT Solving | iPRA | | Jul 18 12:15 |
| Marco Rocchetto, Luca Viganò and Marco Volpe | Using Interpolation for the Verification of Security Protocols (Extended Abstract) | iPRA | | Jul 18 14:30 |
| Kenneth McMillan | Interpolation Strategies | iPRA | | Jul 18 15:00 |
| Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Ruemmer and Jari Stenman | Towards Craig Interpolation for String Constraints | iPRA | | Jul 18 15:30 |
| Aws Albarghouthi, Isil Dillig, Arie Gurfinkel and Marsha Chechik | Specification Synthesis via Generalized Abduction | iPRA | | Jul 18 16:30 |
| Yakir Vizel and Arie Gurfinkel | Interpolants from Clausal Proofs | iPRA | | Jul 18 17:00 |
| Clark Barrett | SMT: Where do we go from here? | SMT | | Jul 17 09:15 |
| Daniel J. Fremont and Sanjit A. Seshia | Speeding Up SMT-Based Quantitative Program Analysis | SMT | | Jul 17 10:45 |
| Hristina Palikareva and Cristian Cadar | Multi-solver Support in Symbolic Execution | SMT | | Jul 17 11:15 |
| Mats Carlsson, Olga Grinchtein and Justin Pearson | Protocol Log Analysis with Constraint Programming | SMT | | Jul 17 11:45 |
| Edmund S. L. Lam and Iliano Cervesato | Reasoning About Set Comprehensions | SMT | | Jul 17 12:15 |
| Juergen Christ and Jochen Hoenicke | Weakly Equivalent Arrays | SMT | | Jul 17 14:30 |
| Francesco Alberti, Silvio Ghilardi and Natasha Sharygina | Decision Procedures for Flat Array Properties | SMT | | Jul 17 15:00 |
| Richard Bonichon, David Déharbe and Cláudia Tavares | Extending SMT-LIB v2 with Lambda-Terms and Polymorphism | SMT | | Jul 17 15:30 |
| Guillaume Melquiond | Automating the Verification of Floating-Point Algorithms | SMT | | Jul 18 09:15 |
| Tim King, Clark Barrett and Cesare Tinelli | Leveraging Linear and Mixed Integer Programming for SMT | SMT | | Jul 18 10:45 |
| To Van Khanh, Vu Xuan Tung and Mizuhito Ogawa | raSAT: SMT for Polynomial Inequality | SMT | | Jul 18 11:15 |
| Marek Kosta, Thomas Sturm and Andreas Dolzmann | Better Answers to Real Questions | SMT | | Jul 18 11:45 |
| Konstantin Korovin, Marek Kosta and Thomas Sturm | Towards Conflict-Driven Learning for Virtual Substitution | SMT | | Jul 18 12:15 |
| Christos Dimoulas, Scott Moore, Aslan Askarov and Stephen Chong | Declarative Policies for Capability Control | CSF | | Jul 19 10:45 |
| Joshua Kroll, Gordon Stewart and Andrew Appel | Portable Software Fault Isolation | CSF | | Jul 19 11:15 |
| Radha Jagadeesan, Cm Lubinski, Corin Pitcher, James Riely and Charles Winebrinner | Certificates for Verifiable Forensics | CSF | | Jul 19 11:45 |
| Andrey Chudnov, George Kuan and David Naumann | Information flow monitoring as abstract interpretation for relational logic | CSF | | Jul 19 12:15 |
| Pablo Buiras, Deian Stefan and Alejandro Russo | On Dynamic Flow-sensitive Floating-Label Systems | CSF | | Jul 19 17:30 |
| Heiko Mantel, Matthias Perner and Jens Sauer | Noninterference under Weak Memory Models | CSF | | Jul 19 18:00 |
| Marian Harbach, Sascha Fahl and Matthew Smith | Who’s Afraid of Which Bad Wolf? A Survey of IT Security Risk Awareness | CSF | | Jul 20 10:45 |
| Jens Grossklags and David Reitter | How Task Familiarity and Cognitive Predispositions Impact Behavior in a Security Game of Timing | CSF | | Jul 20 11:15 |
| Jason Crampton and Alexandre Pinto | Attribute-based Encryption for Access Control Using Elementary Operations | CSF | | Jul 20 14:30 |
| Alex Malozemoff, Jonathan Katz and Matthew Green | Automated Analysis and Synthesis of Block-Cipher Modes of Operation | CSF | | Jul 20 15:00 |
| Joseph Ayo Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt and Pierre-Yves Strub | Certified Synthesis of Efficient Batch Verifiers | CSF | | Jul 20 15:30 |
| Melissa Chase, Markulf Kohlweiss, Anna Lysyanskaya and Sarah Meiklejohn | Malleable Signatures: New Definitions and Delegatable Anonymous Credentials | CSF | | Jul 20 17:30 |
| Chris Culnane and Steve Schneider | A Peered Bulletin Board for Robust Use in Verifiable Voting Systems | CSF | | Jul 20 16:30 |
| Dan Bogdanov, Peeter Laud, Sven Laur and Pille Pullonen | From Input Private to Universally Composable Secure Multi-party Computation Primitives | CSF | | Jul 20 17:00 |
| Daniel Dougherty and Joshua Guttman | Decidability for Lightweight Diffie-Hellman Protocols | CSF | | Jul 21 10:45 |
| Moses Liskov and Francisco Javier Thayer | Modeling Diffie-Hellman Derivability for Automated Analysis | CSF | | Jul 21 11:15 |
| David Basin, Cas Cremers and Marko Horvat | Actor Key Compromise: Consequences and Countermeasures | CSF | | Jul 21 11:45 |
| Sebastian A. Mödersheim and Georgios Katsoris | A Sound Abstraction of the Parsing Problem | CSF | | Jul 21 12:15 |
| Willard Rafnsson and Andrei Sabelfeld | Compositional Information-flow Security for Interactive Systems | CSF | | Jul 21 14:30 |
| Mathy Vanhoef, Willem De Groef, Dominique Devriese, Frank Piessens and Tamara Rezk | Stateful Declassification Policies for Event-Driven Programs | CSF | | Jul 21 15:00 |
| Mario Alvim, Kostas Chatzikokolakis, Annabelle McIver, Carroll Morgan, Catuscia Palamidessi and Geoffrey Smith | Additive and multiplicative notions of leakage, and their capacities | CSF | | Jul 21 15:30 |
| Benjamin Johnson, Aron Laszka and Jens Grossklags | The Complexity of Estimating Systematic Risk in Networks | CSF | | Jul 22 10:45 |
| Roberto Vigo, Flemming Nielson and Hanne Riis Nielson | Automated Generation of Attack Trees | CSF | | Jul 22 11:15 |
| Pedro Adão, Claudio Bozzato, Gian-Luca Dei Rossi, Riccardo Focardi and Flaminia Luccio | Mignis: A semantic based tool for firewall configuration | CSF | | Jul 22 11:45 |
| Michele Bugliesi, Stefano Calzavara, Riccardo Focardi, Wilayat Khan and Mauro Tempesta | Provably Sound Browser-Based Enforcement of Web Session Integrity | CSF | | Jul 22 12:15 |
| Michael Backes, Praveen Manoharan and Esfandiar Mohammadi | TUC: Time-sensitive and Modular Analysis of Anonymous Communication | CSF | | Jul 22 16:30 |
| Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan, Benjamin Pierce and Aaron Roth | Differential Privacy: An Economic Method for Choosing Epsilon | CSF | | Jul 22 17:00 |
| Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz and Pierre-Yves Strub | Proving differential privacy in Hoare logic | CSF | | Jul 22 17:30 |
| Jia Liu, Mark Ryan and Liqun Chen | Balancing Societal Security and Individual Privacy: Accountable Escrow System | CSF | | Jul 22 15:30 |
| Guy Avni, Orna Kupferman and Tami Tamir | From Reachability to Temporal Specifications in Cost-Sharing Games | IJCAR | | |
| Veronique Cortier | Electronic voting: how logic can help | IJCAR | | |
| Rajeev Gore | And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL | IJCAR | | Jul 19 10:45 |
| Kenneth McMillan | Structured Search and Learning | IJCAR | | Jul 22 10:45 |
| Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel | Unified Classical Logic Completeness: A Coinductive Pearl | IJCAR | | Jul 19 11:45 |
| Fredrik Lindblad | A Focused Sequent Calculus for Higher-Order Logic | IJCAR | | Jul 19 12:15 |
| Ori Lahav and Yoni Zohar | SAT-based Decision Procedure for Analytic Pure Sequent Calculi | IJCAR | | Jul 19 14:30 |
| Marijn Heule, Martina Seidl and Armin Biere | Unified Proof System for QBF Preprocessing | IJCAR | | Jul 19 15:00 |
| Carlos Ansótegui, Maria Luisa Bonet, Jesus Giráldez-Cru and Jordi Levy | The Fractal Dimension of SAT Formulas | IJCAR | | Jul 19 15:30 |
| Paula Chocron, Pascal Fontaine and Christophe Ringeissen | A Gentle Non-Disjoint Combination of Satisfiability Procedures | IJCAR | | Jul 19 16:30 |
| Sophie Tourret, Mnacho Echenim and Nicolas Peltier | A Rewriting Strategy to Generate Prime Implicates in Equational Logic | IJCAR | | Jul 20 10:45 |
| Peter Baumgartner, Joshua Bax and Uwe Waldmann | Finite Quantification in Hierarchic Theorem Proving | IJCAR | | Jul 20 11:15 |
| Josh Berdine and Nikolaj Bjorner | Computing All Implied Equalities via SMT-based Partition Refinement | IJCAR | | Jul 20 11:45 |
| Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Stroeder, Steffi Swiderski and Rene Thiemann | Proving Termination of Programs Automatically with AProVE | IJCAR | | Jul 20 12:15 |
| Matthias Horbach and Viorica Sofronie-Stokkermans | Locality Transfer: From Constrained Axiomatizations to Reachability Predicates | IJCAR | | Jul 20 14:30 |
| Thomas Stroeder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel and Peter Schneider-Kamp | Proving Termination and Memory Safety for Programs with Pointer Arithmetic | IJCAR | | Jul 20 15:00 |
| Wenhui Zhang | QBF Encoding of Temporal Properties and QBF-Based Verification | IJCAR | | Jul 20 15:30 |
| Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai and Daniel Weller | Introducing quantified cuts in logic with equality | IJCAR | | Jul 20 16:30 |
| Vivek Nigam, Giselle Reis and Leonardo Lima | Quati: An Automated Tool for Proving Permutation Lemmas | IJCAR | | Jul 20 17:00 |
| Rajeev Gore, Jimmy Thomson and Jesse Wu | A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description | IJCAR | | Jul 20 17:20 |
| Jens Otten | MleanCoP: A Connection Prover for First-Order Modal Logic | IJCAR | | Jul 20 17:40 |
| Serenella Cerrito, Amélie David and Valentin Goranko | Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ | IJCAR | | Jul 21 10:45 |
| Jean-Baptiste Jeannin and André Platzer | dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems | IJCAR | | Jul 21 11:15 |
| Bjoern Lellmann | Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications | IJCAR | | Jul 21 11:45 |
| Cláudia Nalon, João Marcos and Clare Dixon | Clausal Resolution for Modal Logics of Confluence | IJCAR | | Jul 21 12:15 |
| Rajeev Gore, Kerry Olesen and Jimmy Thomson | Implementing Tableaux Calculi Using BDDs: BDDTab System Description | IJCAR | | Jul 21 12:45 |
| Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Ruemmer | Approximations for Model Construction | IJCAR | | Jul 21 14:30 |
| Rüdiger Ehlers and Martin Lange | A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic | IJCAR | | Jul 21 15:00 |
| Aaron Stump, Geoff Sutcliffe and Cesare Tinelli | StarExec: a Cross-Community Infrastructure for Logic Solving | IJCAR | | Jul 21 15:20 |
| Bruno Woltzenlogel Paleo, Joseph Boudou and Andreas Fellner | Skeptik [System Description] | IJCAR | | Jul 21 15:40 |
| Fabio Papacchini and Renate A. Schmidt | Terminating Minimal Model Generation Procedures for Propositional Modal Logics | IJCAR | | Jul 21 16:00 |
| Daniel Gorin, Dirk Pattinson, Lutz Schröder, Thorsten Wißmann and Florian Widmann | COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) | IJCAR | | Jul 21 16:30 |
| Olaf Beyersdorff and Leroy Chew | The Complexity of Theorem Proving in Circumscription and Minimal Entailment | IJCAR | | Jul 22 11:45 |
| Laura Bozzelli and Cesar Sanchez | Visibly Linear Temporal Logic | IJCAR | | Jul 22 12:15 |
| Patrick Koopmann and Renate A. Schmidt | Count and Forget: Uniform Interpolation of SHQ-Ontologies | IJCAR | | Jul 22 14:30 |
| Andreas Steigmiller, Birte Glimm and Thorsten Liebig | Coupling Tableau Algorithms for Expressive Description Logics with Completion-based Saturation Procedures | IJCAR | | Jul 22 15:00 |
| David Carral, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler and Ian Horrocks | EL-ifying Ontologies | IJCAR | | Jul 22 15:30 |
| İsmail İlkan Ceylan and Rafael Peñaloza | The Bayesian Description Logic BEL | IJCAR | | Jul 22 16:30 |
| Michael Beeson and Larry Wos | Otter proofs in Tarskian geometry | IJCAR | | Jul 22 17:00 |
| Nicola Olivetti and Gian Luca Pozzato | NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics | IJCAR | | Jul 22 17:30 |
| Adam Pease and Stephan Schulz | Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 | IJCAR | | Jul 22 17:50 |
| Georg Gottlob | Structural Decomposition Methods: How They Matter | PCCR | | Jul 18 14:30 |
| Stefan Szeider | Fixed-Parameter Algorithms for Reasoning Problems in NP and Beyond | PCCR | | Jul 17 11:00 |
| Robert Ganian, Stefan Szeider and M.S. Ramanujan | Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction | PCCR | | Jul 18 12:00 |
| Serge Gaspers, Neeldhara Misra, Sebastian Ordyniak, Stefan Szeider and Stanislav Zivny | Backdoors into Heterogeneous Classes of SAT and CSP | PCCR | | Jul 18 15:30 |
| Jan Johannsen | Backdoors into Two Occurrences | PCCR | | Jul 18 11:15 |
| Martin Kronegger, Martin Lackner, Andreas Pfandler and Reinhard Pichler | A Parameterized Complexity Analysis of Generalized CP-Nets | PCCR | | Jul 17 12:00 |
| Martin Kronegger, Sebastian Ordyniak and Andreas Pfandler | Backdoors to Planning | PCCR | | Jul 17 12:30 |
| Nadia Labai and Johann Makowsky | Connection matrices of finite rank instead of definability in Monadic Second Order Logic | PCCR | | Jul 18 10:45 |
| R. Ramanujam and S P Suresh | Intuitionistic modal logics: efficient fragments and parameterized complexity | PCCR | | Jul 17 14:30 |
| Martin Gebser and Jael Kriener | The ICLP 2014 Doctoral Consortium | ICLP | | |
| Matthias Baaz, Thomas Eiter and Helmut Veith | Vienna Summer of Logic Preface | ICLP | | |
| Michael Leuschel and Tom Schrijvers | Introduction to the 30th International Conference on Logic Programming Special Issue | ICLP | | |
| Francesco Calimeri, Martin Gebser, Marco Maratea and Francesco Ricca | The Design of the Fifth Answer Set Programming Competition | ICLP | | |
| Andrey Rybalchenko | (Quantified) Horn Constraint Solving for Program Verification and Synthesis | ICLP | | Jul 17 14:30 |
| Neng-Fa Zhou | Combinatorial Search With Picat | ICLP | | |
| Mário Abrantes and Luís Moniz Pereira | Properties of Stable Model Semantics Extensions | ICLP | | Jul 21 11:00 |
| Mario Alviano, Carmine Dodaro and Francesco Ricca | Anytime Computation of Cautious Consequences in Answer Set Programming | ICLP | | Jul 22 17:00 |
| Roberto Amadini, Maurizio Gabbrielli and Jacopo Mauro | SUNNY: a Lazy Portfolio Approach for Constraint Solving | ICLP | | Jul 22 11:30 |
| Christian Antic | On Cascade Products of Answer Set Programs | ICLP | | Jul 20 14:30 |
| Miguel Areias and Ricardo Rocha | A Simple and Efficient Lock-Free Hash Trie Design for Concurrent Tabling | ICLP | | Jul 21 11:00 |
| Rehan Abdul Aziz, Geoffrey Chu and Peter J. Stuckey | Grounding Bound Founded Answer Set Programs | ICLP | | Jul 21 12:15 |
| Marcello Balduccini, William Regli and Duc Nguyen | An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments | ICLP | | Jul 21 12:30 |
| Roman Bartak and Neng-Fa Zhou | Using Tabled Logic Programming to Solve the Petrobras Planning Problem | ICLP | | Jul 22 12:00 |
| Elena Bellodi, Evelina Lamma, Fabrizio Riguzzi, Vítor Santos Costa and Riccardo Zese | Lifted Probabilistic Logic Programming | ICLP | | Jul 19 11:30 |
| Yi Bi, Jia-Huai You and Zhiyong Feng | A Well-Founded Semantics for FOL-Programs | ICLP | | Jul 21 11:15 |
| Bart Bogaerts, Joachim Jansen, Bruynooghe Maurice, Broes De Cat, Joost Vennekens and Marc Denecker | Simulating Dynamic Systems Using Linear Time Calculus Theories | ICLP | | Jul 20 17:00 |
| Bart Bogaerts, Joost Vennekens, Marc Denecker and Jan Van den Bussche | C-Log: A Knowledge Representation Language of Causality | ICLP | | Jul 21 11:45 |
| Stefan Brass | A Framework for Bottom-Up Simulation of SLD-Resolution | ICLP | | Jul 21 12:15 |
| Pedro Cabalar, Jorge Fandiño and Michael Fink | Causal Graph Justifications of Logic Programs | ICLP | | Jul 20 15:30 |
| Luciano Caroprese, Mirek Truszczynski, Ester Zumpano and Irina Trubitsyna | A Measure of Arbitrariness in Abductive Explanations | ICLP | | Jul 21 15:00 |
| Sergio Castro, Kim Mens and Paulo Moura | Customisable Handling of Java References in Prolog Programs | ICLP | | Jul 21 12:00 |
| Angelos Charalambidis, Zoltan Esik and Panos Rondogiannis | Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation | ICLP | | Jul 19 12:00 |
| Marco Comini, Laura Titolo and Alicia Villanueva | Abstract Diagnosis for tccp using a Linear Temporal Logic | ICLP | | Jul 19 12:30 |
| Flavio Cruz, Seth Goldstein, Frank Pfenning and Ricardo Rocha | A Linear Logic Programming Language for Concurrent Programming over Graph Structures | ICLP | | Jul 19 11:00 |
| Gregory J. Duck, Rémy Haemmerlé and Martin Sulzmann | On Termination, Confluence and Consistent CHR-based Type Inference | ICLP | | Jul 20 11:30 |
| Daniel Gall and Thom Frühwirth | Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R | ICLP | | Jul 20 12:00 |
| John P. Gallagher and Bishoksan Kafle | Analysis and Transformation Tools for Constrained Horn Clause Verification | ICLP | | Jul 21 11:30 |
| Marco Gavanelli, Michela Milano, Stefano Bragaglia, Federico Chesani, Elisa Marengo and Paolo Cagnoli | Multi-criteria optimal planning for Energy policies in CLP | ICLP | | Jul 21 10:45 |
| Martin Gebser, Roland Kaminski, Benjamin Kaufmann and Torsten Schaub | Clingo = ASP + Control | ICLP | | Jul 21 11:15 |
| Michael Gelfond and Yuanlin Zhang | Vicious Circle Principle and Logic Programs with Aggregates | ICLP | | Jul 20 15:00 |
| Ana Sofia Gomes and Jose Julio Alferes | Transaction Logic with (Complex) Events | ICLP | | Jul 21 10:45 |
| Jónathan Heras, Ekaterina Komendantskaya and Martin Schmidt | (Co)recursion in Logic Programming: Lazy vs Eager | ICLP | | Jul 21 11:45 |
| Holger Hoos, Marius Lindauer and Torsten Schaub | claspfolio 2: Advances in Algorithm Selection for Answer Set Programming | ICLP | | Jul 20 17:30 |
| Ethan K. Jackson | A Module System for Domain-Specific Languages | ICLP | | Jul 19 14:30 |
| Torbjörn Lager and Jan Wielemaker | Pengines: Web Logic Programming Made Easy | ICLP | | Jul 19 16:30 |
| Tiep Le, Enrico Pontelli, Tran Cao Son and William Yeoh | Logic and Constraint Logic Programming for Distributed Constraint Optimization | ICLP | | Jul 21 11:30 |
| Theofrastos Mantadelis, Ricardo Rocha and Paulo Moura | Tabling, Rational Terms, and Coinduction Finally Together! | ICLP | | Jul 19 17:30 |
| Kyle Marple and Gopal Gupta | Dynamic Consistency Checking in Goal-Directed Answer Set Programming | ICLP | | Jul 22 16:30 |
| Luís Moniz Pereira, Emmanuelle-Anna Dietz and Steffen Hölldobler | Contextual Abductive Reasoning with Side-Effects | ICLP | | Jul 21 15:30 |
| Arun Nampally and C. R. Ramakrishnan | Adaptive MCMC-Based Inference in Probabilistic Logic Programs | ICLP | | Jul 21 12:00 |
| G. Narboni | Numerical Properties of Min-closed CSPs | ICLP | | Jul 21 11:00 |
| Vivek Nigam, Carlos Olarte and Elaine Pimentel | A Proof Theoretic Study of Soft Concurrent Constraint Programming | ICLP | | Jul 22 12:30 |
| Aya Saad, Thom Fruehwirth and Carmen Gervet | The P-Box CDF-Intervals: A Reliable Constraint Reasoning with Quantifiable Information | ICLP | | Jul 20 12:30 |
| Ari Saptawijaya and Luís Moniz Pereira | Joint Tabling of Logic Program Abductions and Updates | ICLP | | Jul 21 10:45 |
| Alejandro Serrano, Pedro Lopez-Garcia and Manuel V. Hermenegildo | Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types | ICLP | | Jul 22 15:30 |
| Martin Slota, Martin Balaz and Joao Leite | On Strong and Default Negation in Answer-Set Program Updates | ICLP | | Jul 21 11:30 |
| George Souza Oliveira and Anderson Faustino Da Silva | Towards an Efficient Prolog System by Code Introspection | ICLP | | Jul 21 11:45 |
| Nataliia Stulova, Jose F. Morales and Manuel V. Hermenegildo | Towards Assertion-based Debugging of Higher-Order (C)LP Programs | ICLP | | Jul 21 11:15 |
| Terrance Swift | Incremental Tabling for Knowledge Representation and Reasoning | ICLP | | Jul 19 17:00 |
| Ilias Tachmazidis, Grigoris Antoniou and Wolfgang Faber | Efficient Computation of the Well-Founded Semantics over Big Data | ICLP | | Jul 22 17:30 |
| Paul Tarau and Fahmida Hamid | Interclausal Logic Variables | ICLP | | Jul 21 12:15 |
| Zhizheng Zhang | ESmodels: An Epistemic Specification Solver | ICLP | | Jul 21 12:00 |
| Rehan Abdul Aziz | Bound Founded Answer Set Programming | ICLP | | |
| Joachim Jansen | Model Revision Inference for Extensions of First Order Logic | ICLP | | |
| Grzegorz Jaśkiewicz | Logic Programming as Scripting Language for Bots in Computer Games - Research Overview | ICLP | | |
| Michael Morak | The Impact of Disjunction on Reasoning under Existential Rules: Research Summary | ICLP | | |
| Aya Saad | CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty | ICLP | | |
| Nada Sharaf | Visualization of Constraint Handling Rules | ICLP | | |
| Heike Stephan | Application of Methods for Syntax Analysis of Context-Free Languages to Query Evaluation of Logic Programs | ICLP | | |
| Riccardo Zese | Reasoning with Probabilistic Logics | ICLP | | |
| Christel Baier, Clemens Dubslaff and Sascha Klueppelholz | Trade-Off Analysis Meets Probabilistic Model Checking | CSL-LICS | | Jul 18 09:15 |
| Patrick Cousot and Radhia Cousot | Abstract Interpretation: Past, Present and Future | CSL-LICS | | Jul 15 16:30 |
| Jasmin Fisher | Understanding Biology through Logic | CSL-LICS | | Jul 14 14:30 |
| Assia Mahboubi | Computer-checked mathematics: a formal proof of the Odd Order theorem | CSL-LICS | | Jul 14 10:45 |
| Anuj Dawar | The Ackermann Award 2014 | CSL-LICS | | Jul 18 17:00 |
| Dexter Kozen | Citations for the Test-of-Time Award from 1994 | CSL-LICS | | Jul 18 16:30 |
| Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar and Patrick Totzke | Infinite-State Energy Games | CSL-LICS | | Jul 16 11:45 |
| Beniamino Accattoli and Ugo Dal Lago | Beta Reduction is Invariant, Indeed | CSL-LICS | | Jul 14 17:00 |
| Rajeev Alur, Adam Freilich and Mukund Raghothaman | Regular Combinators for String Transformations | CSL-LICS | | Jul 18 14:30 |
| Eugene Asarin, Michel Bockelet, Aldric Degorre, Cătălin Dima and Chunyan Mu | Asymptotic behaviour in temporal logic | CSL-LICS | | Jul 18 11:45 |
| Christel Baier, Joachim Klein, Sascha Klueppelholz and Sascha Wunderlich | Weight Monitoring with Linear Temporal Logic: Complexity and Decidability | CSL-LICS | | Jul 18 12:15 |
| Pablo Barceló and Pablo Muñoz | Graph Logics with Rational Relations: The Role of Word Combinatorics | CSL-LICS | | Jul 16 10:45 |
| Michael Benedikt, Balder Ten Cate and Michael Vanden Boom | Effective Interpolation and Preservation in Guarded Logics | CSL-LICS | | Jul 16 16:30 |
| Marco Bernardo, Davide Sangiorgi and Valeria Vignudelli | On the Discriminating Power of Passivation and Higher-Order Interaction | CSL-LICS | | Jul 18 11:15 |
| Paul Bilokon and Abbas Edalat | A domain-theoretic approach to Brownian motion and general continuous stochastic processes | CSL-LICS | | Jul 14 11:45 |
| Achim Blumensath, Thomas Colcombet, Denis Kuperberg, Paweł Parys and Michael Vanden Boom | Two-Way Cost Automata and Cost Logics over Infinite Trees | CSL-LICS | | Jul 15 14:30 |
| Christoph Dittmann, Stephan Kreutzer and Mikolaj Bojanczyk | Decomposition Theorems and Model-Checking for the Modal $\mu$-calculus | CSL-LICS | | Jul 15 14:30 |
| Benedikt Bollig | Logic for Communicating Automata with Parameterized Topology | CSL-LICS | | Jul 14 16:30 |
| Benedikt Bollig, Paul Gastin, Benjamin Monmege and Marc Zeitoun | Logical Characterization of Weighted Pebble Walking Automata | CSL-LICS | | Jul 15 15:00 |
| Filippo Bonchi, Daniela Petrisan, Damien Pous and Jurriaan Rot | Coinduction Up-To in a Fibrational Setting | CSL-LICS | | Jul 15 10:45 |
| Simone Bova, Robert Ganian and Stefan Szeider | Model Checking Existential Logic on Partially Ordered Sets | CSL-LICS | | Jul 16 11:15 |
| Tomas Brazdil, Stefan Kiefer, Antonin Kucera, Petr Novotný and Joost-Pieter Katoen | Zero-Reachability in Probabilistic Multi-Counter Automata | CSL-LICS | | Jul 15 10:45 |
| Romain Brenguier, Jean-Francois Raskin and Mathieu Sassolas | The Complexity of Admissibility in Omega-Regular Games | CSL-LICS | | Jul 17 15:00 |
| Flavien Breuvart | On the characterization of models of H* | CSL-LICS | | Jul 17 15:00 |
| James Brotherston, Carsten Fuhs, Nikos Gorogiannis and Juan Navarro Perez | A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates | CSL-LICS | | Jul 16 17:30 |
| Véronique Bruyère, Noémie Meunier and Jean-Francois Raskin | Secure Equilibria in Weighted Games | CSL-LICS | | Jul 15 11:45 |
| Facundo Carreiro, Alessandro Facchini, Yde Venema and Fabio Zanasi | Weak MSO: Automata and Expressiveness Modulo Bisimilarity | CSL-LICS | | Jul 16 12:15 |
| Simon Castellan, Pierre Clairambault and Glynn Winskel | Symmetry in Concurrent Games | CSL-LICS | | Jul 14 18:00 |
| Witold Charatonik, Emanuel Kieronski and Filip Mazowiecki | Decidability of Weak Logics with Deterministic Transitive Closure | CSL-LICS | | Jul 17 14:30 |
| Kaustuv Chaudhuri and Nicolas Guenot | Equality and Fixpoints in the Calculus of Structures | CSL-LICS | | Jul 16 17:30 |
| Hubie Chen | The Tractability Frontier of Graph-Like First-Order Query Sets | CSL-LICS | | Jul 16 15:30 |
| Hubie Chen and Moritz Mueller | One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries | CSL-LICS | | Jul 16 15:00 |
| Taolue Chen and Stefan Kiefer | On the Total Variation Distance of Labelled Markov Chains | CSL-LICS | | Jul 14 11:15 |
| Julien Cretin and Didier Rémy | System F with Coercion Constraints | CSL-LICS | | Jul 16 14:30 |
| Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo and Akira Yoshimizu | The Geometry of Synchronization | CSL-LICS | | Jul 18 11:15 |
| Anupam Das | On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems | CSL-LICS | | Jul 14 17:30 |
| Stephane Demri and Morgan Deters | Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction | CSL-LICS | | Jul 16 17:00 |
| Thomas Ehrhard | A new correctness criterion for MLL proof nets | CSL-LICS | | Jul 18 11:45 |
| Joerg Endrullis and Dimitri Hendriks | On Periodically Iterated Morphisms | CSL-LICS | | Jul 18 15:00 |
| Diego Figueira and Leonid Libkin | Pattern Logics and Auxiliary Relations | CSL-LICS | | Jul 17 15:30 |
| Marcelo Fiore and Sam Staton | Substitution, jumps, and algebraic effects | CSL-LICS | | Jul 16 16:30 |
| Matt Fredrikson and Somesh Jha | Satisfiability Modulo Counting: A New Approach for Analyzing Privacy Properties | CSL-LICS | | Jul 16 12:15 |
| Georg Gottlob and Enrico Malizia | Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic | CSL-LICS | | Jul 15 15:30 |
| Niels Bjørn Bugge Grathwohl, Dexter Kozen and Konstantinos Mamouras | KAT + B! | CSL-LICS | | Jul 17 14:30 |
| Nicolas Guenot and Lutz Strassburger | Symmetric Normalisation for Intuitionistic Logic | CSL-LICS | | Jul 16 11:45 |
| Julian Gutierrez and Michael Wooldridge | Equilibria of Concurrent Games on Event Structures | CSL-LICS | | Jul 14 17:00 |
| Christoph Haase | Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy | CSL-LICS | | Jul 18 10:45 |
| Matthew Hague | Senescent Ground Tree Rewrite Systems | CSL-LICS | | Jul 15 11:15 |
| Frederik Harwath, Lucas Heimberg and Nicole Schweikardt | Preservation and decomposition theorems for bounded degree structures | CSL-LICS | | Jul 17 11:15 |
| Willem Heijltjes and Robin Houston | No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete | CSL-LICS | | Jul 16 17:00 |
| Wei Chen and Martin Hofmann | Abstract Interpretation from Buchi Automata | CSL-LICS | | Jul 15 11:45 |
| Naohiko Hoshino, Koko Muroya and Ichiro Hasuo | Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects | CSL-LICS | | Jul 17 11:15 |
| Danko Ilik | Axioms and Decidability for Type Isomorphism in the Presence of Sums | CSL-LICS | | Jul 16 10:45 |
| Alan Jeffrey | Functional Reactive Types | CSL-LICS | | Jul 17 15:30 |
| Joost-Pieter Katoen, Lei Song and Lijun Zhang | Probably Safe or Live | CSL-LICS | | Jul 16 15:30 |
| Bakh Khoussainov | A quest for algorithmically random infinite structures | CSL-LICS | | Jul 14 10:45 |
| Stanislav Kikot, Roman Kontchakov, Vladimir Podolskii and Michael Zakharyaschev | On the Succinctness of Query Rewriting over Shallow Ontologies | CSL-LICS | | Jul 17 11:45 |
| Bartek Klin, Sławomir Lasota, Joanna Ochremiak and Szymon Toruńczyk | Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity | CSL-LICS | | Jul 14 16:30 |
| Eric Koskinen and Tachio Terauchi | Local Temporal Reasoning | CSL-LICS | | Jul 15 15:30 |
| Stephan Kreutzer and Nicole Schweikardt | On Hanf-equivalence and the number of embeddings of small induced subgraphs | CSL-LICS | | Jul 16 14:30 |
| Ranko Lazić and Sylvain Schmitz | Non-Elementary Complexities for Branching VASS, MELL, and Extensions | CSL-LICS | | Jul 18 12:15 |
| Stephane Le Roux and Arno Pauly | Infinite sequential games with real-valued payoffs | CSL-LICS | | Jul 15 12:15 |
| Jerome Leroux, M. Praveen and Grégoire Sutre | Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems | CSL-LICS | | Jul 17 10:45 |
| Paul Blain Levy and Sam Staton | Transition systems over games | CSL-LICS | | Jul 17 10:45 |
| Hongjin Liang, Xinyu Feng and Zhong Shao | Compositional Verification of Termination-Preserving Refinement of Concurrent Programs | CSL-LICS | | Jul 14 17:30 |
| Daniel R. Licata and Eric Finster | Eilenberg-MacLane Spaces in Homotopy Type Theory | CSL-LICS | | Jul 18 15:30 |
| Katja Losemann and Wim Martens | MSO Queries on Trees: Enumerating Answers under Updates | CSL-LICS | | Jul 17 12:15 |
| Marcello Mamino | On the Computing Power of +, −, and × | CSL-LICS | | Jul 14 12:15 |
| Konstantinos Mamouras | On the Hoare Theory of Monadic Recursion Schemes | CSL-LICS | | Jul 17 12:15 |
| Guillaume Munch-Maccagnoni | Formulae-as-Types for an Involutive Negation | CSL-LICS | | Jul 18 15:00 |
| Rasmus Ejlers Møgelberg | A type theory for productive coprogramming via guarded recursion | CSL-LICS | | Jul 18 14:30 |
| Luca Padovani | Deadlock and lock freedom in the linear pi-calculus | CSL-LICS | | Jul 15 11:15 |
| Matthieu Perrinel | On Context Semantics for Interaction Nets | CSL-LICS | | Jul 18 10:45 |
| Grgur Petric Maretic, Mohammad Torabi Dashti and David Basin | Anchored LTL Separation | CSL-LICS | | Jul 16 15:00 |
| Thomas Place and Marc Zeitoun | Separating Regular Languages with First-Order Logic | CSL-LICS | | Jul 15 12:15 |
| Ian Pratt-Hartmann | Logics with Counting and Equivalence | CSL-LICS | | Jul 15 15:00 |
| Pierre-Marie Pédrot | A functional functional interpretation | CSL-LICS | | Jul 16 11:15 |
| Takeshi Tsukada and Luke Ong | Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees | CSL-LICS | | Jul 17 11:45 |
| Yaron Velner | Finite-Memory Strategy Synthesis for Robust Multidimensional Mean-Payoff Objectives | CSL-LICS | | Jul 18 15:30 |
| Ryan Williams | Faster decision of first-order graph properties | CSL-LICS | | Jul 14 18:00 |
| Jean-Michel Muller | Getting tight error bounds in floating-point arithmetic: illustration with complex functions, and the real x^n function | NSV | | Jul 17 09:15 |
| Sumit Kumar Jha | Verifying Parameterized Software Models in Computational IData Science against Behavioral Specifications | NSV | | Jul 17 16:30 |
| James Kapinski | Numerical Challenges in Simulation-guided Dynamical System Analysis | NSV | | Jul 18 16:30 |
| Pierre Neron | Certifying Square Root and Division Elimination | NSV | | Jul 17 14:30 |
| Alexandre Chapoutot, Nasrine Damouche and Matthieu Martel | Transformation of a PID Controller for Numerical Accuracy | NSV | | Jul 17 11:15 |
| Christoph Spandl | Computational complexity of iterated maps on points and sets | NSV | | Jul 17 15:00 |
| Geoffrey C. Hulette, Robert C. Armstrong, Jackson R. Mayo and Joseph R. Ruthruff | Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics | NSV | | Jul 17 10:45 |
| Assale Adje | Policy iteration in finite templates domain | NSV | | Jul 17 11:45 |
| Takahito Aoto and Sorin Stratulat | Decision Procedures for Proving Inductive Theorems Without Induction | IFIP-WG16 | | Jul 13 08:45 |
| Gilles Dowek and Ying Jiang | Rewriting, Proofs, and Transition Systems | IFIP-WG16 | | Jul 13 10:45 |
| Maria Paola Bonacina and David Plaisted | Semantically-Guided Goal-Sensitive Theorem Proving | IFIP-WG16 | | Jul 13 11:30 |
| Nao Hirokawa, Aart Middeldorp and Georg Moser | Basic Normalization | IFIP-WG16 | | Jul 13 14:30 |
| Florent Jacquemard, Jean Bresson and Pierre Donat-Bouillud | Rhythm Tree Rewriting | IFIP-WG16 | | Jul 13 15:15 |
| Michael Leuschel | Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools | VPT | | |
| Klaus von Gleissenthall, Andrey Rybalchenko and Santiago Zanella-Béguelin | Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk) | VPT | | Jul 18 08:45 |
| Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti | Program Verification using Constraint Handling Rules and Array Constraint Generalizations | VPT | | Jul 17 11:30 |
| Daniil Frumin and Irina Lomazova | Branching Processes of Conservative Nested Petri Nets | VPT | | Jul 18 11:30 |
| Geoff Hamilton and Morten Heine Sørensen | Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem | VPT | | Jul 18 12:15 |
| Alexei Lisitsa and Andrei Nemytykh | A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal? | VPT | | Jul 17 12:15 |
| Andrei Nemytykh | On Unfolding for Programs Using Strings as a Data Type | VPT | | Jul 18 10:45 |
| Antonina Nepeivoda | Verification of Multi-Party Ping-Pong Protocols via Program Transformation | VPT | | Jul 17 10:45 |
| Thomas Sewell | Formal Replay of Translation Validation for Highly Optimised C | VPT | | Jul 18 17:30 |
| Michael Abseher, Bernhard Bliem, Günther Charwat, Frederico Dusberger and Stefan Woltran | Computing Secure Sets in Graphs using Answer Set Programming | ASPOCP | | Jul 23 15:35 |
| Mario Alviano, Carmine Dodaro, Joao Marques-Silva and Francesco Ricca | On the Implementation of Weak Constraints in WASP | ASPOCP | | Jul 23 16:55 |
| Joseph Babb and Joohyung Lee | Action Language BC+: Preliminary Report | ASPOCP | | Jul 23 12:35 |
| Evgenii Balai and Patrick Kahl | Epistemic Logic Programs with Sorts | ASPOCP | | Jul 23 11:10 |
| Gerhard Brewka, James Delgrande, Javier Romero and Torsten Schaub | ``Are Preferences Giving You a Headache?'' - ``Take asprin!'' | ASPOCP | | Jul 23 16:30 |
| Pedro Cabalar and Martín Diéguez | Temporal Stable Models are LTL-representable | ASPOCP | | Jul 23 11:45 |
| Stefania Costantini and Andrea Formisano | Query Answering in Resource-Based Answer Set Semantics | ASPOCP | | Jul 23 14:45 |
| Martin Gebser, Tomi Janhunen and Jussi Rintanen | Declarative Encodings of Acyclicity Properties | ASPOCP | | Jul 23 15:10 |
| Amelia Harrison, Vladimir Lifschitz, David Pearce and Agustín Valverde | Infinitary Equilibrium Logic | ASPOCP | | Jul 23 09:50 |
| Patrick Kahl, Richard Watson, Michael Gelfond and Yuanlin Zhang | A Refinement of the Language of Epistemic Specifications | ASPOCP | | Jul 23 10:45 |
| Kostyantyn Shchekotykhin | Interactive Query-based Debugging of ASP Programs | ASPOCP | | Jul 23 17:20 |
| Ilias Tachmazidis, Grigoris Antoniou and Wolfgang Faber | Computing Answer Sets for Monadic Logic Programs via MapReduce | ASPOCP | | Jul 23 17:45 |
| Shahab Tasharrofi and Eugenia Ternovska | Supported Semantics for Modular Systems | ASPOCP | | Jul 23 09:25 |
| Shiqi Zhang, Fangkai Yang, Piyush Khandelwal and Peter Stone | Mobile Robot Planning using Action Language BC with Hierarchical Domain Abstractions | ASPOCP | | Jul 23 12:10 |
| Gilles Audemard, Benoît Hoessen, Saïd Jabbour and Cédric Piette | Dolius: A Distributed Parallel SAT Solving Framework | POS | | Jul 13 09:15 |
| Marijn Heule, Norbert Manthey and Tobias Philipp | Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers | POS | | Jul 13 09:45 |
| Laurent Simon | Post Mortem Analysis of SAT Solver Proofs | POS | | Jul 13 10:45 |
| Zoltan Mann and Pal Papp | Formula partitioning revisited | POS | | Jul 13 11:15 |
| Norbert Manthey and Enrique Alfonso | New CNF Features and Formula Classification | POS | | Jul 13 11:45 |
| Zoltan Mann | Typical-case complexity and the SAT competitions | POS | | Jul 13 12:15 |
| Armin Biere | Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling | POS | | Jul 13 14:30 |
| Norbert Manthey, Peter Steinke, Steffen Hölldobler and Tobias Philipp | Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers | POS | | Jul 13 15:30 |
| David Monniaux | How do we get Inductive Invariants? | CAV | | Jul 18 08:45 |
| Fabio Somenzi | Hardware Model Checking | CAV | | Jul 18 14:30 |
| Erik Winfree | Designing and Verifying Molecular Circuits and Systems Made of DNA | CAV | | Jul 19 17:10 |
| Rance Cleaveland | Automated Testing | CAV | | Jul 20 17:10 |
| Rajeev Alur, Dana Fisman, Rishab Singh and Armando Solar-Lezama | The First Syntax-Guided Synthesis Competition (SyGuS-COMP 2014) | CAV | | Jul 19 12:55 |
| Armin Biere and Keijo Heljanko | Hardware Model Checking Competition CAV 2014 Edition | CAV | | Jul 20 14:30 |
| Roderick Bloem, Rüdiger Ehlers and Swen Jacobs | SYNTCOMP - Synthesis Competition for Reactive Systems | CAV | | Jul 21 12:55 |
| Jean-Christophe Filliatre, Léon Gondelman and Andrei Paskevich | The Spirit of Ghost Code | CAV | | Jul 19 10:45 |
| Anvesh Komuravelli, Arie Gurfinkel and Sagar Chaki | SMT-based Model Checking for Recursive Programs | CAV | | Jul 19 11:05 |
| Shachar Itzhaky, Nikolaj Bjorner, Thomas Reps, Mooly Sagiv and Aditya Thakur | Property-Directed Shape Analysis | CAV | | Jul 19 11:25 |
| Quang Loc Le, Cristian Gherghina, Shengchao Qin and Wei-Ngan Chin | Shape Analysis via Second-Order Bi-Abduction | CAV | | Jul 19 11:45 |
| Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider | ICE: A Robust Learning Framework for Synthesizing Invariants | CAV | | Jul 19 12:05 |
| Rahul Sharma and Alex Aiken | From Invariant Checking to Invariant Inference Using Randomized Search | CAV | | Jul 19 12:25 |
| Zvonimir Rakamaric and Michael Emmi | SMACK: Decoupling Source Language Details from Verifier Implementations | CAV | | Jul 19 12:45 |
| Hassan Eldib and Chao Wang | Synthesis of Masking Countermeasures against Side Channel Attacks | CAV | | Jul 19 14:30 |
| Omar Chowdhury, Limin Jia, Deepak Garg and Anupam Datta | Temporal Mode-Checking for Runtime Monitoring of Privacy Policies | CAV | | Jul 19 14:50 |
| Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Reummer and Jari Stenman | String Constraints for Verification | CAV | | Jul 19 15:10 |
| Sudeep Kanav, Peter Lammich and Andrei Popescu | A Conference Management System with Verified Document Confidentiality | CAV | | Jul 19 15:30 |
| Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen and Gennaro Parlato | VAC - Verifier of Administrative Role-based Access Control Policies | CAV | | Jul 19 15:50 |
| Javier Esparza and Jan Kretinsky | From LTL to Deterministic Automata: A Safraless Compositional Approach | CAV | | Jul 19 16:30 |
| Loris D'Antoni and Rajeev Alur | Symbolic Visibly Pushdown Automata | CAV | | Jul 19 16:50 |
| Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair Donaldson, Jeroen Ketema, Dan Liew and Shaz Qadeer | Engineering a Static Verification Tool for GPU Kernels | CAV | | Jul 20 10:45 |
| Kenneth McMillan | Lazy Annotation Revisited | CAV | | Jul 20 11:05 |
| Yakir Vizel and Arie Gurfinkel | Interpolating Property Directed Reachability | CAV | | Jul 20 11:25 |
| Jesse Bingham and Joe Leslie-Hurd | Verifying Relative Error Bounds using Symbolic Simulation | CAV | | Jul 20 11:45 |
| Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi and Darko Marinov | Regression Test Selection for Distributed Software Histories | CAV | | Jul 20 12:05 |
| Anton Wijs, Joost-Pieter Katoen and Dragan Bosnacki | GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components | CAV | | Jul 20 12:25 |
| Dirk Beyer, Georg Dresler and Philipp Wendler | Software Verification in the Google App-Engine Cloud | CAV | | Jul 20 12:45 |
| Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri and Stefano Tonetta | The nuXmv Symbolic Model Checker | CAV | | Jul 20 12:55 |
| Hillel Kugler, Nicola Paoletti, Boyan Yordanov, Youssef Hamadi and Christoph M. Wintersteiger | Analyzing and Synthesizing Genomic Logic Functions | CAV | | Jul 20 14:40 |
| Byron Cook, Jasmin Fisher, Benjamin Hall, Samin Ishtiaq, Garvit Juniwal and Nir Piterman | Finding instability in biological models | CAV | | Jul 20 15:00 |
| Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra and Marta Kwiatkowska | Invariant verification of nonlinear hybrid automata networks of cardiac cells | CAV | | Jul 20 15:20 |
| Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen and Jun Sun | Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions | CAV | | Jul 20 15:40 |
| Willem Hagemann | Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections | CAV | | Jul 20 16:30 |
| Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta | Verifying LTL properties of hybrid systems with K-liveness | CAV | | Jul 20 16:50 |
| Rodica Bozianu, Catalin Dima and Emmanuel Filiot | Safraless Synthesis for Epistemic Temporal Specifications | CAV | | Jul 21 10:45 |
| Tomas Brazdil, David Klaska, Antonin Kucera and Petr Novotný | Minimizing Running Costs in Consumption Systems | CAV | | Jul 21 11:05 |
| Krishnendu Chatterjee, Martin Chmelík and Przemyslaw Daca | CEGAR for Qualitative Analysis of Probabilistic Systems | CAV | | Jul 21 11:25 |
| Thomas Dillig, Isil Dillig and Swarat Chaudhuri | Optimal Guard Synthesis for Memory Safety | CAV | | Jul 21 11:45 |
| Jade Alglave, Daniel Kroening, Vincent Nimal and Daniel Poetzl | Don't sit on the fence: A static analysis approach to automatic fence insertion | CAV | | Jul 21 12:05 |
| Petr Čermák, Alessio Lomuscio, Fabio Mogavero and Aniello Murano | MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications | CAV | | Jul 21 12:25 |
| Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Walker | Solving Games without Controllable Predecessor | CAV | | Jul 21 12:35 |
| Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess and Stefan Stattelmann | G4LTL-ST: Automatic Generation of PLC Programs | CAV | | Jul 21 12:45 |
| Mohsen Lesani, Todd Millstein and Jens Palsberg | Automatic Atomicity Verification for Clients of Concurrent Data Structures | CAV | | Jul 21 14:30 |
| Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach | Regression-free Synthesis for Concurrency | CAV | | Jul 21 14:50 |
| Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre and Gennaro Parlato | Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization | CAV | | Jul 21 15:10 |
| Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer and Filip Niksic | An SMT-based Approach to Coverability Analysis | CAV | | Jul 21 15:30 |
| Alejandro Sanchez and Cesar Sanchez | LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes | CAV | | Jul 21 15:50 |
| Margus Veanes, Nikolaj Bjorner, Lev Nachmanson and Sergey Bereg | Monadic Decomposition | CAV | | Jul 22 10:45 |
| Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett and Morgan Deters | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions | CAV | | Jul 22 11:05 |
| Alexander Nadel | Bit-Vector Rewriting with Automatic Rule Generation | CAV | | Jul 22 11:25 |
| Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli and Kshitij Bansal | A Tale of Two Solver: Eager and Lazy Approaches to Bit-vectors | CAV | | Jul 22 11:45 |
| Andrei Voronkov | AVATAR: The New Architecture for First-Order Theorem Provers | CAV | | Jul 22 12:05 |
| Ruzica Piskac, Thomas Wies and Damien Zufferey | Automating Separation Logic with Trees and Data | CAV | | Jul 22 12:25 |
| Ashish Tiwari and Patrick Lincoln | A Nonlinear Real Arithmetic Fragment | CAV | | Jul 22 12:45 |
| Bruno Dutertre | Yices 2.2 | CAV | | Jul 22 12:55 |
| Moritz Sinn, Florian Zuleger and Helmut Veith | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis | CAV | | Jul 22 14:30 |
| Ravichandhran Madhavan and Viktor Kuncak | Symbolic Resource Bound Inference for Functional Programs | CAV | | Jul 22 14:50 |
| Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio | Proving Non-termination Using Max-SMT | CAV | | Jul 22 15:10 |
| Matthias Heizmann, Jochen Hoenicke and Andreas Podelski | Termination Analysis by Learning Terminating Programs | CAV | | Jul 22 15:30 |
| Andrey Kupriyanov and Bernd Finkbeiner | Causal Termination of Multi-threaded Programs | CAV | | Jul 22 15:50 |
| Johannes Birgmeier, Aaron R. Bradley and Georg Weissenbacher | Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) | CAV | | Jul 22 16:40 |
| Suho Lee and Karem A. Sakallah | Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction | CAV | | Jul 22 17:00 |
| Arlen Cox, Bor-Yuh Evan Chang and Sriram Sankaranarayanan | QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers | CAV | | Jul 22 17:20 |