VSL 2014: VIENNA SUMMER OF LOGIC 2014

A
Abdallah, Samer	(PLP) Exploring probabilistic grammars of symbolic music using PRISM
Abdulla, Parosh Aziz	(CAV) Program Verification through String Rewriting (CSL-LICS) Infinite-State Energy Games (iPRA) Towards Craig Interpolation for String Constraints
Abeille, Anne	(NLCS) TBA
Abel, Andreas	(UNIF) A Categorical Perspective on Pattern Unification (Extended Abstract) (RTA-TLCA) Unnesting of Copatterns
Abou-Msabah, Slimane	(RCRA) An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Abrantes, Mário	(ICLP) Properties of Stable Model Semantics Extensions
Abreu, Salvador	(ParSearchOpt) Towards a Parallel Hierarchical Adaptive Solver Tool (CICLOPS-WLPE) Extending the Finite Domain Solver of GNU Prolog
Abrial, Jean-Raymond	(APPA) Program Verification (B Method)
Abseher, Michael	(LaSh) The D-FLAT System for Dynamic Programming on Tree Decompositions (ASPOCP) Computing Secure Sets in Graphs using Answer Set Programming
Acar, Erman	(PRUV) Multi-Attribute Decision Making using Weighted Description Logics
Accattoli, Beniamino	(2FC) On the Value of Variables (IWC) On the Formalization of Lambda-Calculus Confluence and Residuals (CSL-LICS) Beta Reduction is Invariant, Indeed (HOR) Distilling Abstract Machines
Achilleos, Antonis	(LC) Complexity bounds for Multiagent Justification Logic (LCC) Closing a Gap in the Complexity of Refinement Modal Logic
Achref, El Mouelhi	(CSPSAT) Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms
Acquisti, Alessandro	(CSF) Privacy in the Age of Augmented Reality
Adje, Assale	(NSV) Policy iteration in finite templates domain
Adão, Pedro	(CSF) Mignis: A semantic based tool for firewall configuration
Affeldt, Reynald	(Coq) Formalization of Error-correcting Codes using SSReflect
Aguzzoli, Stefano	(LATD) A method for generalizing finite automata arising from Stone-like dualities
Ahmetaj, Shqiponja	(DL) Planning Problems for Graph Structured Data in Description Logics
Ahmeti, Albin	(DL) SPARQL Update for Materialized Triple Stores under DL-Lite_RDFS Entailment
Ahrendt, Wolfgang	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs
Ahrens, Benedikt	(DTP) Terminal semantics for codata types in intensional Martin-Löf type theory
Aiken, Alex	(CAV) From Invariant Checking to Invariant Inference Using Randomized Search
Aisenberg, James	(PC) Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets
Ait-Mokhtar, Salah	(KR4HC) Semantic Representation of Evidence-based Clinical Guidelines
Akinyele, Joseph Ayo	(CSF) Certified Synthesis of Efficient Batch Verifiers
Akiyoshi, Ryota	(LC) Proof-Theoretic Analysis of Brouwer's Argument of the Bar Induction
Al-Sibahi, Ahmad Salim	(DTP) Scrapping Your Dependently-Typed Boilerplate is Hard
Alaev, Pavel	(LC) The $ \Delta^{0}_{\alpha} $-dimension of computable structures
Alama, Jesse	(ARQNL) Dialogues for proof search
Albarghouthi, Aws	(iPRA) Specification Synthesis via Generalized Abduction
Alberti, Francesco	(FRIDA) Monotonic Abstraction Techniques: from Parametric to Software Model Checking (SMT) Decision Procedures for Flat Array Properties
Albuquerque, Hugo	(LATD) Generalizing the Leibniz and Suszko operators
Aleksandrova, Svetlana	(LC) Uniformization in the hereditarily finite list superstructure over the real exponential field
Alferes, Jose Julio	(ICLP) Transaction Logic with (Complex) Events
Alfonso, Enrique	(POS) New CNF Features and Formula Classification
Alglave, Jade	(CAV) Don't sit on the fence: A static analysis approach to automatic fence insertion (REORDER) Panel session
Ali, Asad	(WWV) Static Enforcement of Role-Based Access Control
All Workshop Presenters,	(ParSearchOpt) General Panel Discussion
Allender, Eric	(LCC) 27 and still counting: Iterated product, inductive counting, and the structure of P
Alonso, Jose-Ramon	(KR4HC) Training residents in the application of clinical guidelines for differential diagnosis of the most frequent causes of arterial hypertension with decision tables
Alsubait, Tahani	(DL) Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure?
Altenkirch, Thorsten	(LFMTP) Some constructions on ω-groupoids
Altukhov, Victor	(FRIDA) Models and techniques for verification of Software Defined Networks
Alur, Rajeev	(CAV) Symbolic Visibly Pushdown Automata (CAV) Syntax-Guided Synthesis Competition Results (CSL-LICS) Regular Combinators for String Transformations (SYNT) The 1st Syntax-Guided Synthesis Competition (SyGuS)
Alves, Péricles	(WST) Real-world loops are easy to predict : a case study
Alves, Sandra	(ITRS) Liquid Intersection Types (PAS) Confluence of Pattern-Based Calculi with Finitary Matching
Alviano, Mario	(ICLP) Anytime Computation of Cautious Consequences in Answer Set Programming (ASPOCP) On the Implementation of Weak Constraints in WASP (RCRA) Declarative Specification of Benchmark Sessions via ASP (NMR) Semantics and Compilation of Answer Set Programming with Generalized Atoms (NMR) Preliminary Report on WASP 2
Alvim, Mario	(FCS-FCC) Adversary Gain vs. Defender Loss in Quantified Information Flow (CSF) Additive and multiplicative notions of leakage, and their capacities
Amadini, Roberto	(ICLP) SUNNY: a Lazy Portfolio Approach for Constraint Solving
Amblard, Maxime	(NLCS) Algebraic Effects and Handlers in Natural Language Interpretation
Aminof, Benjamin	(AISS) Parameterized Model Checking of Rendezvous Systems
Amir, Eyal	(KR) Tracking Beliefs and Intentions in the Werewolf Game
Amla, Nina	(VSL) FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?
Amsden, Edward	(DTP) Type-Directed Editing for Dependently-Typed Programs.
Anand, Abhishek	(ITP) Towards a Formally Verified Proof Assistant (LFMTP) A Generic Approach to Proofs about Substitution
Andréka, Hajnal	(LC) Weak Beth definability property for finite variable fragments.
Angelopoulos, Nicos	(PLP) Welcome (PLP) Discussion on the implementation of PLP systems.
Angione, Claudio	(HSB) Bayesian Design for Whole Cell Synthetic Biology Models
Ansótegui, Carlos	(IJCAR) The Fractal Dimension of SAT Formulas
Antic, Christian	(ICLP) On Cascade Products of Answer Set Programs
Antidze, Nino	(NCPROOFS) Construction and meaning
Antoniotti, Marco	(HSB) Tutorial: The Cellular Potts Model
Antoniou, Grigoris	(ICLP) Efficient Computation of the Well-Founded Semantics over Big Data (DL) Rational Elimination of DL-Lite TBox Axioms (ASPOCP) Computing Answer Sets for Monadic Logic Programs via MapReduce (RCRA) Efficient Computation of the Well-Founded Semantics over Big Data
Antonopoulos, Timos	(LCC) First-Order Logic of Order and Metric has the Three-Variable Property
Antonova, Olga	(LC) Aristotle’s conception of demonstration and modern proof theory
Antonutti Marfori, Marianna	(LC) Justifying proof-theoretic reflection principles
Antoy, Sergio	(TermGraph) Needed Computations Shortcutting Needed Steps
Aoto, Takahito	(IWC) Confluence Competition (IFIP-WG16) Decision Procedures for Proving Inductive Theorems without Induction (RTA-TLCA) Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams
Appel, Andrew	(CSF) Portable Software Fault Isolation
Apt, Krzysztof	(LC) Tutorial on Stategic and Extensive Games 3 (LC) Tutorial on Stategic and Extensive Games 2 (LC) Tutorial on Stategic and Extensive Games 1
Aravantinos, Vincent	(ITP) Implicational Rewriting Tactics in HOL (ITP) Formal Verification of Optical Quantum Flip Gate
Arbelaez, Alejandro	(ParSearchOpt) A Constraint-based Parallel Local Search for Disjoint Rooted Distance-Constrained Minimum Spanning Tree Problem (ParSearchOpt) On the Parallelization of Randomized Propagation-based Constraint Solving
Areias, Miguel	(ICLP) A Simple and Efficient Lock-Free Hash Trie Design for Concurrent Tabling
Arenas, Marcelo	(DL) On Faceted Search over Knowledge Bases
Arhami, Negin	(PAAR) The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics
Arieli, Ofer	(GeTFun) Combining non-determinism and context awareness in consistency restoration systems
Arlt, Stephan	(VeriSure) Quantification of Verification Progress
Armas Romero, Ana	(DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs
Armengol, Eva	(PRUV) Learning Preferences for Collaboration
Armstrong, J Douglas	(HSB) Integration of rule-based models and compartmental models of neurons (HSB) RKappa: Statistical sampling suite for Kappa models.
Armstrong, Robert C.	(NSV) Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics
Artale, Alessandro	(DL) Temporal OBDA with LTL and DL-Lite
Artemov, Sergei	(LC) An outline of intuitionistic epistemic logic
Arthan, Rob	(GSB) On Affine Logic and Łukasiewicz Logic (ITP) HOL with Definitions: Semantics, Soundness, and a Verified Implementation (ITP) HOL Constant Definitions Done Right (LATD) On Pocrims and Hoops
Asarin, Eugene	(CSL-LICS) Asymptotic behaviour in temporal logic
Aschenbrenner, Matthias	(LC) Logic meets number theory in o-minimality
Aschieri, Federico	(CLC) A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
Askarov, Aslan	(CSF) Declarative Policies for Capability Control
Asuncion, Vernon	(KR) Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness
Atif, Jamal	(KR) Concept Dissimilarity with Triangle Inequality
Atig, Mohamed Faouzi	(CAV) Program Verification through String Rewriting (CSL-LICS) Infinite-State Energy Games (iPRA) Towards Craig Interpolation for String Constraints
Atserias, Albert	(PC) Narrow Proofs May Be Maximally Long (PC) Weak Pigeonhole Principles, Circuits for Approximate Counting, and Bounded-Depth Proofs
Aubert, Clément	(RTA-TLCA) Unification and Logarithmic Space
Aucher, Guillaume	(KR) Axioms .2 and .4 as Interaction Axioms
Audemard, Gilles	(SAT) Impact of Community Structure on SAT Solver Performance (SAT) Lazy clause exchange policy for parallel SAT solvers (POS) Dolius: A Distributed Parallel SAT Solving Framework
Avanzini, Martin	(2FC) Automated Complexity Analysis of Term Rewrite Systems (WST) Type Introduction for Runtime Complexity Analysis
Avigad, Jeremy	(ITP) A heuristic prover for real inequalities (Isabelle) A formally verified proof of the Central Limit Theorem
Avron, Arnon	(GeTFun) Effective first-order reasoning about incomplete and inconsistent information
Avron, Arnon	(LC) Predicative Mathematics via Safety Relations (GeTFun) Semi-implication and matrices (LATD) A Semi-relevant, Paraconsistent Dual of {\L}ukasiewicz Logic (LATD) Cut-free calculus for second-order {G\"odel} logic
Awad, Edmond	(KR) Interval Methods for Judgment Aggregation in Argumentation
Ayala Rincón, Mauricio	(IFIP-WG16) Discussion on the International School on Rewriting (ISR)
Aziz, Rehan Abdul	(ICLP) Grounding Bound Founded Answer Set Programs (ICLP) Bound Founded Answer Set Programming
Azmy, Noran	(FRIDA) Having SPASS with Pastry and TLA+
B
Baader, Franz	(VSL) VSL Keynote Talk: Ontology-Based Monitoring of Dynamic Systems (UNIF) Matching with respect to general concept inclusions in the Description Logic EL (DL) Matching with respect to general concept inclusions in the Description Logic EL (LATD) Tutorial: Fuzzy Description Logics (Part 1) (LATD) Tutorial: Fuzzy Description Logics (Part 2)
Baaz, Matthias	(VSL) Welcome Address by the Organizers
Baaz, Matthias	(NCPROOFS) The Epsilon Calculus and Nonclassical Logics
Baaz, Matthias	(NCPROOFS) Construction and meaning
Babb, Joseph	(ASPOCP) Action Language BC+: Preliminary Report
Bacchus, Fahiem	(VSL) FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (QUANTIFY) Algorithmic Paradigms for Solving QBF (CAV) Solving Games without Controllable Predecessor (SAT) Cores in Core based MaxSat Algorithms: an Analysis (CSPSAT) Invited talk: MaxSat and SoftCSPs
Backes, Michael	(CSF) TUC: Time-sensitive and Modular Analysis of Anonymous Communication
Badaev, Serikzhan	(LC) Relativized universal numberings
Bae, Kyungmin	(RTA-TLCA) Predicate Abstraction of Rewrite Theories
Baget, Jean-François	(NMR) Revisiting Chase Termination for Existential Rules and their Extension to Nonmonotonic Negation
Bagheri Hariri, Babak	(KR) State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems
Bagnol, Marc	(SD) A Correctness Criterion Free from Switchings (RTA-TLCA) Unification and Logarithmic Space
Baier, Christel	(CSL-LICS) Weight Monitoring with Linear Temporal Logic: Complexity and Decidability (CSL-LICS) Trade-Off Analysis Meets Probabilistic Model Checking
Baier, Jorge	(KR) Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals
Baioletti, Marco	(RCRA) A Discrete Differential Evolution Algorithm for the Total Flowtime Flowshop Scheduling Problem
Balabanov, Valeriy	(SAT) QBF Resolution Systems and their Proof Complexities (QBF) Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Balai, Evgenii	(ASPOCP) Epistemic Logic Programs with Sorts
Balaz, Martin	(ICLP) On Strong and Default Negation in Answer-Set Program Updates (NMR) On Strong and Default Negation in Logic Program Updates
Balbiani, Philippe	(UNIF) Unification in the normal modal logic Alt1 (ADDCT) Decidability of Iteration-free PDL with Parallel Composition
Baldi, Paolo	(GSB) A proof theoretic approach to standard completeness
Balduccini, Marcello	(ICLP) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments (NMR) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments: Progress Report
Baldwin, John T.	(LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes (INFINITY) When excellence and local finiteness collide (INFINITY) Interactions of Set Theory, $L_{\omega_1,\omega}$, and AEC
Balint, Adrian	(SAT) Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses
Balyo, Tomáš	(SAT) Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
Ban Kirigin, Tajana	(FCS-FCC) Towards Timed Models for Cyber-Physical Security Protocols
Bana, Gergei	(FCS-FCC) Protocol Indistinguishability and the Computationally Complete Symbolic Attacker (FCS-FCC) Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model
Banbara, Mutsunori	(POS) Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
Banerjee, Anindya	(VSTTE) A logical analysis of framing for specifications with pure method calls
Bansal, Kshitij	(CAV) A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors
Barceló, Pablo	(CSL-LICS) Graph Logics with Rational Relations: The Role of Word Combinatorics
Bardsley, Ethel	(CAV) Engineering a Static Verification Tool for GPU Kernels
Barlatier, Patrick	(DTP) A Unifying Framework for Primitive Ontological Relations in Dependent Type Theory
Barnes, Chris P	(VEMDP) An Aspect Oriented Design and Modelling Framework for Synthetic Biology
Barrett, Clark	(APPA) Proofs in Satisfiability Modulo Theories (CAV) A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (CAV) A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (SMT) SMT: Where do we go from here? (SMT) Leveraging Linear and Mixed Integer Programming for SMT
Bartak, Roman	(ICLP) Using Tabled Logic Programming to Solve the Petrobras Planning Problem (ICLP) Constraint Logic Programming II (ICLP) Constraint Logic Programming I
Barthe, Gilles	(APPA) Security (CSF) Proving differential privacy in Hoare logic (CSF) New Directions in Computed-Aided Cryptography (CSF) Certified Synthesis of Efficient Batch Verifiers
Bartholomew, Michael	(KR) Stable Models of Multi-Valued Formulas: Partial vs. Total Functions
Bartocci, Ezio	(HSB) Bayesian Design for Whole Cell Synthetic Biology Models
Bartzia, Evmorfia-Iro	(ITP) A Formal Library for Elliptic Curves in the Coq Proof Assistant
Basaldella, Michele	(CLC) Infinitary Classical Logic: Recursive Equations and Interactive Semantics (Linearity) Ludics without Designs I: Triads
Basin, David	(CSL-LICS) Anchored LTL Separation
Basin, David	(CSF) Actor Key Compromise: Consequences and Countermeasures
Baskent, Can	(LG) Game Semantics for Some Non-Classical Logics
Basold, Henning	(PSC) Observational Equivalence for Behavioural Differential Equations
Bau, Alexander	(CSPSAT) SAT Compilation for Constraints over Finite Structured Domains (WST) Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling
Bauer, Andrej	(LC) Reductions in computability theory from a constructive point of view
Bauer, Lujo	(CSF) Panel: Usability
Baumann, Ringo	(NMR) Compact Argumentation Frameworks
Baumgartner, Alexander	(UNIF) Nominal Anti-Unification
Baumgartner, Peter	(IJCAR) Finite Quantification in Hierarchic Theorem Proving
Bauters, Kim	(KR) Using Answer Set Programming for Solving Boolean Games
Bax, Joshua	(IJCAR) Finite Quantification in Hierarchic Theorem Proving (PAAR) A Model Guided Instantiation Heuristic for the Superposition Calculus with Theories
Bazhenov, Nikolay	(LC) Boolean algebras and degrees of autostability relative to strong constructivizations
Becker, Bernd	(QBF) Incremental QBF Reasoning for the Verification of Partial Designs
Beckert, Bernhard	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs (UITP) How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers (ARW-DT) Towards Evaluating the Usability of Interactive Theorem Provers (VERIFY) Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Beckmann, Arnold	(PC) Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time (PC) Parity games and propositional proofs (LCC) LCC'14 Opening Remarks (INFINITY) Set functions with small circuits (INFINITY) Proof Theoretic Characterisations of Feasible Set Functions (INFINITY) Cobham Recursive Set Functions (LATD) Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences
Bedregal, Benjamín	(GeTFun) Semi-BCI-algebras (GeTFun) On non-deterministic fuzzy negations
Bedrosian, Geghard	(LC) Ultraproduct construction of representative utility functions with infinite-dimensional domain
Beek, Wouter	(KR) Rough Set Semantics for Identity on the Web
Beeson, Michael	(IJCAR) Otter proofs of theorems in Tarskian geometry (QED) Mixing proofs and computations
Beffara, Emmanuel	(CLC) A proof-theoretic view on scheduling in concurrency
Behounek, Libor	(PRUV) In Which Sense Is Fuzzy Logic a Logic for Vagueness? (LATD) Church-style type theories over finitary weakly implicative logics
Beierle, Christoph	(PRUV) Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics
Beillahi, Sidi Mohamed	(FWFM) Towards the Application of Formal Methods in Process Engineering
Belanger, David	(LC) A non-uniqueness theorem for jumps of principal ideals
Belardinelli, Francesco	(KR) Satisfiability of Alternating-time Temporal Epistemic Logic through Tableaux
Belle, Vaishak	(KR) On the Progression of Knowledge in Multiagent Systems (KR) How To Progress Beliefs in Continuous Domains
Bellodi, Elena	(ICLP) Lifted Variable Elimination for Probabilistic Logic Programming
Belov, Anton	(SAT) MUS Extraction using Clausal Proofs
Benda, Thomas	(LC) Formalizing vagueness as a doxastic, relational concept
Bender, Markus	(ARW-DT) Combined Reasoning with Sets and Aggregation Functions
Benedikt, Michael	(CSL-LICS) Effective Interpolation and Preservation in Guarded Logics (DL) Invited Talk: New Perspectives on Query Reformulation
Benevides, Mario	(LC) On graph calculus approach to modalities
Benferhat, Salem	(KR) Reasoning with Uncertain Inputs in Possibilistic Networks
Bengtson, Jesper	(Coq) Automating Abstract Logics (Coq) Coqoon: towards a modern IDE for Coq (LFMTP) Session Types Meet Separation Logic
Benke, Marcin	(ITRS) Lucretia — intersection type polymorphism for scripting languages
Benton, Nick	(LOLA) De haut en bas: relating high-level and low-level abstractions
Benveniste, Albert	(RS) Contracts for System Design
Benzmüller, Christoph	(APPA) Higher-Order Automated Theorem Provers (ARQNL) HOL Provers for First-order Modal Logics --- Experiments (ARQNL) Open Discussion (ARW-DT) The Leo-III Project
Berardi, Stefano	(PSC) Effective Bounds on the Podelski-Rybalchenko Termination Theorem (RTA-TLCA) Ramsey Theorem as an intuitionistic property of well founded relations
Berdine, Josh	(IJCAR) Computing All Implied Equalities via SMT-based Partition Refinement
Bereg, Sergey	(CAV) Monadic Decomposition
Berg, Jeremias	(LaSh) Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability (RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
Berger, Ulrich	(NLCS) Program Extraction Applied to Monadic Parsing (PSC) Extracting Monadic Parsers from Proofs (PSC) Program extraction in Church's simple theory of types (invited talk)
Bernardo, Marco	(CSL-LICS) On the Discriminating Power of Passivation and Higher-Order Interaction
Beros, Achilles	(LC) A DNC function that computes no effectively bi-immune set
Beros, Konstantinos	(LC) Co-analytic ideals on $\omega$
Bertossi, Leopoldo	(NMR) Causality in Databases: The Diagnosis and Repair Connections
Berwanger, Dietmar	(LG) Game Reductions
Besnard, Philippe	(NMR) Revisiting Postulates for Inconsistency Measures
Bessai, Jan	(ITRS) Delegation-based Mixin Composition Synthesis
Betts, Adam	(CAV) Engineering a Static Verification Tool for GPU Kernels
Beyan, Oya	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Beyer, Dirk	(CAV) Software Verification in the Google App-Engine Cloud
Beyersdorff, Olaf	(IJCAR) The Complexity of Theorem Proving in Circumscription and Minimal Entailment (SAT) Unified characterisations of resolution hardness measures (PC) Opening (NMR) Tableau vs. Sequent Calculi for Minimal Entailment
Bezem, Marc	(CHR) Coherent Logic and Applications
Bezerra Silva, George	(ARW-DT) A Resolution-Based Prover for Normal Modal Logics
Bezhanishvili, Nick	(LATD) Canonical formulas for k-potent residuated lattices
Bhatt, Mehul	(KR) Computing Narratives of Cognitive User Experience for Building Design Analysis: KR for Industry Scale Computer-Aided Architecture Design
Bi, Yi	(ICLP) A Well-Founded Semantics for FOL-Programs
Bianchi, Matteo	(LATD) Trakhtenbrot theorem and first-order axiomatic extensions of MTL
Bichhawat, Abhishek	(FCS-FCC) Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis
Bienvenu, Meghyn	(KR) Nested Regular Path Queries in Description Logics (DL) Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries (DL) Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics
Biere, Armin	(VSL) FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (QUANTIFY) EPR Encodings of Bit-Vector Problems Even With Quantifiers (CAV) Hardware Model Checking Competition 2014 CAV Edition (IJCAR) A Unified Proof System for QBF Preprocessing (SAT) Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses (SAT) Detecting cardinality constraints in CNF (SAT) Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask) (LCC) On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic (Vampire) SAT solving experiments in Vampire (POS) iDQ: Instantiation-Based DQBF Solving (POS) Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver Lingeling
Bikmukhametov, Ravil	(LC) On $\Sigma^0_2$-initial segments of computable linear orders
Bilokon, Paul	(CSL-LICS) A domain-theoretic approach to Brownian motion and general continuous stochastic processes
Bingham, Jesse	(CAV) Verifying Relative Error Bounds using Symbolic Simulation
Birgmeier, Johannes	(CAV) Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
Birkedal, Lars	(RTA-TLCA) A Model of Countable Nondeterminism in Guarded Type Theory
Bisping, Benjamin	(FRIDA) Mechanical Verification of a Constructive Proof for FLP
Bizjak, Aleš	(RTA-TLCA) A Model of Countable Nondeterminism in Guarded Type Theory
Bjorndahl, Adam	(KR) Axiomatizing Rationality
Bjorner, Nikolaj	(QUANTIFY) Quantifier Projection (CAV) Property-Directed Shape Analysis (CAV) Monadic Decomposition (IJCAR) Computing All Implied Equalities via SMT-based Partition Refinement
Bjørdal, Frode	(LATD) Truth degrees in the interval [-1,1] for the librationist system $\pounds$.
Blackburn, Patrick	(DL) Invited Talk: Fragments of Logic, Language, and Computation
Blanchette, Jasmin Christian	(IJCAR) Unified Classical Logic Completeness: A Coinductive Pearl (ITP) Cardinals in Isabelle/HOL (ITP) Truly Modular (Co)datatypes for Isabelle/HOL (Vampire) My Life with an Automatic Theorem Prover (Isabelle) Primitively (Co)recursive Definitions for Isabelle/HOL
Blanchette, Patricia	(LC) Frege on mathematical progress (LC) The Birth of Semantic Entailment
Blasum, Holger	(VeriSure) Implicit Assumptions in a Model for Separation Kernels (Isabelle) Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
Blazy, Sandrine	(ITP) Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
Bliem, Bernhard	(LaSh) The D-FLAT System for Dynamic Programming on Tree Decompositions (ASPOCP) Computing Secure Sets in Graphs using Answer Set Programming
Bloch, Isabelle	(KR) Concept Dissimilarity with Triangle Inequality
Block, Alexander	(LC) A new lower bound for the length of the hierarchy of norms
Bloem, Roderick	(CAV) SYNTCOMP - Synthesis Competition for Reactive Systems (SYNT) Parameterized Synthesis Case Study: AMBA AHB (SYNT) How to Handle Assumptions in Synthesis
Bloemen, Vincent	(CICLOPS-WLPE) Extending the Finite Domain Solver of GNU Prolog
Blumensath, Achim	(CSL-LICS) Two-Way Cost Automata and Cost Logics over Infinite Trees
Bobed, Carlos	(ORE) Android Went Semantic: Time for Evaluation
Bobillo, Fernando	(DL) A MILP-based decision procedure for the (Fuzzy) Description Logic ALCB (ORE) Android Went Semantic: Time for Evaluation
Bochman, Alexander	(KR) Dynamic Causal Calculus
Bockelet, Michel	(CSL-LICS) Asymptotic behaviour in temporal logic
Boeing, Philip	(VEMDP) An Aspect Oriented Design and Modelling Framework for Synthetic Biology
Boender, Jaap	(STAST) Modeling Human Behaviour with Higher Order Logic: Insider Threats
Bogaerts, Bart	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories (ICLP) C-Log: A Knowledge Representation Language of Causality (CSPSAT) BreakIDGlucose: on the importance of row symmetry (LaSh) Lazy Model Expansion: Interleaving Grounding with Search (LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development (NMR) Inference in the FO(C) Modelling Language (NMR) FO(C) and Related Modelling Paradigms
Bogdanov, Dan	(CSF) From input private to universally composable secure multiparty computation primitives
Bohy, Aaron	(SYNT) Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
Bojanczyk, Mikolaj	(CSL-LICS) Decomposition Theorems and Model-Checking for the Modal mu-calculus
Bolibekyan, Hovhannes	(LC) On the compactness theorem in many valued logics
Bollig, Benedikt	(CSL-LICS) Logic for Communicating Automata with Parameterized Topology (CSL-LICS) Logical Characterization of Weighted Pebble Walking Automata
Bolotov, Alexander	(ARW-DT) Socratic Proofs for Propositional Linear-Time Logic
Bonacina, Ilario	(PC) Total Space in Resolution
Bonacina, Maria Paola	(UNIF) Constraint Manipulation in SGGS (IFIP-WG16) Semantically-Guided Goal-Sensitive Theorem Proving (PAAR) SGGS Theorem Proving: an Exposition
Bonchi, Filippo	(CSL-LICS) Coinduction Up-To in a Fibrational Setting
Bonchis, Cosmin	(DCM) Interactive Particle Systems and Random Walks on Hypergraphs
Bond, Mike	(ASA) Security APIs for Device Enrolment
Bonet, Maria Luisa	(IJCAR) The Fractal Dimension of SAT Formulas (PC) Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets
Boney, Will	(LC) Computing the number of types of infinite tuples
Bongini, Mattia	(LATD) Poof Search and Co-NP completeness for Many-Valued Logics
Bonichon, Richard	(SMT) Extending SMT-LIB v2 with lambda-terms and polymorphism
Bono, Viviana	(ITRS) Lucretia — intersection type polymorphism for scripting languages
Booth, Richard	(KR) Interval Methods for Judgment Aggregation in Argumentation (NMR) Abduction in Argumentation: Dialogical Proof Procedures and Instantiation
Borgwardt, Stefan	(KR) Decidable Gödel Description Logics without the Finitely-Valued Model Property (DL) Fuzzy DLs over Finite Lattices with Nominals (DL) Gödel Description Logics with General Models (DL) Gödel FL_0 with Greatest Fixed-Point Semantics (PRUV) Many-valued Horn Logic is Hard
Boricic, Branislav	(LC) An Intuitionistic Interpretation of Classical Implication
Boricic, Marija	(LC) Models for the probabilistic sequent calculus
Bormer, Thorsten	(VERIFY) Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Bortolussi, Luca	(HSB) Bayesian Design for Whole Cell Synthetic Biology Models
Bosnacki, Dragan	(CAV) GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
Botoeva, Elena	(KR) Query Inseparability for Description Logic Knowledge Bases (DL) Query Inseparability by Games
Botta, Nicola	(DTP) Sequential decision problems and a computational theory of avoidability
Bottazzi, Emanuele	(LC) Elementary numerosities and measures.
Bottrighi, Alessio	(KR4HC) META-GLARE: a meta-system for defining your own CIG system: Architecture and Acquisition (KR4HC) Conformance Analysis of the Execution of Clinical Guidelines with Basic Medical Knowledge and Clinical Terminology
Bou, Felix	(LATD) Introducing an exotic MTL-chain
Bouajjani, Ahmed	(FRIDA) On Checking Correctness of Concurrent Data Structures
Boudou, Joseph	(IJCAR) Skeptik [System Description] (ADDCT) Decidability of Iteration-free PDL with Parallel Composition
Boulmé, Sylvain	(VSTTE) A certifying frontend for (sub)polyhedral abstract domains
Bourgaux, Camille	(DL) Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics
Bourguet, Jean-Rémi	(ORE) TROvE: a Graphical Tool to Evaluate OWL Reasoners
Bourhis, Pierre	(DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs (DL) How to Best Nest Regular Path Queries
Bourke, Timothy	(ITP) Showing invariance compositionally for a process algebra for network protocols
Bova, Simone	(CSL-LICS) Model Checking Existential Logic on Partially Ordered Sets
Boyland, John	(LFMTP) Variable Arity for LF
Bozianu, Rodica	(CAV) Safraless Synthesis for Epistemic Temporal Specifications
Bozzato, Claudio	(CSF) Mignis: A semantic based tool for firewall configuration
Bozzato, Loris	(DL) Contextualized Knowledge Repositories with Justifiable Exceptions
Bozzelli, Laura	(IJCAR) Visibly Linear Temporal Logic
Bradley, Aaron R.	(CAV) Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
Brady, Edwin	(DTP) Sequential decision problems and a computational theory of avoidability (LFMTP) Idris: Implementing a Dependently Typed Programming Language
Bragaglia, Stefano	(ICLP) Multi-criteria optimal planning for Energy policies in CLP
Braibant, Thomas	(ITP) Compositional Computational Reflection (ASA) Well-typed generic smart-fuzzing for APIs
Brass, Stefan	(ICLP) A Framework for Bottom-Up Simulation of SLD-Resolution
Braud-Santoni, Nicolas	(FRIDA) Synthesis for Resilient Distributed Systems
Brayton, Robert	(VEMDP) Boolean modelling and formal verification of tiered-rate chemical reaction networks
Brazdil, Tomas	(CAV) Minimizing Running Costs in Consumption Systems (CSL-LICS) Zero-Reachability in Probabilistic Multi-Counter Automata
Brazma, Alvis	(HSB) Modeling and analysis of qualitative behavior of gene regulatory networks
Break,	(WPTE) Short break
Breathnach, Ciara	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Brenguier, Romain	(SYNT) AbsSynthe: abstract synthesis from succinct safety specifications
Brenguier, Romain	(CSL-LICS) The Complexity of Admissibility in Omega-Regular Games
Bresson, Jean	(IFIP-WG16) Rhythm Tree Rewriting
Breuvart, Flavien	(CSL-LICS) On the characterization of models of H*
Brewka, Gerhard	(ASPOCP) ``Are Preferences Giving You a Headache?'' - ``Take asprin!''
Briggs, Pam	(STAST) Decision justifications for wireless network selection
Britz, Arina	(DL) TBox abduction in ALC using a DL tableau (PRUV) Towards a Logic of Dilation
Brock-Nannestad, Taus	(SD) Substructural Cut Elimination (LFMTP) Hybrid Extensions in a Logical Framework (Linearity) Cut Elimination in Multifocused Linear Logic
Brockschmidt, Marc	(IJCAR) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (IJCAR) Proving Termination of Programs Automatically with AProVE
Brodmann, Paul-David	(FRIDA) Mechanical Verification of a Constructive Proof for FLP
Brotherston, James	(CSL-LICS) A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates
Brouette, Quentin	(LC) Differential Galois theory in the class of formally real fields.
Brown, Gavin	(KR) Predicting Performance of OWL Reasoners: Locally or Globally? (DL) Predicting OWL Reasoners: Locally or Globally?
Bruggink, Sander	(RTA-TLCA) Termination of Cycle Rewriting
Bruns, Daniel	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs
Bruyère, Véronique	(CSL-LICS) Secure Equilibria in Weighted Games (SYNT) Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
Bubel, Richard	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs (WING) A Theorem Prover Backed Approach to Array Abstraction
Bucciarelli, Antonio	(Linearity) The inhabitation problem for non-idempotent intersection
Buchberger, Bruno	(PAS) The Theorema Approach to Mathematics
Buchholtz, Ulrik	(INFINITY) Systems of Strength H(1)
Buchman, David	(KR) Relational Logistic Regression
Buchs, Didier	(FWFM) Introducing Formal Verification with Lego
Buckley, Oliver	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Bucur, Anca	(KR4HC) A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols
Bugliesi, Michele	(CSF) Provably Sound Browser-Based Enforcement of Web Session Integrity
Buiras, Pablo	(CSF) On Dynamic Flow-sensitive Floating-Label Systems
Bulatov, Andrei	(SAT) Approximating highly satisfiable random 2-SAT
Bundy, Alan	(CSL-LICS) Automating inductive proof
Bunte, Kerstin	(RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
Burel, Guillaume	(RTA-TLCA) Cut Admissibility by Saturation
Burnett, Heather	(NLCS) Mereological Comparatives in Delineation Semantics
Buss, Sam	(PC) Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets (LCC) Search problems, proof complexity, and second-order bounded arithmetic (INFINITY) Set functions with small circuits (INFINITY) Cobham Recursive Set Functions
Butterfield, Andrew	(VSTTE) Separation Kernel Verification: the XtratuM Case Study (UITP) UTP2: Higher-Order Equational Reasoning by Pointing
Béziau, Jean-Yves	(GeTFun) Non truth-functional bivalent logics extending classical bivalent logics
Böhl, Florian	(UITP) How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers (ARW-DT) Towards Evaluating the Usability of Interactive Theorem Provers
C
Cabalar, Pedro	(ICLP) Causal Graph Justifications of Logic Programs (KR) Strong Equivalence of Non-monotonic Temporal Theories (ASPOCP) Temporal Stable Models are LTL-representable
Cabrer, Leonardo Manuel	(UNIF) From Admissibility to a New Hierarchy of Unification Types (LATD) Classification of germinal MV-algebras
Cabrio, Elena	(NMR) Towards a Benchmark of Natural Language Arguments
Cadar, Cristian	(SMT) Multi-solver Support in Symbolic Execution
Cagnoli, Paolo	(ICLP) Multi-criteria optimal planning for Energy policies in CLP
Caianiello, Pasquale	(RCRA) Concept Learning by a Monte-Carlo Tree Search of Argumentations
Caleiro, Carlos	(GeTFun) Semi-BCI-algebras (GeTFun) On the characterization of broadly truth-functional logics
Calimeri, Francesco	(VSL) FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (ICLP) The Design of the Fifth Answer Set Programming Competition
Calvanese, Diego	(KR) Nested Regular Path Queries in Description Logics (KR) State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems (DL) Shape and Content: Incorporating Domain Knowledge into Shape Analysis (DL) Planning Problems for Graph Structured Data in Description Logics (DL) SPARQL Update for Materialized Triple Stores under DL-Lite_RDFS Entailment (DL) Expressive Identification Constraints to Capture Functional Dependencies in Description Logics (ORE) A Scalable Benchmark for OBDA Systems: Preliminary Report
Calzavara, Stefano	(CSF) Provably Sound Browser-Based Enforcement of Web Session Integrity
Caminati, Marco B.	(ARW-DT) Reasoning about Auctions
Campeotto, Federico	(ParSearchOpt) Towards a complete constraint solver on GPU
Cantone, Domenico	(ADDCT) On dual tableau-based decision procedures for relational fragments
Capelli, Florent	(SAT) Hypergraph Acyclicity and Propositional Model Counting
Cappai, Alberto	(FCS-FCC) Towards a Coinductive Characterization of Computational Indistinguishability
Carbone, Alessandra	(LSB) TBA
Cardelli, Luca	(VEMDP) Morphisms of reaction networks that couple structure to function
Carlos, Marcelo	(STAST) Modelling User Devices in Security Ceremonies
Carlsson, Mats	(SMT) Protocol log analysis with constraint programming
Caroprese, Luciano	(ICLP) A Measure of Arbitrariness in Abductive Explanations
Carral, David	(IJCAR) EL-ifying Ontologies (DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs
Carreiro, Facundo	(CSL-LICS) Weak MSO: Automata and Expressiveness Modulo Bisimilarity
Casadio, Claudia	(NLCS) Computing Italian clitic and relative clauses with tupled pregroups
Cashmore, Michael	(QUANTIFY) Encoding Reachability with Quantification
Castellan, Simon	(CSL-LICS) Symmetry in Concurrent Games
Castro, Sergio	(ICLP) Customisable Handling of Java References in Prolog Programs
Cavada, Roberto	(CAV) The nuXmv Symbolic Model Checker
Cerami, Marco	(DL) Complexity sources in FDL (PRUV) Many-valued Horn Logic is Hard
Cerans, Karlis	(HSB) Modeling and analysis of qualitative behavior of gene regulatory networks
Cerna, David	(CLC) Cut-Elimination in Schematic Proofs and Herbrand Sequents
Cerny, Pavol	(CAV) Regression-free Synthesis for Concurrency
Cerrito, Serenella	(IJCAR) Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
Cerutti, Federico	(KR) An SCC Recursive Meta-Algorithm for Computing Preferred Labellings in Abstract Argumentation (DL) Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information
Cervesato, Iliano	(CHR) Constraint Handling Rules with Multiset Comprehension Patterns (SMT) Reasoning About Set Comprehensions (LFMTP) Proof-Theoretic Foundations of Indexing in Logic Programming
Ceska, Milan	(VEMDP) Guiding the development of DNA walker systems to guarantee reliability and performance
Ceylan, İsmail İlkan	(IJCAR) The Bayesian Description Logic BEL (DL) Bayesian Description Logics
Chabane, Yahia	(DL) WApproximation: computing approximate answers for ontological queries
Chai, Ming	(LATD) Five-valued LTL for Runtime Verification
Chaki, Sagar	(CAV) SMT-based Model Checking for Recursive Programs
Chamarthi, Harsh Raju	(ACL2) Data Definitions in ACL2 Sedan
Chandra, Satish	(VSTTE) What Gives? A Hybrid Algorithm for Error Explanation
Chang, Bor-Yuh Evan	(CAV) QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
Chang, Liang	(DL) An ABox Revision Algorithm for the Description Logic EL_\bot
Chapman, Rod	(ITP) Invited talk: Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK
Chapoutot, Alexandre	(NSV) Transformation of a PID Controller for Numerical Accuracy
Charalambidis, Angelos	(ICLP) Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation (KR) Constructive Negation in Extensional Higher-Order Logic Programming
Charatonik, Witold	(CSL-LICS) Decidability of Weak Logics with Deterministic Transitive Closure
Charwat, Günther	(LaSh) The D-FLAT System for Dynamic Programming on Tree Decompositions (ASPOCP) Computing Secure Sets in Graphs using Answer Set Programming
Chase, Melissa	(CSF) Malleable Signatures: New Definitions and Delegatable Anonymous Credentials
Chatterjee, Krishnendu	(CAV) CEGAR for Qualitative Analysis of Probabilistic Systems
Chatzikokolakis, Kostas	(CSF) Additive and multiplicative notions of leakage, and their capacities
Chaudhuri, Kaustuv	(CSL-LICS) Equality and Fixpoints in the Calculus of Structures (SD) Opening Remarks (LFMTP) Automatically Deriving Schematic Theorems for Dynamic Contexts (Linearity) Undecidability of Multiplicative Subexponential Logic
Chaudhuri, Swarat	(CAV) Optimal Guard Synthesis for Memory Safety
Chechik, Marsha	(iPRA) Specification Synthesis via Generalized Abduction
Chemeritskiy, Eugene	(FRIDA) Models and techniques for verification of Software Defined Networks
Chen, Geng	(VSTTE) Store Buffer Reduction with MMUs
Chen, Hubie	(QUANTIFY) Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction (PC) Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction (CSL-LICS) One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries (CSL-LICS) The Tractability Frontier of Graph-Like First-Order Query Sets
Chen, Jiang	(PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Chen, Jieying	(DL) Evaluation of Extraction Techniques for Ontology Excerpts
Chen, Liqun	(CSF) Balancing Societal Security and Individual Privacy: Accountable Escrow System
Chen, Pin Hsiuan	(PAS) Automatic App Testing of LTL Properties
Chen, Taolue	(CSL-LICS) On the Total Variation Distance of Labelled Markov Chains
Chen, Tzu-Chun	(ITRS) Semantic Types for Classes and Mixins
Chen, Wei	(CSL-LICS) Abstract Interpretation from Buchi Automata
Chen, Xiaoyu	(PAS) RCK: A Software Toolkit for R-calculus
Chen, Yu-Fang	(CAV) Program Verification through String Rewriting (iPRA) Towards Craig Interpolation for String Constraints
Cheng, Chih-Hong	(CAV) G4LTL-ST: Automatic Generation of PLC Programs
Chesani, Federico	(ICLP) Multi-criteria optimal planning for Energy policies in CLP
Chew, Leroy	(IJCAR) The Complexity of Theorem Proving in Circumscription and Minimal Entailment (NMR) Tableau vs. Sequent Calculi for Minimal Entailment
Chiancone, Andrea	(RCRA) Self Regulating Mechanisms for Network Immunization
Chiang, Wen-Hong	(PAS) Automatic App Testing of LTL Properties
Chiba, Yuki	(WPTE) Verifying the Correctness of Tupling Transformations based on Conditional Rewriting
Chin, Wei-Ngan	(CAV) Shape Analysis via Second-Order Bi-Abduction (LC) Completeness of second-order separation logic for program verification
Chistikov, Dmitry	(AISS) Unary Pushdown Automata and Straight-Line Programs
Chlipala, Adam	(Coq) Automating Abstract Logics (ITP) Experience Implementing a Performant Category-Theory Library in Coq (ITP) Compositional Computational Reflection
Chmelík, Martin	(CAV) CEGAR for Qualitative Analysis of Probabilistic Systems
Chocron, Paula	(IJCAR) A Gentle Non-Disjoint Combination of Satisfiability Procedures (ADDCT) Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
Choi, Arthur	(KR) Probabilistic Sentential Decision Diagrams
Chong, Nathan	(CAV) Engineering a Static Verification Tool for GPU Kernels
Chong, Stephen	(CSF) Declarative Policies for Capability Control
Chowdhury, Md Solimul	(CICLOPS-WLPE) A System for Embedding Global Constraints into SAT
Chowdhury, Omar	(CAV) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies
Christ, Juergen	(SMT) Weakly Equivalent Arrays
Christiansen, David Raymond	(DTP) Tool Demonstration: An IDE for Programming and Proving in Idris
Chu, Geoffrey	(ICLP) Grounding Bound Founded Answer Set Programs
Chubaryan, Anahit	(LC) On proof complexities of strong equal modal tautologies.
Chudnov, Andrey	(CSF) Information flow monitoring as abstract interpretation for relational logic
Chvalovský, Karel	(LATD) Undecidability of consequence relation in Full Non-associative Lambek Calculus
Chyzak, Frédéric	(ITP) A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Ciabattoni, Agata	(LATD) Poof Search and Co-NP completeness for Many-Valued Logics (LATD) Embeddings into BiFL-algebras and conservativity
Ciaffaglione, Alberto	(LFMTP) Internal Adequacy of Bookkeeping in Coq
Cimatti, Alessandro	(CAV) The nuXmv Symbolic Model Checker (CAV) Verifying LTL properties of hybrid systems with K-liveness
Cintula, Petr	(GeTFun) First-order non-classical logics: an order-based approach
Ciobaca, Stefan	(RTA-TLCA) All-Path Reachability Logic (PAS) Programming Language Aggregation with Applications in Equivalence Checking
Citkin, Alex	(LATD) A meta-Logic of multiple-conclusion rules
Clairambault, Pierre	(CSL-LICS) Symmetry in Concurrent Games
Clarke, Edmund	(VSL) VSL Keynote Talk: Verification of Computer Systems with Model Checking (RS) Model Checking Hybrid Systems
Cleaveland, Rance	(CAV) Automated Testing (preliminary title)
Clochard, Martin	(VSTTE) Formalizing Semantics with an Automatic Program Verifier (VSTTE) Automatically verified implementation of data structures based on AVL trees (SHORT)
Cock, David	(ITP) From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle
Codescu, Mihai	(ARQNL) Proof Support for Common Logic
Codish, Michael	(SAT) Simplifying Pseudo-Boolean Constraints in Residual Number Systems (CICLOPS-WLPE) Proofs for Optimality of Sorting Networks by Logic Programming
Codognet, Philippe	(ParSearchOpt) On the Parallelization of Randomized Propagation-based Constraint Solving
Cohen, Cyril	(ITP) A Coq Formalization of Finitely Presented Modules
Cohen, Ernie	(VSTTE) Store Buffer Reduction with MMUs
Cohen, Liron	(LC) Predicative Mathematics via Safety Relations (PSC) Intuitionistic Ancestral Logic
Cohn, Tony	(KR) Knowledge Representation Meets Computer Vision: From Pixels to Symbolic Activity Descriptions
Cok, David	(VSL) FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
Colange, Maximilien	(FWFM) Introducing Formal Verification with Lego
Colcombet, Thomas	(CSL-LICS) Two-Way Cost Automata and Cost Logics over Infinite Trees
Collingbourne, Peter	(CAV) Engineering a Static Verification Tool for GPU Kernels
Collins, Sandra	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Comini, Marco	(ICLP) Abstract Diagnosis for tccp using a Linear Temporal Logic
Comon-Lundh, Hubert	(FCS-FCC) Protocol Indistinguishability and the Computationally Complete Symbolic Attacker (FCS-FCC) A tool for automating the computationally complete symbolic attacker
Condoravdi, Cleo	(NLSR) Natural Language Access to Data
Conradie, Willem	(LC) Algorithmic-algebraic canonicity for mu-calculi (LC) Hybrid extensions of S4 with the finite model property
Console, Marco	(DL) Graphol: Ontology representation through diagrams (DL) Reducing global consistency to local consistency in Ontology-based Data Access - Extended Abstract
Constable, Robert	(PSC) Intuitionistic Ancestral Logic
Cook, Byron	(VSL) FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (CAV) Finding instability in biological models (LC) The place of logic in computer science education (WST) Reducing Deadlock and Livelock Freedom to Termination (WST) Fairness for Infinite-State Systems
Cooper, Robin	(NLCS) How to do things with types
Copello, Ernesto	(LFMTP) Gentle Formalisation of Stoughton’s Lambda Calculus Substitution
Coppo, Mario	(ITRS) On Isomorphism of "Functional'' Intersection and Union Types
Coquand, Thierry	(CLC) A sheaf model of the algebraic closure
Cortier, Véronique	(VSL) FLoC Plenary Talk: Electronic voting: how logic can help? (FCS-FCC) A tool for automating the computationally complete symbolic attacker
Costantini, Stefania	(RCRA) Concept Learning by a Monte-Carlo Tree Search of Argumentations
Costantini, Stefania	(ASPOCP) Query Answering in Resource-Based Answer Set Semantics
Coste-Marquis, Sylvie	(KR) On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses
Cousin, Michael	(HSB) FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference
Cousot, Patrick	(CSL-LICS) Abstract Interpretation: Past, Present and Future
Cousot, Radhia	(CSL-LICS) Abstract Interpretation: Past, Present and Future
Coventry, Lynne	(STAST) Decision justifications for wireless network selection (STAST) Tackling the Awareness-Behaviour Divide in Security: (step 1) Understand the User
Cowles, John	(ACL2) On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics (ACL2) Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis (ACL2) Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
Cox, Arlen	(CAV) QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
Craig, Andrew	(LC) Algorithmic-algebraic canonicity for mu-calculi (LATD) Many-valued modal logic over residuated lattices via duality
Cramer, Marcos	(NLCS) Modelling implicit dynamic introduction of function symbols in mathematical texts (QED) The Naproche system: Proof-checking mathematical texts in controlled natural language
Crampton, Jason	(CSF) Attribute-based Encryption for Access Control Using Elementary Operations
Creese, Sadie	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Creignou, Nadia	(NMR) Belief merging within fragments of propositional logic
Cremers, Cas	(CSF) Actor Key Compromise: Consequences and Countermeasures
Cretin, Julien	(CSL-LICS) System F with Coercion Constraints
Creus, Carles	(SAT) Automatic Evaluation of Reductions between NP-complete Problems (RTA-TLCA) Automatic Evaluation of Context-Free Grammars (System Description) (RTA-TLCA) Tree Automata with Height Constraints between Brothers
Crouch, Richard	(NLCS) Transfer Semantics for the Clear Parser
Cruanes, Simon	(PAAR) Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Cruz, Flavio	(ICLP) A Linear Logic Programming Language for Concurrent Programming over Graph Structures (CICLOPS-WLPE) A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs
Cruz-Filipe, Luís	(CICLOPS-WLPE) Proofs for Optimality of Sorting Networks by Logic Programming
Crăciun, Adrian	(SAT) Proof complexity and the Lovasz-Kneser Theorem
Cuenca Grau, Bernardo	(IJCAR) EL-ifying Ontologies (DL) Pay-as-you-go Ontology Query Answering Using a Datalog Reasoner (DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs (DL) On Faceted Search over Knowledge Bases (DL) Controlled Query Evaluation over Lightweight Ontologies (DL) Datalog Rewriting Techniques for Non-Horn Ontologies
Culnane, Chris	(CSF) A Peered Bulletin Board for Robust Use in Verifiable Voting Systems
Curzon, Paul	(VeriSure) Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project
Cussens, James	(PLP) First-order representations for integer programming
Cuteri, Bernardo	(RCRA) Declarative Specification of Benchmark Sessions via ASP
Cvrcek, Dan	(ASA) Application Oriented Low Cost Security Modules
Czajka, Łukasz	(RTA-TLCA) A Coinductive Confluence Proof for Infinitary Lambda-Calculus.
D
D'Agostino, Giovanna	(LC) On Uniform Interpolation for the Guarded Fragment
D'Amato, Claudia	(ORE) Exploring Reasoning with the DMOP Ontology
D'Antoni, Loris	(CAV) Symbolic Visibly Pushdown Automata
D'Souza, Deepak	(VSTTE) Efficient Refinement Checking in VCC
D'Urso, Enrico	(VeriSure) Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project
Da Silveira, Marcos	(KR4HC) Towards a Conceptual Model for Enhancing Reasoning about Clinical Guidelines: A case-study on Comorbidity
Daca, Przemyslaw	(CAV) CEGAR for Qualitative Analysis of Probabilistic Systems
Dal Lago, Ugo	(2FC) Subrecursive Linear Dependent Types and Computational Security (FCS-FCC) Towards a Coinductive Characterization of Computational Indistinguishability (CSL-LICS) The Geometry of Synchronization (CSL-LICS) Beta Reduction is Invariant, Indeed (Linearity) Wave-Style Token Machines and Quantum Lambda Calculi
Dal Palù, Alessandro	(ParSearchOpt) Towards a complete constraint solver on GPU
Dalchau, Neil	(VEMDP) Software tools for analysing the chemical master equation
Damouche, Nasrine	(NSV) Transformation of a PID Controller for Numerical Accuracy
Dang, Thao	(HSB) Exploiting the eigenstructures of linear systems to speed up reachability computation (HSB) Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models
Dannenberg, Frits	(VEMDP) Guiding the development of DNA walker systems to guarantee reliability and performance
Danos, Vincent	(VEMDP) Formal mean field theories for graph rewriting
Dapoigny, Richard	(DTP) A Unifying Framework for Primitive Ontological Relations in Dependent Type Theory
Darwiche, Adnan	(KR) Skolemization for Weighted First-Order Model Counting (KR) Probabilistic Sentential Decision Diagrams (PLP) Lifted Inference for Probabilistic Logic Programs
Das, Anupam	(PC) n^O(log log n) size monotone proofs of the weak pigeonhole principle (CSL-LICS) On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems
Datta, Anupam	(CAV) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (FCS-FCC) Actual Causes of Security Violations
David, Amélie	(IJCAR) Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
Davis, Jared	(ITP) Invited talk: Microcode Verification - Another Piece of the Microprocessor Verification Puzzle (ACL2) Industrial-Strength Documentation for ACL2
Davis, Jared	(ITP) The reflective Milawa theorem prover is sound (down to the machine code that runs it)
Davis, Jennifer	(ACL2) Development of a Translator from LLVM to ACL2
Dawar, Anuj	(CSL-LICS) The Ackermann Award 2014 (LCC) On the power of fixed-point logic with counting
De Angelis, Emanuele	(VPT) Program Verification using Constraint Handling Rules and Array Constraint Generalizations
De Bra, Paul	(KR4HC) A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols
de Carvalho, Daniel	(RTA-TLCA) An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting
De Cat, Broes	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories (LaSh) Lazy Model Expansion: Interleaving Grounding with Search (LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development
De Clercq, Sofie	(KR) Using Answer Set Programming for Solving Boolean Games
De Cock, Martine	(KR) Using Answer Set Programming for Solving Boolean Games
De Groef, Willem	(CSF) Stateful Declassification Policies for Event-Driven Programs
De Haan, Ronald	(KR) The Parameterized Complexity of Reasoning Problems Beyond NP (SAT) Fixed-parameter tractable reductions to SAT
de Jong, Hidde	(HSB) Collaboration success stories: Control of Gene Expression in E.coli (with Hans Geiselman)
De Liguoro, Ugo	(ITRS) Semantic Types for Classes and Mixins
de Maria, Elisabetta	(LSB) A Logical Framework for Systems Biology
de Mel, Geeth	(DL) Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information
De Moura, Leonardo	(APPA) Proofs in Satisfiability Modulo Theories (QUANTIFY) Finding Conflicting Instances of Quantified Formulas in SMT (SAT) A Model-Constructing Satisfiability Calculus
De Nivelle, Hans	(ARQNL) Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic
de Paiva, Valeria	(LC) An intuitive semantics for {Full Intuitionistic Linear Logic}
De Raedt, Luc	(PLP) Compiling Probabilistic Logic Programs into Sentential Decision Diagrams (PLP) PageRank, ProPPR and Stochastic Logic Programs
de Vrijer, Roel	(RTA-TLCA) Proof terms for infinitary rewriting
Debruyne, Christophe	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Decker, Stefan	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Degorre, Aldric	(CSL-LICS) Asymptotic behaviour in temporal logic
Deharbe, David	(VSL) FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (SMT) Extending SMT-LIB v2 with lambda-terms and polymorphism
Dei Rossi, Gian-Luca	(CSF) Mignis: A semantic based tool for firewall configuration
Del Vescovo, Chiara	(DL) DeaLing with Ontologies using CODs
Delgrande, James P.	(KR) Belief Change and Base Dependence (KR) Toward a Knowledge Level Analysis of Forgetting (ASPOCP) ``Are Preferences Giving You a Headache?'' - ``Take asprin!'' (NMR) An Approach to Forgetting in Disjunctive Logic Programs that Preserves Strong Equivalence
Deligiannis, Pantazis	(CAV) Engineering a Static Verification Tool for GPU Kernels
Dellunde, Pilar	(LATD) Advances on elementary equivalence in model theory of fuzzy logics
Delzanno, Giorgio	(FRIDA) Model Checking Distributed Consensus Algorithms
Demirović, Emir	(LaSh) Modeling High School Timetabling as PartialWeighted maxSAT
Demri, Stephane	(CSL-LICS) Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction
Denecker, Marc	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories (ICLP) C-Log: A Knowledge Representation Language of Causality (KR) The Well-Founded Semantics Is the Principle of Inductive Definition, revisited (LaSh) Lazy Model Expansion: Interleaving Grounding with Search (LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development (NMR) Inference in the FO(C) Modelling Language (NMR) FO(C) and Related Modelling Paradigms
Depauli-Schimanovich, Werner	(VSL) Lifetime Achievement Award
Dershowitz, Nachum	(RS) Towards a General Model of Evolving Interaction (WST) Another Proof for the Recursive Path Ordering (IFIP-WG16) Discussion on the Open Problems List in Rewriting (DCM) Cellular Automata are Generic
Dershowitz, Nachum	(RTA-TLCA) Confluence by Critical Pair Analysis
Desai, Ankush	(EC2) A new reduction for event-driven distributed programs
Despeyroux, Joelle	(LSB) A Logical Framework for Systems Biology
Deters, Morgan	(CAV) A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions (CSL-LICS) Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction
Detlefsen, Michael	(CSL-LICS) Inductive Proofs & the Knowledge They Represent
Deutsch, Alin	(KR) State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems
Devriendt, Jo	(CSPSAT) BreakIDGlucose: on the importance of row symmetry
Devriese, Dominique	(CSF) Stateful Declassification Policies for Event-Driven Programs
Dezani-Ciancaglini, Mariangiola	(ITRS) On Isomorphism of "Functional'' Intersection and Union Types (RTA-TLCA) Preciseness of subtyping on intersection and union types
Di Noia, Tommaso	(PRUV) Computing k-Rank Answers with Ontological CP-Nets
Di Nola, Antonio	(LATD) On the Logic of Perfect MV-algebras
Di Pierro, Alessandra	(DCM) Probabilistic Types and Function Overloading
Di Sciascio, Eugenio	(ORE) Mini-ME 2.0: powering the Semantic Web of Things
Diaconescu, Denisa	(LATD) A method for generalizing finite automata arising from Stone-like dualities
Diakidoy, Irene-Anna	(KR) A Psychology-Inspired Approach to Automated Narrative Text Comprehension (NMR) Non-Monotonic Reasoning and Story Comprehension
Diaz, Daniel	(ParSearchOpt) Towards a Parallel Hierarchical Adaptive Solver Tool (CICLOPS-WLPE) Extending the Finite Domain Solver of GNU Prolog
Dietz, Emmanuelle-Anna	(ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect
Dillig, Isil	(CAV) Optimal Guard Synthesis for Memory Safety (iPRA) Specification Synthesis via Generalized Abduction
Dillig, Thomas	(CAV) Optimal Guard Synthesis for Memory Safety
Dillinger, Peter	(ACL2) Data Definitions in ACL2 Sedan
Dima, Catalin	(CAV) Safraless Synthesis for Epistemic Temporal Specifications (CSL-LICS) Asymptotic behaviour in temporal logic
Dimopoulos, Yannis	(KR) Heuristic Guided Optimization for Propositional Planning
Dimoulas, Christos	(CSF) Declarative Policies for Capability Control
Dinis, Bruno	(LC) An axiomatic approach to modelling of orders of magnitude
Distel, Felix	(KR) Decidable Gödel Description Logics without the Finitely-Valued Model Property (KR) Concept Dissimilarity with Triangle Inequality (DL) Gödel Description Logics with General Models
Dittmann, Christoph	(CSL-LICS) Decomposition Theorems and Model-Checking for the Modal mu-calculus
Divakaran, Sumesh	(VSTTE) Efficient Refinement Checking in VCC
Dixon, Clare	(IJCAR) Clausal Resolution for Modal Logics of Confluence
Diéguez, Martín	(KR) Strong Equivalence of Non-monotonic Temporal Theories (ASPOCP) Temporal Stable Models are LTL-representable
Djeddai, Ala	(DL) Reasoning about Belief Uncertainty in DL-Lite N bool (PRUV) A New DL‐Lite N Bool Probabilistic Extension Using Belief
Dobrinen, Natasha	(LC) Budding Trees
Dobrinen, Natasha	(LC) Generalized Ellentuck spaces and initial Tukey chains of non-p-points
Dobrowolski, Jan	(LC) Topologies on Polish structures
Dockins, Robert	(ITP) Formalized, effective domain theory in Coq
Doczkal, Christian	(ITP) Completeness and Decidability Results for CTL in Coq
Dodaro, Carmine	(ICLP) Anytime Computation of Cautious Consequences in Answer Set Programming (ASPOCP) On the Implementation of Weak Constraints in WASP (NMR) Preliminary Report on WASP 2
Dodds, Mike	(FRIDA) A Fast, Correct Time-Stamped Stack
Doko, Marko	(REORDER) Reasoning about Fences in C11 Weak Memory Model
Doligez, Damein	(ARQNL) Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Dolzmann, Andreas	(SMT) Better Answers to Real Questions
Donaldson, Alastair	(CAV) Engineering a Static Verification Tool for GPU Kernels (WST) Automatic Termination Analysis for GPU Kernels
Donat-Bouillud, Pierre	(IFIP-WG16) Rhythm Tree Rewriting
Donze, Alexandre	(HSB) Tutorial: Simulation-based Parameter Synthesis in Systems Biology
Dorigatti, Michele	(CAV) The nuXmv Symbolic Model Checker
Dorzhieva, Marina	(LC) Computable numberings in Analytical Hierarchy
Dougherty, Daniel	(FCS-FCC) A Hybrid Analysis for Security Protocols with State (CSF) Decidability for Lightweight Diffie-Hellman Protocols (PAAR) Razor: Provenance and Exploration in Model-Finding
Doumane, Amina	(SD) A Correctness Criterion Free from Switchings
Doutre, Sylvie	(KR) A Dynamic Logic Framework for Abstract Argumentation
Dovier, Agostino	(ParSearchOpt) Towards a complete constraint solver on GPU
Dowek, Gilles	(APPA) Deduction Modulo (SD) Simply Typed Lambda-Calculus Modulo Type Isomorphisms (IFIP-WG16) Rewriting, Proofs and Transition Systems
Dragan, Ioan	(Vampire) SAT solving experiments in Vampire
Dragoi, Cezara	(FRIDA) Round model for distributed algorithms: from verification to implementation. (FRIDA) A Logic-based Framework for Verifying Consensus Algorithms
Draief, Moez	(RCRA) Concept Learning by a Monte-Carlo Tree Search of Argumentations
Dramnesc, Isabela	(PAS) Synthesis of Algorithms on Sets Represented as Monotone Lists
Dreossi, Tommaso	(NSV) Epsilon-semantics and hybrid automata
Dreossi, Tommaso	(HSB) Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models
Dresler, Georg	(CAV) Software Verification in the Google App-Engine Cloud
Dubasi, Mohana Asha Latha	(VSTTE) Timed Refinements for Verification of Real-Time Object Code Programs
Dubslaff, Clemens	(CSL-LICS) Trade-Off Analysis Meets Probabilistic Model Checking
Duck, Gregory J.	(ICLP) On Termination, Confluence and Consistent CHR-based Type Inference
Duckham, Matt	(KR) On Redundant Topological Constraints (Extended Abstract)
Dudenhefner, Andrej	(ITRS) Delegation-based Mixin Composition Synthesis
Dufour-Lussier, Valmi	(KR) Belief Revision in the Propositional Closure of a Qualitative Algebra
Dufourd, Jean-François	(ITP) Hypermap Specification and Certified Linked Implementation using Orbits
Dundua, Besik	(PAS) Confluence of Pattern-Based Calculi with Finitary Matching
Dunne, Paul E.	(KR) Characteristics of Multiple Viewpoints in Abstract Argumentation
Durand, Arnaud	(SAT) Hypergraph Acyclicity and Propositional Model Counting
Dusberger, Frederico	(LaSh) The D-FLAT System for Dynamic Programming on Tree Decompositions (ASPOCP) Computing Secure Sets in Graphs using Answer Set Programming
Dutertre, Bruno	(CAV) Yices 2.2
Dvořák, Wolfgang	(KR) Characteristics of Multiple Viewpoints in Abstract Argumentation (NMR) Compact Argumentation Frameworks
Dyrkolbotn, Sjur Kristoffer	(KR) How to Argue for Anything: Enforcing Arbitrary Sets of Labellings Using AFs
Dzik, Wojciech	(LC) Almost structurally complete consequence operations extending S4.3 (LATD) Admissible rules and almost structural completeness in some first-order modal logics
Dénès, Maxime	(Coq) QuickChick: Property-Based Testing for Coq
Düdder, Boris	(ITRS) Delegation-based Mixin Composition Synthesis
E
Eades Iii, Harley	(CLC) Dualized Type Theory
Eastaugh, Benedict	(LC) Computational reverse mathematics and foundational analysis
Echenim, Mnacho	(IJCAR) A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PAAR) A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
Ecke, Andreas	(KR) Answering Instance Queries Relaxed by Concept Similarity (DL) Mary, What's Like All Cats? (PRUV) Similarity-based Relaxed Instance Queries in EL++
Eckert, Daniel	(LATD) Boolean-valued judgment aggregation
Edalat, Abbas	(CSL-LICS) A domain-theoretic approach to Brownian motion and general continuous stochastic processes
Een, Niklas	(iPRA) Interpolants in Two-Player Games
Egly, Uwe	(QUANTIFY) Quantifier handling in calculi for quantified Boolean formulas (QBF) On the Relation between Resolution Calculi for QBFs and First-order Formulas (QBF) Conformant Planning as a Case Study of Incremental QBF Solving
Eguchi, Naohi	(TermGraph) Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
Ehlers, Ruediger	(CAV) SYNTCOMP - Synthesis Competition for Reactive Systems (IJCAR) A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (SYNT) Low-effort Specification Debugging and Analysis (SYNT) How to Handle Assumptions in Synthesis
Ehrhard, Thomas	(CSL-LICS) A new correctness criterion for MLL proof nets
Eisentraeger, Kirsten	(LC) Generalizations of Hilbert's Tenth Problem
Eiter, Thomas	(DL) Contextualized Knowledge Repositories with Justifiable Exceptions (DL) Towards Practical Deletion Repair of Inconsistent DL-programs (ORE) Using OpenStreetMap Data to Create Benchmarks for Description Logic Reasoners
Eiter, Thomas	(VSL) Welcome Address by the Organizers
Eldib, Hassan	(CAV) Synthesis of Masking Countermeasures against Side Channel Attacks
Eleftheriou, Pantelis	(LC) Pregeometries and definable groups
Eloussi, Lamyaa	(CAV) Regression Test Selection for Distributed Software Histories
Emmes, Fabian	(IJCAR) Proving Termination of Programs Automatically with AProVE (CICLOPS-WLPE) Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
Emmi, Michael	(CAV) SMACK: Decoupling Source Language Details from Verifier Implementations
Emoto, Kento	(ITP) A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
Endrullis, Joerg	(CSL-LICS) On Periodically Iterated Morphisms (WST) Non-termination using Regular Languages (WIR) An Introduction to the Clocked Lambda Calculus
Englander, Cecilia	(GeTFun) Natural deduction for non-deterministic finite-valued logics
Engström, Fredrik	(DL) Understandable Explanations in Description Logic
Erbatur, Serdar	(UNIF) Hierarchical Combination of Matching Algorithms (Extended Abstract) (UNIF) On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
Erdem, Esra	(RCRA) A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks
Escardo, Martin	(PSC) Excluded Middle Considered as a Mathematical Problem (Invited Talk) (RTA-TLCA) Abstract datatypes for real numbers in type theory
Esik, Zoltan	(ICLP) Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation
Esparza, Javier	(CAV) From LTL to Deterministic Automata: A Safraless Compositional Approach (CAV) An SMT-Based Approach to Coverability Analysis
Espindola, Christian	(LC) Semantic completeness of first order theories in constructive reverse mathematics (PSC) Constructive completeness and exploding models
Espírito Santo, José	(CLC) Confluence for classical logic through the distinction between values and computations
Esteban, Guillermo	(ORE) Android Went Semantic: Time for Evaluation
Esteva, Francesc	(LATD) Axiomatising a fuzzy modal logic over the standard product algebra
Etessami, Kousha	(LCC) ImmermanFest Opening Remarks
European Masters Program In Computational Logic,	(VSL) EMCL Distinguished Alumni Award (ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect
Everaere, Patricia	(KR) On Egalitarian Belief Merging
Everyone,	(CHR) Discussion (ICLP) On Termination, Confluence and Consistent CHR-based Type Inference
Ewin, Christopher	(KR) Transforming Situation Calculus Action Theories for Optimised Reasoning
F
Faber, Wolfgang	(ICLP) Efficient Computation of the Well-Founded Semantics over Big Data (ASPOCP) Computing Answer Sets for Monadic Logic Programs via MapReduce (RCRA) Efficient Computation of the Well-Founded Semantics over Big Data (NMR) Semantics and Compilation of Answer Set Programming with Generalized Atoms
Facchini, Alessandro	(CSL-LICS) Weak MSO: Automata and Expressiveness Modulo Bisimilarity
Facchini, Stefano	(DCM) Quantum Circuits for the Unitary Permutation Problem
Faggian, Claudia	(CSL-LICS) The Geometry of Synchronization
Fahl, Sascha	(CSF) Who’s Afraid of Which Bad Wolf? A Survey of IT Security Risk Awareness
Faithfull, Alexander	(Coq) Coqoon: towards a modern IDE for Coq
Faizrahmanov, Marat	(LC) Limitwise monotonic sets of reals
Falcão, Pedro	(GeTFun) Modal functions as moody truth-functions
Falkovich, Evgenia	(DCM) Cellular Automata are Generic
Fallenstein, Benja	(VERIFY) Verifying safety properties of Artificial General Intelligence: The ultimate safety-critical system?
Fan, Chuchu	(CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells
Fan, Tuan-Fang	(LC) Fuzzy Bsimulation for Standard Godel Modal Logic
Fanchon, Eric	(HSB) Exploiting the eigenstructures of linear systems to speed up reachability computation (HSB) Collaboration success stories: Modeling Iron Homeostasis in Mammalian Cells (with J.M. Moulis)
Fandiño, Jorge	(ICLP) Causal Graph Justifications of Logic Programs
Farahani, Hadi	(LC) Predicate Glivenko theorems and substructural aspects of negative translations
Farzan, Azadeh	(EC2) Concolic Testing of Concurrent Programs
Faustino Da Silva, Anderson	(ICLP) Towards an Efficient Prolog System by Code Introspection
Feier, Cristina	(IJCAR) EL-ifying Ontologies (DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs
Fekete, Yoav	(SAT) Simplifying Pseudo-Boolean Constraints in Residual Number Systems
Felgenhauer, Bertram	(WST) Type Introduction for Runtime Complexity Analysis
Fellermann, Harold	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Fellner, Andreas	(IJCAR) Skeptik [System Description]
Felsing, Dennis	(ARW-DT) Automating Regression Verification
Felty, Amy	(LSB) A Logical Framework for Systems Biology
Feng, Xinyu	(CSL-LICS) Compositional Verification of Termination-Preserving Refinement of Concurrent Programs
Feng, Zhiyong	(ICLP) A Well-Founded Semantics for FOL-Programs
Feret, Jerome	(LSB) An algebraic approach for inferring and using symmetries in rule-based models
Fernandez, Maribel	(WWV) Static Enforcement of Role-Based Access Control
Fernandez Gil, Oliver	(DL) On the Non-Monotonic Description Logic ALC+Tmin
Fernández, Pau	(SAT) Automatic Evaluation of Reductions between NP-complete Problems
Fernández-Duque, David	(LC) Provability logics and proof-theoretic ordinals
Ferrara, Anna Lisa	(CAV) VAC - Verifier of Administrative Role-based Access Control Policies
Ferrari, Mauro	(PSC) Proof-search in natural deduction calculi for IPL
Field, Hartry	(LC) Prospects for a Naive Theory of Classes
Figueira, Diego	(CSL-LICS) Pattern Logics and Auxiliary Relations
Filiot, Emmanuel	(CAV) Safraless Synthesis for Epistemic Temporal Specifications
Filliatre, Jean-Christophe	(CAV) The Spirit of Ghost Code (VSTTE) Formalizing Semantics with an Automatic Program Verifier
Filmus, Yuval	(PC) From Small Space to Small Width in Resolution (PC) Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
Fink, Michael	(ICLP) Causal Graph Justifications of Logic Programs (DL) Towards Practical Deletion Repair of Inconsistent DL-programs
Finkbeiner, Bernd	(CAV) Causal Termination of Multi-threaded Programs (SAT) Fast DQBF Refutation (SYNT) Petri Games: Synthesis of Distributed Systems with Causal Memory (Invited Talk)
Finkel, Olivier	(LC) Infinite Games Specified by 2-Tape Automata
Finkelstein, Anthony	(VEMDP) An Aspect Oriented Design and Modelling Framework for Synthetic Biology
Finster, Eric	(CSL-LICS) Eilenberg-MacLane Spaces in Homotopy Type Theory
Fionda, Valeria	(KR) Knowledge Maps of Web Graphs
Fioravanti, Fabio	(VPT) Program Verification using Constraint Handling Rules and Array Constraint Generalizations
Fiore, Marcelo	(CSL-LICS) Substitution, jumps, and algebraic effects
Fiorentini, Camillo	(PSC) Proof-search in natural deduction calculi for IPL
Fioretto, Ferdinando	(ParSearchOpt) Towards a complete constraint solver on GPU
Fischer, Bernd	(CAV) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
Fischer, Vera	(LC) Cardinal invariants and template iterations
Fischl, Wolfgang	(DL) Expressive Identification Constraints to Capture Functional Dependencies in Description Logics
Fischmeister, Sebastian	(SAT) Impact of Community Structure on SAT Solver Performance
Fisher, Jasmin	(CAV) Finding instability in biological models (CSL-LICS) Understanding Biology through Logic (RS) Cancer as Reactivity (WST) Termination of Biological Programs
Fitting, Melvin	(LATD) The Range of Realization Which modal logics have explicit counter parts
Fitting, Melvin	(NCPROOFS) Applications of Nested-Sequent Proof Systems for Modal Logics to the Craig Interpolation Property
Flaminio, Tommaso	(LATD) A method for generalizing finite automata arising from Stone-like dualities
Floc Olympic Games,	(VSL) FLoC Olympic Games Award Ceremony 1 (VSL) FLoC Olympic Games Award Ceremony 2
Florido, Mário	(ITRS) Liquid Intersection Types (PAS) Confluence of Pattern-Based Calculi with Finitary Matching
Focardi, Riccardo	(CSF) Mignis: A semantic based tool for firewall configuration
Focardi, Riccardo	(CSF) Provably Sound Browser-Based Enforcement of Web Session Integrity
Fokina, Ekaterina	(LC) Degree spectra of structures under $\Sigma_n$-equivalence.
Font, Josep Maria	(LATD) Generalizing the Leibniz and Suszko operators (LATD) On logics of varieties and logics of semilattices
Fontaine, Pascal	(APPA) Proofs in Satisfiability Modulo Theories (IJCAR) A Gentle Non-Disjoint Combination of Satisfiability Procedures (ADDCT) Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
Foreman, Matt	(LC) The Singular Cardinals Problem after 130 years or so
Formisano, Andrea	(ASPOCP) Query Answering in Resource-Based Answer Set Semantics
Forssell, Henrik	(LC) Constructive completeness and Joyal's theorem (PSC) Constructive completeness and exploding models
Fouilhe, Alexis	(VSTTE) A certifying frontend for (sub)polyhedral abstract domains
Fouquere, Christophe	(NLCS) Divergence in Dialogues (SD) Multiplicative Decomposition of Behaviours in Ludics
Fox, Anthony	(HOL) HOL4 Hidden Features
Fox, Maria	(QUANTIFY) Encoding Reachability with Quantification
Francez, Nissim	(NLCS) Proof-Theoretic Semantics for intensional transitive verbs
Franconi, Enrico	(iPRA) Interpolation and Domain Independence applied to Databases
Frank, Michael	(CICLOPS-WLPE) Proofs for Optimality of Sorting Networks by Logic Programming
Franklin, Johanna	(LC) UD-randomness and the Turing degrees
Fraser, Gordon	(WING) Loop Invariants by Mutation, Dynamic Validation, and Static Checking
Fredrikson, Matt	(CSL-LICS) Satisfiability Modulo Counting: A New Approach for Analyzing Privacy Properties
Freilich, Adam	(CSL-LICS) Regular Combinators for String Transformations
Freitas, Fred	(DL) A Method to Develop Description Logic Ontologies Iteratively with Automatic Requirement Traceability
Freitas, Leo	(VSTTE) A Model for Capturing and Replaying Proof Strategies
Fremont, Daniel J.	(SMT) Speeding Up SMT-Based Quantitative Program Analysis
French, George	(ASA) Banking security Wish list: notes from the edge
Frenkel, Sergey	(VeriSure) Assurance of some system reliability characteristics in formal design verification
Freuder, Eugene	(RCRA) Dispensable Instantiations in Constraint Satisfaction Problems
Friedman, Sy-David	(INFINITY) Set functions with small circuits (INFINITY) Cobham Recursive Set Functions
Frittella, Sabine	(LC) Display-type calculi for non classical logics
Frittella, Sabine	(GSB) Display-type calculi and their cut elimination metatheorem
Froeschle, Sibylle	(FCS-FCC) On Well-Founded Security Protocols
Frohn, Florian	(IJCAR) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (IJCAR) Proving Termination of Programs Automatically with AProVE
Frolov, Andrey	(LC) $\Delta_2^0$-spectra of linear orderings (LC) On categoricity of scattered linear orders
Frtús, Jozef	(NMR) Credulous and Skeptical Argument Games for Complete Semantics in Conflict Resolution based Argumentation
Fruehwirth, Thom	(CHR) From XML Schema to JSON Schema: Translation with CHR (ICLP) The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information (ICLP) Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R
Frumin, Daniil	(VPT) Branching Processes of Conservative Nested Petri Nets
Fränzle, Martin	(iPRA) Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems
Fröhlich, Andreas	(QUANTIFY) EPR Encodings of Bit-Vector Problems Even With Quantifiers (SAT) Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses (SAT) Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask) (LCC) On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic (POS) iDQ: Instantiation-Based DQBF Solving
Fu, Hao Cheng	(LC) A Defense of Information Economy Principle
Fu, Peng	(RTA-TLCA) Self Types for Dependently Typed Lambda Encodings
Fuhs, Carsten	(IJCAR) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (IJCAR) Proving Termination of Programs Automatically with AProVE (CSL-LICS) A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates (WST) Discussion (WST) Discussion (WST) Discussion (WST) Discussion and Business Meeting (CICLOPS-WLPE) Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs (RTA-TLCA) First-Order Formative Rules
Furbach, Ulrich	(ARW-DT) Automated Reasoning in Deontic Logic
Furia, Carlo A.	(WING) Loop Invariants by Mutation, Dynamic Validation, and Static Checking
Futatsugi, Kokichi	(WST) Specifying and verifying liveness properties of QLOCK in CafeOBJ
Függer, Matthias	(FRIDA) Towards binary circuit models that faithfully reflect physical (un)solvability
G
Gabbay, Dov	(NMR) Abduction in Argumentation: Dialogical Proof Procedures and Instantiation
Gabbrielli, Maurizio	(ICLP) SUNNY: a Lazy Portfolio Approach for Constraint Solving
Gableske, Oliver	(SAT) An Ising Model inspired Extension of the Product-based MP Framework for SAT
Gaboardi, Marco	(CSF) Differential Privacy: An Economic Method for Choosing Epsilon (CSF) Proving differential privacy in Hoare logic (DCM) Differential privacy at work: Verification of approximate probabilistic programs and models for choosing epsilon
Galatos, Nick	(GeTFun) From display logic to nested sequents via residuated frames (LATD) Densification via polynomial extensions (LATD) Embeddings into BiFL-algebras and conservativity (LATD) Canonical formulas for k-potent residuated lattices
Galeotti, Juan Pablo	(WING) Loop Invariants by Mutation, Dynamic Validation, and Static Checking
Galesi, Nicola	(PC) Total Space in Resolution
Gall, Daniel	(ICLP) Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R
Gallagher, John P.	(ICLP) Analysis and Transformation Tools for Constrained Horn Clause Verification
Gallego Arias, Emilio Jesus	(CSF) Proving differential privacy in Hoare logic
Gambino, Nicola	(RTA-TLCA) A unified approach to Univalent Foundations and Homotopical Algebra
Gamboa, Ruben	(ACL2) On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics (ACL2) Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis (ACL2) Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
Gan, Edward	(Linearity) Type Classes for Lightweight Substructural Types
Ganesh, Vijay	(SAT) Impact of Community Structure on SAT Solver Performance
Ganian, Robert	(CSL-LICS) Model Checking Existential Logic on Partially Ordered Sets (PCCR) Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction
Gao, Sicun	(NSV) Verifying Floating-Point Implementations of Nonlinear Functions
García-Cerdaña, Àngel	(LATD) Advances on elementary equivalence in model theory of fuzzy logics
Garg, Deepak	(CAV) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies (FCS-FCC) Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis
Garg, Pranav	(EC2) A new reduction for event-driven distributed programs (CAV) ICE: A Robust Learning Framework for Synthesizing Invariants
Garlik, Michal	(LC) Model theory of bounded arithmetic and complexity theory
Garreau, Fabien	(NMR) Revisiting Chase Termination for Existential Rules and their Extension to Nonmonotonic Negation
Garrigue, Jacques	(Coq) Formalization of Error-correcting Codes using SSReflect
Gascón, Adrià	(QBF) Synthesis of distributed systems using QBF (SYNT) Synthesis of a simple self stabilizing system
Gaspers, Serge	(PCCR) Backdoors into Heterogeneous Classes of SAT and CSP
Gastin, Paul	(CSL-LICS) Logical Characterization of Weighted Pebble Walking Automata
Gatens, William	(DL) Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies
Gauthier, Thibault	(PAAR) Beagle as a HOL4 external ATP method
Gavanelli, Marco	(ICLP) Multi-criteria optimal planning for Energy policies in CLP
Gawron-Deutsch, Tobias	(FRIDA) Verification and Validation Challenges in Smart Grids from the Industrial Perspective
Gebser, Martin	(VSL) FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (ICLP) Answer Set Programming I (ICLP) The Design of the Fifth Answer Set Programming Competition (ICLP) Answer Set Programming II (ICLP) Clingo = ASP + Control (KR) ASP Encodings of Acyclicity Properties (ASPOCP) Declarative Encodings of Acyclicity Properties (ICLP) Test of Time Award: 10 Years (Talk presented at ICLP Main Conference)
Gelfond, Michael	(ICLP) Vicious Circle Principle and Logic Programs with Aggregates (ASPOCP) A Refinement of the Language of Epistemic Specifications (NMR) Integrating Declarative Programming and Probabilistic Graphical Models for Knowledge Representation and Reasoning in Robotics
Genot, Emmanuel	(LG) Game Semantics from a Cognitive Modeling Standpoint
Geraedts, Wouter	(CLC) A type system for Continuation Calculus
Gerlich, Ralf	(CHR) Automated Test Case Generation and Model Checking with CHR
Geron, Bram	(CLC) A type system for Continuation Calculus
Gervet, Carmen	(ICLP) The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information
Geser, Alfons	(IFIP-WG16) Discussion on the International School on Rewriting (ISR)
Geser, Alfons	(WST) Kurth's Criterion H Revisited (WST) A Solution to Endrullis-08 and Similar Problems
Geuvers, Herman	(CLC) A type system for Continuation Calculus (PSC) A typed lambda-calculus with call-by-name and call-by-value iteration
Gheorghe, Marian	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Gherghina, Cristian	(CAV) Shape Analysis via Second-Order Bi-Abduction
Ghilardi, Silvio	(FRIDA) Monotonic Abstraction Techniques: from Parametric to Software Model Checking (SMT) Decision Procedures for Flat Array Properties (LATD) Step frames analysis in single- and multi-conclusion calculi
Ghilezan, Silvia	(RTA-TLCA) Preciseness of subtyping on intersection and union types
Ghosh, Sujata	(LG) Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground
Giacomin, Massimiliano	(KR) An SCC Recursive Meta-Algorithm for Computing Preferred Labellings in Abstract Argumentation
Gibbons, Jeremy	(DTP) Relational ornaments
Giese, Martin	(DL) OptiqueVQS: Visual Query Formulation for OBDA
Giesl, Jürgen	(VSL) FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014) (IJCAR) Proving Termination and Memory Safety for Programs with Pointer Arithmetic (IJCAR) Proving Termination of Programs Automatically with AProVE (IFIP-WG16) Business Meeting (CICLOPS-WLPE) Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
Gilbert, David	(GSB) Sequent Systems for Classical Modal Logics
Gill, Andrew	(WPTE) HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell
Gilmore, Stephen	(HSB) FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference
Gimenez, Stéphane	(2FC) On the parallel reduction and complexity of interaction-net systems
Giordano, Laura	(DL) Rational closure in SHIQ (KR4HC) Conformance Analysis of the Execution of Clinical Guidelines with Basic Medical Knowledge and Clinical Terminology
Girju, Roxana	(KR) Tracking Beliefs and Intentions in the Werewolf Game
Girlea, Codruta	(KR) Tracking Beliefs and Intentions in the Werewolf Game
Giráldez-Cru, Jesus	(IJCAR) The Fractal Dimension of SAT Formulas
Gispert, Joan	(LATD) Quasivarieties of MV-algebras and structurally complete Lukasiewicz logics
Giunchiglia, Enrico	(QUANTIFY) Encoding Reachability with Quantification (CSPSAT) Tutorial (tentative): TBA
Gladisch, Christoph	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs
Gligoric, Milos	(CAV) Regression Test Selection for Distributed Software Histories
Glimm, Birte	(VSL) FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (IJCAR) Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures (DL) Abstraction Refinement for Ontology Materialization (DL) Optimised Absorption for Expressive Description Logics
Gliozzi, Valentina	(DL) Rational closure in SHIQ
Gmeiner, Karl	(IWC) On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation (WPTE) On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings (WPTE) Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems
Goasdoué, François	(DL) Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics
Godfroy, Hubert	(LOLA) Abstract Self Modifying Machines
Godo, Lluis	(LATD) Axiomatising a fuzzy modal logic over the standard product algebra
Godoy, Guillem	(SAT) Automatic Evaluation of Reductions between NP-complete Problems (RTA-TLCA) Automatic Evaluation of Context-Free Grammars (System Description) (RTA-TLCA) Tree Automata with Height Constraints between Brothers
Gold, Nicolas	(PLP) Exploring probabilistic grammars of symbolic music using PRISM
Goldsmith, Michael	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Goldstein, Seth	(ICLP) A Linear Logic Programming Language for Concurrent Programming over Graph Structures (CICLOPS-WLPE) A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs
Golinska-Pilarek, Joanna	(ADDCT) On dual tableau-based decision procedures for relational fragments
Gomes, Ana Sofia	(ICLP) Transaction Logic with (Complex) Events
Goncharov, Sergey	(LOLA) Programming and Verifying with Effect Handling and Iteration
Goncharov, Sergey	(LC) Relativized universal numberings
Gondelman, Léon	(CAV) The Spirit of Ghost Code
Gonnord, Laure	(WST) Real-world loops are easy to predict : a case study
Gonschorek, Tim	(VeriSure) A Graphical Notation for Probabilistic Specifications
Gonthier, Georges	(QED) How to prove the odd order from the four color theorem
Goranko, Valentin	(IJCAR) Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+ (LC) On the almost sure validities in the finite in some fragments of monadic second-order logic
Gordon, Mike	(ACL2) Linking ACL2 and HOL: past achievements and future prospects
Gore, Rajeev	(IJCAR) A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (IJCAR) And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (IJCAR) Implementing Tableaux Calculi Using BDDs: BDDTab System Description (VERIFY) Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Gorin, Daniel	(IJCAR) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
Gorogiannis, Nikos	(CSL-LICS) A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates
Gottlob, Georg	(VSL) FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change? (KR) Datalog+/–: Questions and Answers (KR) Stable Model Semantics for Guarded Existential Rules and Description Logics (KR) Polynomial Combined Rewritings for Existential Rules (CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic (CSL-LICS) Decidable languages for knowledge representation and inductive definitions: From Datalog to Datalog+/- (PCCR) Structural Decomposition Methods: How They Matter
Goudsmit, Jeroen	(LC) Characterising Logics through their Admissible Rules (LATD) The Admissible Rules of Subframe Logics
Grabmayer, Clemens	(TermGraph) Nested Term Graphs
Grabowski, Adam	(QED) 25 years of the Mizar Mathematical Library
Gradinariu Potop-Butucaru, Maria	(FRIDA) On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering
Gramegna, Filippo	(ORE) Mini-ME 2.0: powering the Semantic Web of Things
Grant, Dolores	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Grant, Rebecca	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Grathwohl, Niels Bjørn Bugge	(CSL-LICS) KAT + B!
Grebing, Sarah	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs (UITP) How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers (ARW-DT) Automating Regression Verification (ARW-DT) Towards Evaluating the Usability of Interactive Theorem Provers
Greco, Giuseppe	(GSB) Display-type calculi and their cut elimination metatheorem
Green, Matthew	(CSF) Automated Analysis and Synthesis of Block-Cipher Modes of Operation
Greenberg, Noam	(LC) Applications of admissible computability
Gregoire, Benjamin	(CSF) Certified Synthesis of Efficient Batch Verifiers
Grellois, Charles	(ITRS) Indexed linear logic and higher-order model checking (HOPA) The modal nature of colors in higher-order model-checking
Greve, David	(ACL2) Development of a Translator from LLVM to ACL2
Griggio, Alberto	(CAV) The nuXmv Symbolic Model Checker (CAV) Verifying LTL properties of hybrid systems with K-liveness
Grigolia, Revaz	(LATD) On the Logic of Perfect MV-algebras
Grigoriev, Oleg	(LC) Two Formalisms for a Logic of Generalized Truth Values (ARW-DT) Socratic Proofs for Propositional Linear-Time Logic
Grimes, Diarmuid	(RCRA) Dispensable Instantiations in Constraint Satisfaction Problems
Grinchtein, Olga	(SMT) Protocol log analysis with constraint programming
Gritzalis, Dimitris	(PAS) Source code profiling and classification for automated detection of logical errors
Gross, Jason	(Coq) Presentation of Three Neat Tricks in Coq 8.5 (ITP) Experience Implementing a Performant Category-Theory Library in Coq
Grossi, Davide	(KR) Justified Beliefs by Justified Arguments
Grossklags, Jens	(CSF) The Complexity of Estimating Systematic Risk in Networks (CSF) How task familiarity and cognitive predispositions impact behavior in a security game of timing
Grosu, Radu	(HSB) Tutorial: Challenges and opportunities in controlling the human heart
Grov, Gudmund	(UITP) Tinker, tailor, solver, proof
Grumberg, Orna	(VSTTE) Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems (RS) Automated Abstraction-Refinement for the Verification of Behavioral UML Models (iPRA) SAT-Based Model Checking with Interpolation
Grun, Casey	(VEMDP) A domain-level DNA strand displacement reaction enumerator allowing arbitrary non-pseudoknotted secondary structures
Grun, Casey	(VEMDP) DyNAMiC Workbench: Automated design and verification of dynamic DNA nanosystems
Grüninger, Michael	(ARQNL) Proof Support for Common Logic
Gu, Tianlong	(DL) An ABox Revision Algorithm for the Description Logic EL_\bot
Guagliardo, Paolo	(iPRA) Interpolation and Domain Independence applied to Databases
Guan, Shuiwang	(PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Guenot, Nicolas	(CSL-LICS) Equality and Fixpoints in the Calculus of Structures (CSL-LICS) Symmetric Normalisation for Intuitionistic Logic (LFMTP) Hybrid Extensions in a Logical Framework (Linearity) Cut Elimination in Multifocused Linear Logic
Guerrieri, Giulio	(TermGraph) Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion (LC) Natural deduction for intuitionistic differential linear logic (Linearity) A new point of view on the Taylor expansion of proof-nets and uniformity
Guet, Calin	(HSB) Synthetic Systems Biology
Guglielmi, Alessio	(APPA) Deep Inference (NCPROOFS) Introducing Substitution in Proof Theory
Guiraud, Yves	(IWC) Confluence of linear rewriting and homology of algebras
Gunter, Elsa	(LOLA) A Cross-Language Framework for Verifying Compiler Optimizations (WPTE) Verifying Optimizations for Concurrent Programs
Guo, Long	(ParSearchOpt) A Portfolio Based Parallel SAT Solver with Multiple Deletion Strategies
Gupta, Ashutosh	(Vampire) Proofs in Vampire (Vampire) Reasoning in First-Order Theories with Extensionality
Gupta, Gopal	(ICLP) Summer School Closing (ICLP) Dynamic Consistency Checking in Goal-Directed Answer Set Programming (ICLP) Summer School Opening (ICLP) Summer School Opening
Gurfinkel, Arie	(CAV) Interpolating Property Directed Reachability (CAV) SMT-based Model Checking for Recursive Programs (iPRA) Specification Synthesis via Generalized Abduction (iPRA) Interpolation from Clausal Proofs
Gurrin, Brian	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
Gutierrez, Claudio	(KR) Knowledge Maps of Web Graphs
Gutierrez, Julian	(KR) Reasoning about Equilibria in Game-like Concurrent Systems (CSL-LICS) Equilibria of Concurrent Games on Event Structures
Gutiérrez Basulto, Víctor	(KR) Lightweight Description Logics and Branching Time: a Troublesome Marriage
Guttman, Joshua	(FCS-FCC) A Hybrid Analysis for Security Protocols with State (CSF) Decidability for Lightweight Diffie-Hellman Protocols
Gyenis, Zalán	(LC)
H
Haas, Andreas	(FRIDA) A Fast, Correct Time-Stamped Stack
Haase, Christoph	(CSL-LICS) Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
Habič, Miha	(LC) Restricting Martin's axiom to a ccc ground model
Habli, Ibrahim	(VeriSure) Balancing the Formal and Informal in Safety Case Arguments
Hachtman, Sherwood	(LC) Unraveling $\Sigma^0_\alpha(\Pi^1_1)$-Determinacy
Hadarean, Liana	(CAV) A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors
Haeberlen, Andreas	(CSF) Differential Privacy: An Economic Method for Choosing Epsilon
Haeusler, Edward Hermann	(GeTFun) Yoneda’s embedding and Post-completeness
Haeusler, Hermann	(GSB) An Intuitionisticaly based Description Logic (GeTFun) Yoneda’s embedding and Post-completeness (DCM) Propositional Logics Complexity and the sub-formula Property
Haftmann, Florian	(Isabelle) Towards abstract and executable multivariate polynomials in Isabelle
Hagemann, Willem	(CAV) Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections
Hagiya, Masami	(VEMDP) Molecular computers for molecular robots as hybrid systems
Hague, Matthew	(CSL-LICS) Senescent Ground Tree Rewrite Systems (HOPA) Saturation of Concurrent Collapsible Pushdown Systems (Extended Abstract)
Halasz, Adam	(HSB) Collaboration success stories: Membrane-bound Receptor Imaging, Data Analysis and Model Building (with J.S. Edwards)
Hales, Thomas C.	(QED) TBA
Halevy, Alon	(DL) Invited Talk: Structured Data on the Web (or, a Personal Journey Away From and Back To Ontologies)
Hall, Benjamin	(CAV) Finding instability in biological models
Halland, Ken	(DL) TBox abduction in ALC using a DL tableau
Halpern, Joseph	(KR) Appropriate Causal Models and Stability of Causation (KR) Axiomatizing Rationality (FRIDA) Beyond Nash Equilibrium: Solution Concepts for the 21st Century
Hamadi, Youssef	(CAV) Analyzing and Synthesizing Genomic Logic Functions
Hamid, Fahmida	(ICLP) Entanglement Patterns and Logic Programming Language Constructs
Hamilton, Geoff	(VPT) Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem
Hammer, Christian	(FCS-FCC) Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis
Hanikova, Zuzana	(LATD) On satisfiability of terms in FLew-algebras
Hansen, Helle Hvid	(PSC) Observational Equivalence for Behavioural Differential Equations
Hansen, Henri	(CAV) Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions
Hansen, Peter	(DL) Query Rewriting under EL TBoxes: Efficient Algorithms
Hao, Kecheng	(ITP) Mechanical Certification of Loop Pipelining Transformations: A Preview (ACL2) Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
Harbach, Marian	(CSF) Who’s Afraid of Which Bad Wolf? A Survey of IT Security Risk Awareness
Hardin, David	(ACL2) Development of a Translator from LLVM to ACL2
Harel, David	(HSB) The Whole Organism Challenge
Hargreaves, Felix	(EC2) Group Communication Patterns for High Performance Computing in Scala (FRIDA) Correctness and Performance Analysis of Distributed High Performance Programs in Scala
Harrenstein, Paul	(KR) Reasoning about Equilibria in Game-like Concurrent Systems
Harrison, Amelia	(KR) The Semantics of Gringo and Infinitary Propositional Formulas (ASPOCP) Infinitary Equilibrium Logic
Harrison, John	(QED) QED: a grand unified theory? (QED) Panel Discussion
Harrison-Trainor, Matthew	(LC) Degree spectra of relations on a cone
Harwath, Frederik	(CSL-LICS) Preservation and Decomposition Theorems for Bounded Degree Structures
Hasuo, Ichiro	(LOLA) Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (CSL-LICS) The Geometry of Synchronization (CSL-LICS) Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects
Hauesler, Hermann	(GeTFun) An intuitionistic ALC description default logic
Hauesler, Hermann	(GeTFun) Natural deduction for non-deterministic finite-valued logics
Havle, Oto	(VeriSure) Implicit Assumptions in a Model for Separation Kernels (Isabelle) Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
He, Fanny	(WIR) From the finite to the transfinite: Λμ-terms and streams.
Hecher, Markus	(LaSh) The D-FLAT System for Dynamic Programming on Tree Decompositions
Heifetz, Aviad	(LG) Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground
Heijltjes, Willem	(CSL-LICS) No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete (SD) Opening Remarks
Heimberg, Lucas	(CSL-LICS) Preservation and Decomposition Theorems for Bounded Degree Structures
Heitmeyer, Constance	(VeriSure) Assurance and Verification of Security Properties
Heizmann, Matthias	(CAV) Termination Analysis by Learning Terminating Programs (WST) Geometric Series as Nontermination Arguments for Linear Lasso Programs
Hellström, Lars	(IWC) Critical Pairs in Network Rewriting (WST) Ordering Networks
Hempel, Nadja	(LC) Around n-dependent fields
Hendriks, Dimitri	(CSL-LICS) On Periodically Iterated Morphisms (WIR) An Introduction to the Clocked Lambda Calculus
Hensel, Jera	(IJCAR) Proving Termination and Memory Safety for Programs with Pointer Arithmetic
Hentschel, Martin	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs
Henzinger, Thomas	(FRIDA) A Logic-based Framework for Verifying Consensus Algorithms (CAV) Regression-free Synthesis for Concurrency (RS) Quantitative Reactive Modeling (LSB) Model Checking the Evolution of Gene Regulatory Networks
Heras, Jónathan	(ICLP) Guarding Corecursion in Logic Programming (Coq) Proof-Pattern Search in Coq/SSReflect (ACL2) ACL2(ml): Machine-Learning for ACL2
Herbelin, Hugo	(PSC) Computing with Gödel’s completeness theorem
Hermann, Alice	(KR) Belief Revision in the Propositional Closure of a Qualitative Algebra
Hermant, Olivier	(WING) ALICe: A Framework to Improve Affine Loop Invariant Computation
Hermenegildo, Manuel V.	(ICLP) Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types (ICLP) Towards Assertion-based Debugging of Higher-Order (C)LP Programs (CICLOPS-WLPE) Towards Pre-Indexed Terms
Hermo, Montserrat	(QUANTIFY) Projective Quantifier Elimination for Equational Constraint Solving
Hernich, André	(KR) Stable Model Semantics for Guarded Existential Rules and Description Logics
Hertl, Josef	(ASA) Caetus tool
Herzberg, Frederik	(LC) Ultraproduct construction of representative utility functions with infinite-dimensional domain (LATD) Boolean-valued judgment aggregation
Herzig, Andreas	(KR) A Dynamic Logic Framework for Abstract Argumentation (KR) Belief Change Operations: A Short History of Nearly Everything, Told in Dynamic Logic of Propositional Assignments
Hetzl, Stefan	(IJCAR) Introducing quantified cuts in logic with equality
Heule, Marijn	(APPA) Satisfiability Solvers (IJCAR) A Unified Proof System for QBF Preprocessing (SAT) DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (SAT) MUS Extraction using Clausal Proofs (SAT) Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask) (QBF) A Unified Proof System for QBF Preprocessing (POS) Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers
Hewelt, Marcin	(KR4HC) Process Information and Guidance Systems in the Hospital
Heyman, Tamir	(SAT) Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
Hibbs, Peter	(UNIF) Unification Modulo Common List Functions
Hicks, Michael	(FCS-FCC) Adversary Gain vs. Defender Loss in Quantified Information Flow
Higuchi, Kojiro	(LC) The order dimensions of degree structures
Hinchey, Michael	(VSTTE) Separation Kernel Verification: the XtratuM Case Study
Hirokawa, Nao	(IWC) Normalization Equivalence of Rewrite Systems (IWC) Confluence and Critical-Pair-Closing Systems (IWC) Confluence Competition (ITP) A New and Formalized Proof of Abstract Completion (IFIP-WG16) Basic Normalization (RTA-TLCA) Automated Complexity Analysis Based on Context-Sensitive Rewriting
Hitzler, Pascal	(IJCAR) EL-ifying Ontologies (DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs
Hoare, Tony	(RS) A Geometric Model for Concurrent Programming
Hoenicke, Jochen	(CAV) Termination Analysis by Learning Terminating Programs (SMT) Weakly Equivalent Arrays
Hoessen, Benoît	(POS) Dolius: A Distributed Parallel SAT Solving Framework
Hofbauer, Dieter	(WST) On the derivational complexity of Kachinuki orderings
Hoffbeck, Eric	(IWC) Confluence of linear rewriting and homology of algebras
Hofferek, Georg	(iPRA) Tree-based Modular SMT Solving
Hofman, Piotr	(AISS) Simulation for infinite state systems. (CSL-LICS) Infinite-State Energy Games
Hofmann, Martin	(CSL-LICS) Abstract Interpretation from Buchi Automata (RTA-TLCA) Amortised Resource Analysis and Typed Polynomial Interpretations
Holik, Lukas	(CAV) Program Verification through String Rewriting (iPRA) Towards Craig Interpolation for String Constraints
Holzer, Andreas	(EC2) Concolic Testing of Concurrent Programs
Homola, Martin	(DL) Typed Higher-Order Variant of SROIQ - Why Not?
Hong, Hoon	(PAS) Test-Input Generation using Computational Real Algebraic Geometry
Hoos, Holger	(ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming
Horbach, Matthias	(IJCAR) Locality Transfer: From Constrained Axiomatizations to Reachability Predicates (ARW-DT) Modular Verification of Interconnected Families of Uniform Linear Hybrid Automata
Horcik, Rostislav	(LATD) Densification via polynomial extensions
Horrocks, Ian	(IJCAR) EL-ifying Ontologies (DL) Pay-as-you-go Ontology Query Answering Using a Datalog Reasoner (DL) OptiqueVQS: Visual Query Formulation for OBDA (DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs (DL) Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems
Horsten, Leon	(LC) Reflection, Trust, Entitlement
Horvat, Marko	(CSF) Actor Key Compromise: Consequences and Countermeasures
Hoshino, Naohiko	(LOLA) Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (CSL-LICS) Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects
Hostettler, Steve	(FWFM) Introducing Formal Verification with Lego
Hou, Ping	(ARQNL) A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems
Hou, Tie	(PSC) Program extraction in Church's simple theory of types (invited talk)
Hou, Xiaomei	(PAS) A hybrid path constraint solver combined with meta-heuristic search
Houston, Robin	(CSL-LICS) No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete
Hritcu, Catalin	(Coq) QuickChick: Property-Based Testing for Coq (FCS-FCC) Micro-Policies: Formally Verified Low-Level Tagging Schemes for Safety and Security (Short Paper)
Hsu, Justin	(CSF) Differential Privacy: An Economic Method for Choosing Epsilon (CSF) Proving differential privacy in Hoare logic (DCM) Differential privacy at work: Verification of approximate probabilistic programs and models for choosing epsilon
Huang, Chung-Hao	(CAV) G4LTL-ST: Automatic Generation of PLC Programs
Huang, Hao	(PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Huang, Wei	(PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Huang, Xiaowei	(KR) A Temporal Logic of Strategic Knowledge
Huang, Zhenqi	(CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells
Huang, Zhisheng	(KR4HC) Semantic Representation of Evidence-based Clinical Guidelines
Hughes, Dominic	(CLC) Separable Sequent Calculus for First-order Classical Logic (Work in Progress) (GSB) Simpler Proof Net Quantifiers: Unification Nets (Work in Progress) (SD) First-order Proofs Without Syntax: Summary of Work in Progress
Hulette, Geoffrey C.	(NSV) Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics
Hungar, Hardi	(VeriSure) Introducing Semi-Formal Specifications into a Distributed Development Process
Hunt, Warren	(SAT) DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
Hunter, Aaron	(NMR) Belief Revision and Trust
Hunter, Anthony	(NMR) Analysis of Dialogical Argumentation via Finite State Machines
Hunter, Paul	(LCC) First-Order Logic of Order and Metric has the Three-Variable Property
Husam, Husam	(SAT) Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
Hyttinen, Tapani	(INFINITY) Infinitely deep languages and neighbors
Hähnle, Reiner	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs (VERIFY) Introducing a Sound Deductive Compilation Approach
Höfner, Peter	(ITP) Showing invariance compositionally for a process algebra for network protocols
Höhnerbach, Markus	(PRUV) Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics
Hölldobler, Steffen	(POS) Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers
Hölzl, Johannes	(ITP) Recursive Functions on Codatatypes via Domains and Topologies (ITP) Truly Modular (Co)datatypes for Isabelle/HOL (Isabelle) A formally verified proof of the Central Limit Theorem
Hölzl, Rupert	(LC) Randomness in the Weihrauch degrees
I
Ianovski, Egor	(KR) ∃GUARANTEENASH for Boolean Games Is NEXP-Hard
Ibanez-Garcia, Yazmin	(KR) Finite Model Reasoning in Horn Description Logics
Iemhoff, Rosalie	(SD) Completions and the Schuette method (LATD) Cut and completion?
Ieva, Saverio	(ORE) Mini-ME 2.0: powering the Semantic Web of Things
Ignatiev, Alexey	(SAT) On Reducing Maximum Independent Set to Minimum Satisfiability (RCRA) Maximal Falsifiability: Definitions, Algorithms, and Applications
Ikegami, Daisuke	(LC) Large cardinals, forcing axioms, and the theory of subsets of \omega_1
Ilic, Mirjana	(LC) An Intuitionistic Interpretation of Classical Implication
Ilik, Danko	(CSL-LICS) Axioms and Decidability for Type Isomorphism in the Presence of Sums (PSC) Computing with Gödel’s completeness theorem
Immerman, Neil	(LCC) Closing Remarks
Inaba, Mary	(SAT) Community Branching for Parallel Portfolio SAT Solvers
Incurvati, Luca	(LC) Restrictiveness relative to notions of interpretation
Inverso, Omar	(CAV) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
Ionescu, Cezar	(DTP) Sequential decision problems and a computational theory of avoidability (DTP) Domain Specific Languages of Mathematics
Ipate, Florentin	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Ireland, Andrew	(VSTTE) A Verification Condition Visualizer
Irigoin, François	(WING) ALICe: A Framework to Improve Affine Loop Invariant Computation
Ishtiaq, Samin	(CAV) Finding instability in biological models
Issakhov, Assylbek	(LC) Ideals without minimal numberings in the Rogers semilattice
Istrate, Gabriel	(SAT) Proof complexity and the Lovasz-Kneser Theorem (DCM) Interactive Particle Systems and Random Walks on Hypergraphs
Itsykson, Dmitry	(PC) Lower bounds for splittings by linear combinations
Itzhaky, Shachar	(CAV) Property-Directed Shape Analysis
Ivanov, Alexandre	(LC) Extreme amenability of precompact expansions of countably categorical structures
Ivanova, Marieta Georgieva	(STAST) Modeling Human Behaviour with Higher Order Logic: Insider Threats
J
Jabbour, Said	(ParSearchOpt) A Portfolio Based Parallel SAT Solver with Multiple Deletion Strategies (POS) Dolius: A Distributed Parallel SAT Solving Framework
Jackson, Ethan K.	(ICLP) A Module System for Domain-Specific Languages
Jackson, Paul	(PAS) A note on real quantifier elimination by virtual term substitution of unbounded degree
Jacobs, Swen	(FRIDA) Parameterized Synthesis (FRIDA) Synthesis for Resilient Distributed Systems (CAV) SYNTCOMP - Synthesis Competition for Reactive Systems (SYNT) The 1st Synthesis Competition for Reactive Systems (SyntComp) (SYNT) Parameterized Synthesis Case Study: AMBA AHB (SYNT) How to Handle Assumptions in Synthesis
Jacot, Justine	(LG) Game Semantics from a Cognitive Modeling Standpoint
Jacquemard, Florent	(IFIP-WG16) Rhythm Tree Rewriting
Jaeger, Gerhard	(CSL-LICS) Weak well orders and related inductions
Jagadeesan, Radha	(CSF) Certificates for Verifiable Forensics
Jagannathan, Suresh	(EC2) Atomicity Refinement for Verified Compilation
Jagiella, Grzegorz	(LC) Definable topological dynamics and real Lie groups
Jameel, Tahir	(PAS) A hybrid path constraint solver combined with meta-heuristic search
Jami, Madiha	(VSTTE) A Verification Condition Visualizer
Janhunen, Tomi	(KR) ASP Encodings of Acyclicity Properties (LaSh) Cross-Translating Answer Set Programs (ASPOCP) Declarative Encodings of Acyclicity Properties
Janota, Mikoláš	(QBF) Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs (QBF) On Instantiation-Based Calculi for QBF
Jansana, Ramon	(LATD) Generalizing the Leibniz and Suszko operators (LATD) Congruential deductive systems associated with equationally orderable varieties
Jansen, Joachim	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories (LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development (ICLP) Model Revision Inference for Extensions of First Order Logic (CICLOPS-WLPE) Refining definitions with unknown opens using XSB for IDP3
Janssens, Gerda	(PLP) cProbLog: Restricting the Possible Worlds of Probabilistic Logic Programs (LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development (CICLOPS-WLPE) Refining definitions with unknown opens using XSB for IDP3
Jansson, Patrik	(DTP) Sequential decision problems and a computational theory of avoidability (DTP) Domain Specific Languages of Mathematics
Jaśkiewicz, Grzegorz	(ICLP) Logic Programming as Scripting Language for Bots in Computer Games
Jeannin, Jean-Baptiste	(IJCAR) dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems
Jeffrey, Alan	(DTP) FRP, LTL and GUIs (CSL-LICS) Functional Reactive Types
Jegou, Philippe	(CSPSAT) Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms
Jenei, Sándor	(LATD) Recent advances in the structural description of involutive FL$_e$-chains
Jeske, Debora	(STAST) Decision justifications for wireless network selection
Jeřábek, Emil	(PC) Parameter-free induction in bounded arithmetic
Jha, Somesh	(CSL-LICS) Satisfiability Modulo Counting: A New Approach for Analyzing Privacy Properties
Jha, Susmit	(SYNT) Are There Good Mistakes? A Theoretical Analysis of CEGIS
Ji, Jianmin	(NMR) Implementing Default and Autoepistemic Logics via the Logic of GK
Ji, Ran	(VERIFY) Introducing a Sound Deductive Compilation Approach
Jia, Limin	(CAV) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies
Jiang, Dongchen	(PAS) The Verification of Conversion Algorithms between Finite Automata
Jiang, Jie-Hong Roland	(SAT) QBF Resolution Systems and their Proof Complexities (QBF) Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Jiang, Ying	(IFIP-WG16) Rewriting, Proofs and Transition Systems
Jimenez-Ruiz, Ernesto	(DL) OptiqueVQS: Visual Query Formulation for OBDA
Jipsen, Peter	(LATD) The lattice of varieties generated by small residuated lattices
Johannsen, Jacob	(TermGraph) Needed Computations Shortcutting Needed Steps
Johannsen, Jan	(PC) Size-Space Bounds and Trade-offs for CDCL Proofs (PCCR) Backdoors into Two Occurrences
Johnson, Benjamin	(CSF) The Complexity of Estimating Systematic Risk in Networks
Johnson, Robert F.	(VEMDP) Verifying Polymer Reaction Networks using Bisimulation
Jones, Alison	(NLCS) Program Extraction Applied to Monadic Parsing (PSC) Extracting Monadic Parsers from Proofs
Jones, Cliff B.	(VSTTE) A Model for Capturing and Replaying Proof Strategies
Joosten, Joost	(LC) Provability logics and proof-theoretic ordinals
Joosten, Sebastiaan	(ACL2) Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
Jordan, Charles	(SAT) MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing (QBF) The QBF Gallery 2014
Jouannaud, Jean-Pierre	(RTA-TLCA) Confluence by Critical Pair Analysis
Jovanović, Dejan	(CAV) A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (SAT) A Model-Constructing Satisfiability Calculus
Judge, Mark	(ARW-DT) (AI) Planning to Reconfigure your Robot? (ARW-DT) Using CSP Meta Variables in AI Planning
Jung, Jean Christoph	(KR) Lightweight Description Logics and Branching Time: a Troublesome Marriage
Jungnickel, Tim	(FRIDA) Mechanical Verification of a Constructive Proof for FLP
Juniwal, Garvit	(CAV) Finding instability in biological models
Järvisalo, Matti	(SAT) Conditional Lower Bounds for Failed Literals and Related Techniques (LaSh) Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability (RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
K
Kaci, Souhila	(NMR) Abduction in Argumentation: Dialogical Proof Procedures and Instantiation
Kafle, Bishoksan	(ICLP) Analysis and Transformation Tools for Constrained Horn Clause Verification
Kahl, Patrick	(ASPOCP) A Refinement of the Language of Epistemic Specifications (ASPOCP) Epistemic Logic Programs with Sorts
Kahl, Wolfram	(DCM) A Simple Parallel Implementation of Interaction Nets in Haskell
Kahle, Reinhard	(LCC) Towards recursion schemata for the probablistic class PP
Kahrs, Stefan	(WIR) Normal Forms and Infinity
Kaiser, Lukasz	(SAT) MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
Kakas, Antonis	(KR) A Psychology-Inspired Approach to Automated Narrative Text Comprehension (LC) Argumentation Logic (NMR) Non-Monotonic Reasoning and Story Comprehension
Kalimullin, Iskander	(LC) On limitwise monotonic reducibility of Σ^0_2-sets. (LC) Limitwise monotonic sets of reals (LC) Uniform and non-uniform reducibilities of algebraic structures
Kaliszyk, Cezary	(ACL2) Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (PAAR) Beagle as a HOL4 external ATP method (PAAR) Machine Learner for Automated Reasoning 0.4 and 0.5 (QED) Hammering towards QED
Kalvala, Sara	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Kamal, Amroun	(RCRA) A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary CSP
Kaminski, Mark	(DL) Datalog Rewriting Techniques for Non-Horn Ontologies
Kaminski, Roland	(ICLP) Clingo = ASP + Control
Kammueller, Florian	(STAST) Modeling Human Behaviour with Higher Order Logic: Insider Threats
Kanav, Sudeep	(CAV) A Conference Management System with Verified Document Confidentiality
Kanazawa, Makoto	(NLCS) Toward a Logic of Cumulative Quantification
Kang, Juyeon	(NLCS) Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts
Kanovei, Vladimir	(LC) A generalization of Solovay's Sigma-construction with application to intermediate models
Kanovich, Max	(FCS-FCC) Towards Timed Models for Cyber-Physical Security Protocols
Kapinski, Jim	(NSV) Numerical Challenges in Simulation-guided Dynamical System Analysis
Kapur, Deepak	(UNIF) Hierarchical Combination of Matching Algorithms (Extended Abstract) (UNIF) On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
Karimi, Ahmad	(LC) A universal diagonal schema by fixed-points and Yablo’s paradox
Karthik, Aadithya V.	(VEMDP) Boolean modelling and formal verification of tiered-rate chemical reaction networks
Kaski, Samuel	(RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
Kataoka, Takumi	(WST) On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants
Kataoka, Toshiki	(LOLA) Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction
Kato, Tomofumi	(WPTE) Inverse Unfold Problem and Its Heuristic Solving
Katoen, Joost-Pieter	(CAV) GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components (CSL-LICS) Zero-Reachability in Probabilistic Multi-Counter Automata (CSL-LICS) Probably Safe or Live
Katsaros, Panagiotis	(PAS) Source code profiling and classification for automated detection of logical errors
Katsoris, Georgios	(CSF) A Sound Abstraction of the Parsing Problem
Katz, Jonathan	(CSF) Automated Analysis and Synthesis of Block-Cipher Modes of Operation
Kaufmann, Benjamin	(ICLP) Clingo = ASP + Control
Kaufmann, Matt	(ITP) Rough Diamond: An Extension of Equivalence-based Rewriting (ACL2) Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (ACL2) Industrial-Strength Documentation for ACL2
Kaynar, Dilsun	(FCS-FCC) Actual Causes of Security Violations
Kazakov, Yevgeny	(DL) Abstraction Refinement for Ontology Materialization (DL) Goal-Directed Tracing of Inferences in EL Ontologies (DL) Bridging the Gap between Tableau and Consequence-Based Reasoning
Kazemi, Seyed Mehran	(KR) Relational Logistic Regression
Keet, C. Maria	(DL) Transition Constraints for Temporal Attributes (ORE) Exploring Reasoning with the DMOP Ontology
Keller, Chantal	(PAAR) Beagle as a HOL4 external ATP method
Kelly, Tim	(VeriSure) Balancing the Formal and Informal in Safety Case Arguments
Kerber, Manfred	(ARW-DT) Reasoning about Auctions
Kerhet, Volha	(iPRA) Interpolation and Domain Independence applied to Databases
Kerjean, Marie	(SD) Weak topologies for Linear Logic
Kern-Isberner, Gabriele	(PRUV) TBA
Kersting, Kristian	(KR) Relational Logistic Regression
Kesala, Meeri	(LC) Quasiminimal structures and excellence
Kesner, Delia	(Linearity) The inhabitation problem for non-idempotent intersection
Ketema, Jeroen	(CAV) Engineering a Static Verification Tool for GPU Kernels (WST) Automatic Termination Analysis for GPU Kernels
Khadir, Tarek	(DL) Reasoning about Belief Uncertainty in DL-Lite N bool (PRUV) A New DL‐Lite N Bool Probabilistic Extension Using Belief
Khalimov, Ayrat	(SYNT) Parameterized Synthesis Case Study: AMBA AHB
Khan, Wilayat	(CSF) Provably Sound Browser-Based Enforcement of Web Session Integrity
Khan, Zubeida	(ORE) Exploring Reasoning with the DMOP Ontology
Khandelwal, Piyush	(ASPOCP) Applying Action Language BC with Hierarchical Domain Abstraction to Mobile Robots
Khanna, Sanjeev	(CSF) Differential Privacy: An Economic Method for Choosing Epsilon
Kharlamov, Evgeny	(DL) OptiqueVQS: Visual Query Formulation for OBDA (DL) On Faceted Search over Knowledge Bases (DL) Controlled Query Evaluation over Lightweight Ontologies
Khlaaf, Heidy	(WST) Fairness for Infinite-State Systems
Khoussainov, Bakhadyr	(LC) On finitely presented expansions of groups and algebras (CSL-LICS) A quest for algorithmically random infinite structures
Kiefer, Stefan	(CSL-LICS) Zero-Reachability in Probabilistic Multi-Counter Automata (CSL-LICS) On the Total Variation Distance of Labelled Markov Chains
Kieronski, Emanuel	(CSL-LICS) Decidability of Weak Logics with Deterministic Transitive Closure
Kikot, Stanislav	(CSL-LICS) On the Succinctness of Query Rewriting over OWL 2 QL Ontologies with Bounded Chase (DL) Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries
Kikuchi, Kentaro	(CLC) A Translation of Intersection and Union Types for the lambda-mu Calculus (ITRS) Uniform Proofs of Normalisation and Approximation for Intersection Types
Kiljan, Sven	(STAST) What You Enter Is What You Sign: input integrity in an online banking environment
Kimmig, Angelika	(PLP) PageRank, ProPPR and Stochastic Logic Programs
King, Tim	(SMT) Leveraging Linear and Mixed Integer Programming for SMT (ADDCT) Finding Minimum Type Error Sources
Kirchner, Claude	(IFIP-WG16) Discussion on Massive Open Online Courses and Overlay Journals (IFIP-WG16) Impacts of the Digital Revolution on two Main Activities of Scientists: Teaching and Publishing
Kirchner, Florent	(FWFM) Chekofv: Crowd-sourced Formal Verification
Kirsch, Christoph	(FRIDA) A Fast, Correct Time-Stamped Stack
Kirsten, Michael	(VERIFY) Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Kisa, Doga	(KR) Probabilistic Sentential Decision Diagrams
Kislak-Malinowska, Aleksandra	(NLCS) Computing Italian clitic and relative clauses with tupled pregroups
Kissinger, Aleks	(UITP) Tinker, tailor, solver, proof
Klarman, Szymon	(DL) TBox abduction in ALC using a DL tableau
Klarman, Szymon	(DL) Complexity of Temporal Query Abduction in DL-Lite
Klaska, David	(CAV) Minimizing Running Costs in Consumption Systems
Klebanov, Vladimir	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs (ARW-DT) Automating Regression Verification
Klein, Gerwin	(QED) The seL4 microkernel verification
Klein, Joachim	(CSL-LICS) Weight Monitoring with Linear Temporal Logic: Complexity and Decidability
Klin, Bartek	(CSL-LICS) Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity
Klinov, Pavel	(DL) Goal-Directed Tracing of Inferences in EL Ontologies (DL) Bridging the Gap between Tableau and Consequence-Based Reasoning
Klop, Jan Willem	(WIR) An Introduction to the Clocked Lambda Calculus
Klueppelholz, Sascha	(CSL-LICS) Weight Monitoring with Linear Temporal Logic: Complexity and Decidability (CSL-LICS) Trade-Off Analysis Meets Probabilistic Model Checking
Kluka, Jan	(DL) Typed Higher-Order Variant of SROIQ - Why Not?
Knight, Julia	(LC) Computable structure theory and formulas of special forms (INFINITY) Computing a floor function
Knoop, Jens	(PAS) Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis
Ko, Hsiang-Shang	(DTP) Relational ornaments
Koenig, Barbara	(RTA-TLCA) Termination of Cycle Rewriting
Koenighofer, Robert	(QBF) Reactive Synthesis using (Incremental) QBF Solving (SYNT) How to Handle Assumptions in Synthesis
Koerwien, Martin	(LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes (INFINITY) When excellence and local finiteness collide
Kogabaev, Nurlan	(LC) The isomorphism problem for computable projective planes
Kohlhase, Michael	(QED) MathHub.info: Active Mathematics
Kohlweiss, Markulf	(CSF) Malleable Signatures: New Definitions and Delegatable Anonymous Credentials
Kojima, Ryosuke	(PLP) Prefix and infix probability computation in PRISM
Kolaitis, Phokion	(LCC) Some Reflections on Definability and Complexity
Kolanski, Rafal	(LOLA) On Machines, Virtual Memory and Successful System Verification
Kolodziejczyk, Leszek	(LC) The problem of a model without collection and without exponentiation
Komendantskaya, Ekaterina	(ICLP) Guarding Corecursion in Logic Programming (Coq) Proof-Pattern Search in Coq/SSReflect (ACL2) ACL2(ml): Machine-Learning for ACL2
Komuravelli, Anvesh	(CAV) SMT-based Model Checking for Recursive Programs
Kondoh, Shuya	(SAT) Community Branching for Parallel Portfolio SAT Solvers
Konev, Boris	(KR) Exact Learning of Lightweight Description Logic Ontologies (KR) Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference (SAT) A SAT Attack on the Erdos Discrepancy Conjecture (DL) Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies
Konieczny, Sébastien	(KR) On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses (KR) On Egalitarian Belief Merging
Konikowska, Beata	(GeTFun) Effective first-order reasoning about incomplete and inconsistent information
Kontchakov, Roman	(KR) Query Inseparability for Description Logic Knowledge Bases (CSL-LICS) On the Succinctness of Query Rewriting over OWL 2 QL Ontologies with Bounded Chase (DL) Query Inseparability by Games (DL) Temporal OBDA with LTL and DL-Lite
Konur, Savas	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Koopmann, Patrick	(IJCAR) Count and Forget: Uniform Interpolation of SHQ-Ontologies (DL) Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes (ARW-DT) Computing Uniform Interpolants of ALCH-Ontologies with Background Knowledge (iPRA) Resolution Based Uniform Interpolation for Expressive Description Logics
Kop, Cynthia	(RTA-TLCA) First-Order Formative Rules (HOR) The Higher-order Dependency Pair Framework
Korhonen, Janne H.	(SAT) Conditional Lower Bounds for Failed Literals and Related Techniques
Korovin, Konstantin	(LaSh) Instantiation-based reasoning, EPR encodings and all that
Korovin, Konstantin	(SMT) Towards Conflict-Driven Learning for Virtual Substitution
Koskinen, Eric	(CSL-LICS) Local Temporal Reasoning
Kosta, Marek	(SMT) Towards Conflict-Driven Learning for Virtual Substitution (SMT) Better Answers to Real Questions
Kostrzycka, Zofia	(LC) On Hallden complete modal logics determined by homogeneous frames
Kostylev, Egor V.	(DL) XPath for DL-Lite Ontologies (DL) Controlled Query Evaluation over Lightweight Ontologies
Kotek, Tomer	(AISS) Parameterized Model Checking of Rendezvous Systems (DL) Shape and Content: Incorporating Domain Knowledge into Shape Analysis (DL) Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability (FWFM) Explaining the decompositionality of MSO using applications to combinatorics
Kotelnikov, Evgeny	(Vampire) First Class Boolean Type in First-Order Theorem Proving and TPTP
Kovacs, Laura	(Vampire) First Class Boolean Type in First-Order Theorem Proving and TPTP (Vampire) First-Order Theorem Proving with Vampire (Vampire) Reasoning in First-Order Theories with Extensionality (Vampire) Discussions (Vampire) SAT solving experiments in Vampire (iPRA) Discussions (iPRA) Concluding discussions (PAS) Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis
Kovalev, Mikhail	(VSTTE) Store Buffer Reduction with MMUs
Kovtunova, Alisa	(DL) Temporal OBDA with LTL and DL-Lite
Kovásznai, Gergely	(QUANTIFY) EPR Encodings of Bit-Vector Problems Even With Quantifiers (LCC) On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic (POS) iDQ: Instantiation-Based DQBF Solving
Kowalski, Tomasz	(GSB) Link formulas in implication fragments of substructural logics
Kozen, Dexter	(CSL-LICS) Citations for the Test-of-Time Award from 1994 (CSL-LICS) KAT + B!
Kragl, Bernhard	(Vampire) Reasoning in First-Order Theories with Extensionality
Krasnogor, Natalio	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Kraus, Lydia	(STAST) Using Statistical Information to Communicate Android Permission Risks to Users
Krebbers, Robbert	(VSTTE) Separation algebras for C verification in Coq (ITP) Formal C semantics: CompCert and the C standard
Kretinsky, Jan	(CAV) From LTL to Deterministic Automata: A Safraless Compositional Approach
Kreutzer, Stephan	(CSL-LICS) On Hanf-equivalence and the number of embeddings of small induced subgraphs (CSL-LICS) Decomposition Theorems and Model-Checking for the Modal mu-calculus
Kriener, Jael	(ARQNL) Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Krivine, Jean	(VEMDP) Rule based modelling of DNA repair
Kroening, Daniel	(CAV) Don't sit on the fence: A static analysis approach to automatic fence insertion (HCVS) Invited talk: Proof and Refutations for Horn-clause Encodings of Reachability Problems
Kroll, Joshua	(CSF) Portable Software Fault Isolation
Kronegger, Martin	(QBF) Conformant Planning as a Case Study of Incremental QBF Solving (PCCR) Backdoors to Planning (PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets
Kropotin, Alexander	(ORE) Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software Development
Kroupa, Tomáš	(LATD) Constructing many-valued logical functions with small influence of their variables
Krötzsch, Markus	(KR) Nominal Schemas in Description Logics: Complexities Clarified (DL) Complexities of Nominal Schemas (DL) How to Best Nest Regular Path Queries
Kuan, George	(CSF) Information flow monitoring as abstract interpretation for relational logic
Kucera, Antonin	(CAV) Minimizing Running Costs in Consumption Systems (CSL-LICS) Zero-Reachability in Probabilistic Multi-Counter Automata
Kugler, Hillel	(CAV) Analyzing and Synthesizing Genomic Logic Functions (RS) On Statecharts, Scenarios and Biological Modeling
Kullmann, Oliver	(SAT) Unified characterisations of resolution hardness measures
Kulpeshov, Beibut	(LC) Some remarks on $\aleph_0$-categorical weakly circularly minimal structures
Kumar, Ramana	(ITP) HOL with Definitions: Semantics, Soundness, and a Verified Implementation (HOL) Discussion Session (HOL) Hack Session 3 (HOL) Welcome (HOL) Hack Session 1 (HOL) New Styles of Proof (HOL) Hack Session 2 (QED) Towards Formally Verified Theorem Provers - Part II
Kumar Jha, Sumit	(NSV) Verifying Parameterized Software Models in Computational Data Science against Behavioral Specifications
Kuncak, Viktor	(CAV) Symbolic Resource Bound Inference for Functional Programs (SYNT) Automating Deductive Synthesis with Leon (Invited Talk)
Kunz, Cesar	(CSF) Proving differential privacy in Hoare logic
Kunčar, Ondřej	(Isabelle) From Types to Sets in Isabelle/HOL
Kuperberg, Denis	(CSL-LICS) Two-Way Cost Automata and Cost Logics over Infinite Trees
Kupfermann, Orna	(VSL) FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory
Kupke, Clemens	(KR) Stable Model Semantics for Guarded Existential Rules and Description Logics
Kupriyanov, Andrey	(CAV) Causal Termination of Multi-threaded Programs
Kurt Gödel Research Prize Fellowships Program,	(VSL) Foundations and Technology Competitions Award Ceremony
Kurz, Alexander	(GSB) Display-type calculi and their cut elimination metatheorem
Kusakari, Keiichirou	(RTA-TLCA) Nagoya Termination Tool (System Description)
Kutsia, Temur	(UNIF) Opening
Kutsia, Temur	(UNIF) Nominal Anti-Unification (PAS) Confluence of Pattern-Based Calculi with Finitary Matching
Kutz, Oliver	(ARQNL) Proof Support for Common Logic
Kuyper, Rutger	(LC) Effective genericity and differentiable functions
Kuznets, Roman	(NCPROOFS) Applications of Nested-Sequent Proof Systems for Modal Logics to the Craig Interpolation Property (GeTFun) Separating truth and proof in the Logic of Proofs
Kuznetsov, Stepan	(NLCS) On Translating Context-Free Grammars into Lambek Categorial Grammars
Kwiatkowska, Marta	(CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells (VEMDP) Opening remarks (RS) Probabilistic model checking at the nanoscale: from molecular signalling to molecular walkers
Kwiatkowska, Marta	(VEMDP) Guiding the development of DNA walker systems to guarantee reliability and performance
Kyriakopoulos, Charalampos	(HSB) Optimal Observation Time Points in Stochastic Chemical Kinetics
Königsmann, Jochen	(LC) Definable valuation rings
L
La Torre, Salvatore	(CAV) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
Labai, Nadia	(PCCR) Connection matrices of finite rank instead of definability in Monadic Second Order Logic
Labich, Nicholas	(HOPA) Analyzing JavaScript: The Bad Parts
Lackner, Martin	(PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets
Ladroue, Christophe	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Lager, Torbjörn	(ICLP) Pengines: Web Logic Programming Made Easy
Lahav, Ori	(NCPROOFS) From Frame Properties to Hypersequent Rules in Modal Logics (GSB) On the Construction of Analytic Sequent Calculi for Sub-classical Logics (IJCAR) SAT-based Decision Procedure for Analytic Pure Sequent Calculi (LATD) Cut-free calculus for second-order {G\"odel} logic
Lakemeyer, Gerhard	(KR) On the Progression of Knowledge in Multiagent Systems (KR) Decidable Reasoning in a Fragment of the Epistemic Situation Calculus
Lam, Edmund Soon Lee	(CHR) Constraint Handling Rules with Multiset Comprehension Patterns (SMT) Reasoning About Set Comprehensions
Lamma, Evelina	(ICLP) Lifted Variable Elimination for Probabilistic Logic Programming
Lammich, Peter	(CAV) A Conference Management System with Verified Document Confidentiality (ITP) Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm (Isabelle) The CAVA Automata Library (Isabelle) The CoCon Experiment
Lampis, Michael	(LCC) Closing a Gap in the Complexity of Refinement Modal Logic
Lamport, Leslie	(ARQNL) Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Lampropoulos, Leonidas	(Coq) QuickChick: Property-Based Testing for Coq
Lang, Martin	(AISS) Quantitative Automatic Structures
Lange, Christoph	(ARQNL) Proof Support for Common Logic (ARW-DT) Reasoning about Auctions
Lange, Martin	(IJCAR) A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (LCC) Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
Langenstein, Bruno	(Isabelle) Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
Lanti, Davide	(ORE) A Scalable Benchmark for OBDA Systems: Preliminary Report
Lapenta, Serafina	(LATD) On tensor product in Lukasiewicz logic (LATD) MV-algebras with product and the Pierce-Birkhoff conjecture
Laporte, Vincent	(ITP) Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
Lara-Martin, Andres Cordon-Franco And F. Felix	(LC) Pi_1 induction axioms vs Pi 1 induction rules (LC) On local induction schemes
Larraz, Daniel	(CAV) Proving Non-termination Using Max-SMT (SAT) Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
Lash,	(LaSh) LaSh and QUANTIFY Openings
Laskowski, Michael C.	(LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes (INFINITY) When excellence and local finiteness collide
Lasota, Sławomir	(CSL-LICS) Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity
Laszka, Aron	(CSF) The Complexity of Estimating Systematic Risk in Networks
Laud, Peeter	(CSF) From input private to universally composable secure multiparty computation primitives
Laur, Sven	(CSF) From input private to universally composable secure multiparty computation primitives
Lauria, Massimo	(PC) From Small Space to Small Width in Resolution (PC) Narrow Proofs May Be Maximally Long (PC) Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds (PC) Size-Space Bounds and Trade-offs for CDCL Proofs
Lawrence, David	(FWFM) Introducing Formal Verification with Lego
Lawrynowicz, Agnieszka	(ORE) Exploring Reasoning with the DMOP Ontology
Lazić, Ranko	(CSL-LICS) Non-Elementary Complexities for Branching VASS, MELL, and Extensions
Le, Quang Loc	(CAV) Shape Analysis via Second-Order Bi-Abduction
Le, Tiep	(ICLP) Logic and Constraint Logic Programming for Distributed Constraint Optimization
Le, Xuan Hung	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
Le Ber, Florence	(KR) Belief Revision in the Propositional Closure of a Qualitative Algebra
Le Berre, Daniel	(SAT) Detecting cardinality constraints in CNF (POS) Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem (NMR) Some thoughts about benchmarks for NMR
Le Roux, Stephane	(CSL-LICS) Infinite sequential games with real-valued payoffs
Le Sueur, Chris	(LC) Determinacy of Refinements to the Difference Hierarchy of Co-analytic sets
Lederman, Harvey	(LC) Prospects for a Naive Theory of Classes
Ledesma-Garza, Ruslán	(CAV) An SMT-Based Approach to Coverability Analysis
Lee, Joohyung	(KR) Stable Models of Multi-Valued Formulas: Partial vs. Total Functions (PRUV) Stable Models of Fuzzy Propositional Formulas (ASPOCP) Action Language BC+: Preliminary Report
Lee, Jui-Lin	(LC) Explosiveness, Model Existence, and Incompatible Paraconsistencies
Lee, Suho	(CAV) Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction
Legg, Alexander	(CAV) Solving Games without Controllable Predecessor (iPRA) Practical CNF Interpolants Via BDDs (iPRA) Interpolants in Two-Player Games
Legg, Philip	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Leike, Jan	(WST) Geometric Series as Nontermination Arguments for Linear Lasso Programs
Leite, Joao	(ICLP) On Strong and Default Negation in Answer-Set Program Updates (NMR) On Strong and Default Negation in Logic Program Updates
Leitsch, Alexander	(APPA) Mathematical Proof Analysis (CLC) Cut-Elimination in Schematic Proofs and Herbrand Sequents (IJCAR) Introducing quantified cuts in logic with equality (LC) The place of logic in computer science education
Lellmann, Björn	(GSB) Comparing Sequent Calculi via Hilbert-style Axioms (IJCAR) Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
Lembo, Domenico	(DL) Graphol: Ontology representation through diagrams (DL) Visualization and management of mappings in ontology-based data access (progress report)
Lenzerini, Maurizio	(DL) Practical query answering over Hi (DL-LiteR) knowledge bases (DL) Reducing global consistency to local consistency in Ontology-based Data Access - Extended Abstract
Lenzi, Giacomo	(LC) On Uniform Interpolation for the Guarded Fragment (LATD) On the Logic of Perfect MV-algebras
Leo, Jared	(DL) Temporalising EL Concepts with Time Intervals
Leong, Lance	(SAT) Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
Lepore, Lorenzo	(DL) Practical query answering over Hi (DL-LiteR) knowledge bases
Leroux, Jerome	(CSL-LICS) Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems
Leroy, Xavier	(ITP) Formal C semantics: CompCert and the C standard
Lesani, Mohsen	(CAV) Automatic Atomicity Verification for Clients of Concurrent Data Structures
Leslie-Hurd, Joe	(CAV) Verifying Relative Error Bounds using Symbolic Simulation
Letichevsky, Alexander	(PAS) New predicate transformer for symbolic modeling
Letychevskyi, Oleksandr	(PAS) New predicate transformer for symbolic modeling
Leuschel, Michael	(HCVS) Invited talk: Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools
Leustean, Ioana	(LATD) On tensor product in Lukasiewicz logic (LATD) MV-algebras with product and the Pierce-Birkhoff conjecture
Leustean, Laurentiu	(LC) Effective results on the asymptotic behavior of nonexpansive iterations
Levesque, Hector J.	(KR) Decidable Reasoning in a Fragment of the Epistemic Situation Calculus (KR) Forgetting in Action (KR) How To Progress Beliefs in Continuous Domains
Levy, Jordi	(UNIF) Nominal Anti-Unification (UNIF) On the Limits of Second-Order Unification (IJCAR) The Fractal Dimension of SAT Formulas
Levy, Paul Blain	(CSL-LICS) Transition systems over games
Lewis, Robert Y.	(ITP) A heuristic prover for real inequalities
Leyva Galano, José A.	(DL) Gödel FL_0 with Greatest Fixed-Point Semantics
Lhoussaine, Cedric	(WPTE) Attractor Equivalence: An Observational Semantics for Reaction Networks (LSB) Attractor equivalence: An observational semantics for reaction networks
Li, Kangjie	(PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Li, Nuo	(LFMTP) Some constructions on ω-groupoids
Li, Sanjiang	(KR) On Redundant Topological Constraints (Extended Abstract)
Li, Wei	(PAS) An Attempt to Formalize Popper's Logic of Scientific Discovery (PAS) A Model Theory for R-calculus without Cut
Li, Yuefeng	(DL) Instance-driven TBox Revision in DL-Lite
Liang, Hongjin	(CSL-LICS) Compositional Verification of Termination-Preserving Refinement of Concurrent Programs
Liang, Tianyi	(CAV) A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
Liau, Churn-Jung	(LC) Fuzzy Bsimulation for Standard Godel Modal Logic
Libal, Tomer	(UITP) Advanced Proof Viewing in PROOFTOOL (ARQNL) Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Libby, Steven	(TermGraph) Needed Computations Shortcutting Needed Steps
Libkin, Leonid	(KR) Certain Answers as Objects and Knowledge (CSL-LICS) Pattern Logics and Auxiliary Relations
Licata, Daniel	(Coq) What is Homotopy Type Theory? (CSL-LICS) Eilenberg-MacLane Spaces in Homotopy Type Theory
Lieber, Jean	(KR) Belief Revision in the Propositional Closure of a Qualitative Algebra
Liebig, Thorsten	(IJCAR) Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures (DL) Abstraction Refinement for Ontology Materialization (DL) Optimised Absorption for Expressive Description Logics
Liefke, Kristina	(NLCS) Solving Partee's Temperature Puzzle in an EFL-Ontology
Liew, Dan	(CAV) Engineering a Static Verification Tool for GPU Kernels
Lifschitz, Vladimir	(KR) The Semantics of Gringo and Infinitary Propositional Formulas (ASPOCP) Infinitary Equilibrium Logic
Liiva, Kristjan	(PAS) A note on real quantifier elimination by virtual term substitution of unbounded degree
Lima, Leonardo	(IJCAR) Quati: An Automated Tool for Proving Permutation Lemmas
Lin, Fangzhen	(KR) A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations (KR) A Formalization of Programs in First-Order Logic with a Discrete Linear Order
Lin, Mengxiang	(PAS) A hybrid path constraint solver combined with meta-heuristic search
Lin, Shang-Wei	(CAV) Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions
Lin, Yuhui	(UITP) Tinker, tailor, solver, proof
Linard, Alban	(FWFM) Introducing Formal Verification with Lego
Lincoln, Patrick	(CAV) A Nonlinear Real Arithmetic Fragment
Lindauer, Marius	(ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming
Lindblad, Fredrik	(IJCAR) A Focused Sequent Calculus for Higher-Order Logic
Linsbichler, Thomas	(KR) Characteristics of Multiple Viewpoints in Abstract Argumentation (NMR) Compact Argumentation Frameworks
Lio', Pietro	(HSB) Bayesian Design for Whole Cell Synthetic Biology Models
Lisitsa, Alexei	(SAT) A SAT Attack on the Erdos Discrepancy Conjecture (VPT) A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal?
Liskov, Moses	(CSF) Modeling Diffie-Hellman Derivability for Automated Analysis
Litak, Tadeusz	(CLC) Negative Translations and Heyting Algebra Expansions
Liu, Jia	(CSF) Balancing Societal Security and Individual Privacy: Accountable Escrow System
Liu, Jiaxiang	(RTA-TLCA) Confluence by Critical Pair Analysis
Liu, Weiming	(KR) On Redundant Topological Constraints (Extended Abstract)
Liu, Yang	(CAV) Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions
Lochbihler, Andreas	(ITP) Recursive Functions on Codatatypes via Domains and Topologies (ITP) Truly Modular (Co)datatypes for Isabelle/HOL (Isabelle) Towards abstract and executable multivariate polynomials in Isabelle (Isabelle) Programming TLS in Isabelle/HOL
Loding, Christof	(CAV) ICE: A Robust Learning Framework for Synthesizing Invariants
Loewe, Benedikt	(LC) Restrictiveness relative to notions of interpretation
Logas, Heather	(FWFM) Chekofv: Crowd-sourced Formal Verification
Lomazova, Irina	(VPT) Branching Processes of Conservative Nested Petri Nets
Lombardi, Carlos	(RTA-TLCA) Proof terms for infinitary rewriting
Lomuscio, Alessio	(KR) Model Checking Unbounded Artifact-Centric Systems (KR) An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications (KR) Verification of Multi-Agent Systems against Epistemic Specifications (Part II) (KR) Verification of Multi-Agent Systems against Epistemic Specifications (Part I) (CAV) MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
Lonca, Emmanuel	(SAT) Detecting cardinality constraints in CNF
Long, Zhiguo	(KR) On Redundant Topological Constraints (Extended Abstract)
Lonlac, Jerry	(ParSearchOpt) A Portfolio Based Parallel SAT Solver with Multiple Deletion Strategies
Lonsing, Florian	(SAT) MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing (QBF) Conformant Planning as a Case Study of Incremental QBF Solving
Lopez-Garcia, Pedro	(ICLP) Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
Losemann, Katja	(CSL-LICS) MSO Queries on Trees: Enumerating Answers under Updates
Loseto, Giuseppe	(ORE) Mini-ME 2.0: powering the Semantic Web of Things
Loulergue, Frédéric	(ITP) A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
Lovotti, Irene	(KR4HC) META-GLARE: a meta-system for defining your own CIG system: Architecture and Acquisition
Lozes, Etienne	(LCC) Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
Lubarsky, Robert	(LC) Elementary epimorphisms between models of set theory
Lubinski, Cm	(CSF) Certificates for Verifiable Forensics
Lucanu, Dorel	(PAS) Programming Language Aggregation with Applications in Equivalence Checking
Luccio, Flaminia	(CSF) Mignis: A semantic based tool for firewall configuration
Lucio, Paqui	(QUANTIFY) Projective Quantifier Elimination for Equational Constraint Solving
Ludwig, Michel	(KR) Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference (DL) Brave and Cautious Reasoning in EL (DL) Detecting Conjunctive Query Differences between ELHr-Terminologies using Hypergraphs (DL) Evaluation of Extraction Techniques for Ontology Excerpts (ORE) Just: a Tool for Computing Justifications w.r.t. ELH Ontologies
Lukasiewicz, Thomas	(KR) Datalog+/–: Questions and Answers (KR) Stable Model Semantics for Guarded Existential Rules and Description Logics (PRUV) Computing k-Rank Answers with Ontological CP-Nets (PRUV) Answering Ontological Ranking Queries Based on Subjective Reports
Luo, Jie	(PAS) RCK: A Software Toolkit for R-calculus (PAS) A Model Theory for R-calculus without Cut
Luque, Amneris	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
Lutz, Carsten	(KR) Exact Learning of Lightweight Description Logic Ontologies (KR) Finite Model Reasoning in Horn Description Logics (DL) Query Rewriting under EL TBoxes: Efficient Algorithms
Lyaletski, Alexander	(ARQNL) Computer-oriented inference search in first-order sequent logics (ARW-DT) On Herbrand theorems for classical and non-classical logics
Lyde, Steven	(HOPA) Environment Unrolling (HOPA) Strong Function Call
Lynce, Ines	(SAT) Open-WBO: a Modular MaxSAT Solver
Lysyanskaya, Anna	(CSF) Malleable Signatures: New Definitions and Delegatable Anonymous Credentials
López Bóbeda, Edmundo	(FWFM) Introducing Formal Verification with Lego
Lücke, Philipp	(LC) Locally definable well-orders
Lüth, Christoph	(ITP) Collaborative Interactive Theorem Proving with Clide
M
Ma, Yue	(DL) Evaluation of Extraction Techniques for Ontology Excerpts (DL) Towards Parallel Repair: An Ontology Decomposition-based Approach
Mackie, Ian	(TermGraph) An Implementation Model for Interaction Nets (TermGraph) Numeral Systems in the Lambda Calculus (Linearity) Continuations, closed reduction and process networks (DCM) Some observations for the parallel implementation of interaction nets
Madarász, Judit X.	(LC) A completeness theorem for general relativity
Madelaine, Guillaume	(WPTE) Attractor Equivalence: An Observational Semantics for Reaction Networks
Madhavan, Ravichandhran	(CAV) Symbolic Resource Bound Inference for Functional Programs
Madhusudan, P.	(EC2) A new reduction for event-driven distributed programs (CAV) VAC - Verifier of Administrative Role-based Access Control Policies (CAV) ICE: A Robust Learning Framework for Synthesizing Invariants
Maffezioli, Paolo	(GSB) Sequent Systems for Classical Modal Logics
Maghsoodi, Aisan	(KR4HC) A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols
Magill, Stephen	(WST) Reducing Deadlock and Livelock Freedom to Termination
Mahajan, Yogesh	(SAT) Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
Mahboubi, Assia	(ITP) A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (CSL-LICS) Computer-checked mathematics: a formal proof of the Odd Order theorem
Mahdi, Ahmed	(iPRA) Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems
Mahmoud, Mohamed Yousri	(ITP) On the Formalization of Z-Transform in HOL (ITP) Formal Verification of Optical Quantum Flip Gate
Maieli, Roberto	(RTA-TLCA) Construction of retractile proof structures
Mailly, Jean-Guy	(KR) On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses
Maisonneuve, Vivien	(WING) ALICe: A Framework to Improve Affine Loop Invariant Computation
Majer, Ondrej	(LG) Semantic games for Łukasiewicz logic
Majumdar, Rupak	(CAV) Regression Test Selection for Distributed Software Histories (CAV) An SMT-Based Approach to Coverability Analysis (AISS) Unary Pushdown Automata and Straight-Line Programs
Makowsky, Johann	(PCCR) Connection matrices of finite rank instead of definability in Monadic Second Order Logic
Malbos, Philippe	(IWC) Confluence of linear rewriting and homology of algebras
Malecha, Gregory	(Coq) Automating Abstract Logics (ITP) Compositional Computational Reflection
Maler, Oded	(HSB) Concluding remarks: Dynamic Systems Biology
Malheiros, Yuri	(DL) A Method to Develop Description Logic Ontologies Iteratively with Automatic Requirement Traceability
Malicki, Maciej	(LC) Consequences of the existence of ample generics and automorphism groups of homogeneous metric structures
Malizia, Enrico	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
Malone, Brandon	(LaSh) Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability
Malozemoff, Alex	(CSF) Automated Analysis and Synthesis of Block-Cipher Modes of Operation
Mamino, Marcello	(CSL-LICS) On the Computing Power of +, −, and ×
Mamouras, Konstantinos	(CSL-LICS) KAT + B! (CSL-LICS) On the Hoare Theory of Monadic Recursion Schemes
Mancarella, Paolo	(LC) Argumentation Logic
Mancini, Luca	(RCRA) Self Regulating Mechanisms for Network Immunization
Manferdelli, John	(VSTTE) Formal Modeling and Verification of CloudProxy
Mann, Zoltan	(POS) Formula partitioning revisited (POS) Typical-case complexity and the SAT competitions
Manna, Marco	(KR) Polynomial Combined Rewritings for Existential Rules
Mannaa, Bassel	(CLC) A sheaf model of the algebraic closure
Manoharan, Praveen	(CSF) TUC: Time-sensitive and Modular Analysis of Anonymous Communication
Manolios, Panagiotis	(ACL2) Data Definitions in ACL2 Sedan
Manquinho, Vasco	(SAT) Open-WBO: a Modular MaxSAT Solver
Mansky, William	(LOLA) A Cross-Language Framework for Verifying Compiler Optimizations (WPTE) Verifying Optimizations for Concurrent Programs
Mantadelis, Theofrastos	(ICLP) Tabling, Rational Terms, and Coinduction Finally Together! (CICLOPS-WLPE) A Portable Prolog Predicate for Printing Rational Terms
Mantel, Heiko	(CSF) Noninterference under Weak Memory Models
Manthey, Norbert	(SAT) Detecting cardinality constraints in CNF (POS) Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers (POS) New CNF Features and Formula Classification (POS) Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers (ARW-DT) Extended Resolution in Modern SAT Solving
Maoz, Shahar	(RS) A Short Story on Scenarios
Mar, Gary	(LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
Maratea, Marco	(VSL) FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (ICLP) The Design of the Fifth Answer Set Programming Competition (NMR) The Multi-engine ASP Solver ME-ASP: Progress Report
Marcelino, Sérgio	(GeTFun) On the characterization of broadly truth-functional logics
Marché, Claude	(VSTTE) Formalizing Semantics with an Automatic Program Verifier
Marciuska, Sarunas	(DL) On Faceted Search over Knowledge Bases
Marcone, Alberto	(LC) Reverse mathematics of WQOs and Noetherian spaces
Marcos, João	(IJCAR) Clausal Resolution for Modal Logics of Confluence (GeTFun) Semi-BCI-algebras (GeTFun) On the characterization of broadly truth-functional logics (GeTFun) On non-deterministic fuzzy negations (GeTFun) A survey on Suszko’s Thesis and its formal developments (GeTFun) Broadly truth-functional logics through classical lenses
Marcos, Mar	(KR4HC) An Algorithm for Guideline Transformation: from BPMN to PROforma (KR4HC) Assessment of Clinical Guideline Models Based on Metrics for Business Process Models
Mardziel, Piotr	(FCS-FCC) Adversary Gain vs. Defender Loss in Quantified Information Flow
Marechal, Alexis	(FWFM) Introducing Formal Verification with Lego
Marengo, Elisa	(ICLP) Multi-criteria optimal planning for Energy policies in CLP
Margaria, Ines	(ITRS) On Isomorphism of "Functional'' Intersection and Union Types
Maric, Filip	(POS) Instance-based Selection of CSP Solvers using Short Training
Marin, Mircea	(DCM) Interactive Particle Systems and Random Walks on Hypergraphs
Marin, Paolo	(QBF) Incremental QBF Reasoning for the Verification of Partial Designs
Marin, Sonia	(GSB) Modular Systems for Intuitionistic Modal Logics in Nested Sequents
Marinov, Darko	(CAV) Regression Test Selection for Distributed Software Histories
Marion, Jean-Yves	(LOLA) Abstract Self Modifying Machines
Mariotti, Alessandro	(CAV) The nuXmv Symbolic Model Checker
Marple, Kyle	(ICLP) Dynamic Consistency Checking in Goal-Directed Answer Set Programming
Marques-Silva, Joao	(SAT) On Reducing Maximum Independent Set to Minimum Satisfiability (SAT) On Computing Preferred MUSes and MCSes (SAT) MUS Extraction using Clausal Proofs (ASPOCP) On the Implementation of Weak Constraints in WASP (RCRA) Maximal Falsifiability: Definitions, Algorithms, and Applications
Marquis, Pierre	(KR) On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses (KR) On Egalitarian Belief Merging
Marra, Vincenzo	(LATD) The space of directions of a polyhedron (LATD) Tutorial 2/2: The more, the less, and the much more: An introduction to Lukasiewicz logic as a logic of vague propositions, and to its applications (LATD) Tutorial 1/2: The more, the less, and the much more: An introduction to Lukasiewicz logic as a logic of vague propositions, and to its applications (LATD) Interpreting Lukasiewicz logic into Intuitionistic logic
Marrano, Rossella	(LATD) Ordinal foundation for Lukasiewicz semantics
Marrella, Andrea	(KR) SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical Planning
Marshall, Andrew M.	(UNIF) Hierarchical Combination of Matching Algorithms (Extended Abstract) (UNIF) On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
Martel, Matthieu	(NSV) Transformation of a PID Controller for Numerical Accuracy
Martens, Moritz	(ITRS) Delegation-based Mixin Composition Synthesis
Martens, Wim	(CSL-LICS) MSO Queries on Trees: Enumerating Answers under Updates
Marti, Johannes	(LG) Game Semantics for Conditional Logic
Martimiano, Taciane	(STAST) Modelling User Devices in Security Ceremonies
Martin-Recuerda, Francisco	(DL) Axiom Dependency Hypergraphs for Fast Modularisation and Atomic Decomposition
Martina, Jean Everson	(STAST) Modelling User Devices in Security Ceremonies
Martinez, Maria Vanina	(PRUV) Computing k-Rank Answers with Ontological CP-Nets (PRUV) Answering Ontological Ranking Queries Based on Subjective Reports
Martinez-Fernandez, Jose	(LC) Non-monotonic extensions of the weak Kleene clone with constants
Martins, Ruben	(SAT) Open-WBO: a Modular MaxSAT Solver
Marto, Marcus	(PRUV) Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics
Martínez-Salvador, Begoña	(KR4HC) An Algorithm for Guideline Transformation: from BPMN to PROforma (KR4HC) Assessment of Clinical Guideline Models Based on Metrics for Business Process Models
Marx, Dániel	(PCCR) CSPs and fixed-parameter tractability
Maršík, Jiří	(NLCS) Algebraic Effects and Handlers in Natural Language Interpretation
Masci, Paolo	(VeriSure) Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project
Massolo, Alba	(LC) Modelling Inference in Fiction
Matentzoglu, Nicolas	(VSL) FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Matentzoglu, Nicolas	(DL) An Empirical Investigation of Difficulty of Subsets of Description Logic Ontologies (ORE) A Family History Knowledge Base in OWL 2
Matichuk, Daniel	(ITP) An Isabelle Proof Method Language
Matthes, Ralph	(CLC) Confluence for classical logic through the distinction between values and computations
Maurer, Ueli	(FCS-FCC) Constructive Cryptography and Security Proofs
Maurice, Bruynooghe	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories (CSPSAT) BreakIDGlucose: on the importance of row symmetry (LaSh) Lazy Model Expansion: Interleaving Grounding with Search (LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development
Mauro, Jacopo	(ICLP) SUNNY: a Lazy Portfolio Approach for Constraint Solving
May, Eva	(WING) Loop Invariants by Mutation, Dynamic Validation, and Static Checking
Mayer, Jonathan	(CSF) Surveillance and Privacy
Mayo, Jackson R.	(NSV) Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics
Mayr, Richard	(CSL-LICS) Infinite-State Energy Games
Mazowiecki, Filip	(CSL-LICS) Decidability of Weak Logics with Deterministic Transitive Closure
Mazza, Damiano	(2FC) Computational complexity in the lambda-calculus: what's new? (LCC) Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus (HOR) On Infinitary Affine Lambda-Calculi
McCleeary, Ryan	(CLC) Dualized Type Theory
McClurg, Jedidiah	(ACL2) Development of a Translator from LLVM to ACL2
McIlraith, Sheila	(KR) Situation Calculus: The Last 15 Years (KR) Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals
McInerney, Michael	(LC) Integer-valued randomness and degrees
McIver, Annabelle	(CSF) Additive and multiplicative notions of leakage, and their capacities
McKenney, Paul	(REORDER) Reordering and Verification in the Linux Kernel
McMillan, Kenneth	(CAV) Lazy Annotation Revisited (IJCAR) Structured Search and Learning (iPRA) Interpolation Strategies
McNeill, Daniel	(LATD) The space of directions of a polyhedron (LATD) Interpreting Lukasiewicz logic into Intuitionistic logic
Meadows, Catherine	(UNIF) On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
Mecella, Massimo	(KR) SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical Planning
Meert, Wannes	(KR) Skolemization for Weighted First-Order Model Counting (PLP) TBA (PLP) Lifted Inference for Probabilistic Logic Programs
Mehnert, Hannes	(DTP) Tool Demonstration: An IDE for Programming and Proving in Idris
Mehta, Deepak	(ParSearchOpt) A Constraint-based Parallel Local Search for Disjoint Rooted Distance-Constrained Minimum Spanning Tree Problem
Mehto, Shweta	(UNIF) Unification Modulo Common List Functions
Meiklejohn, Sarah	(CSF) Malleable Signatures: New Definitions and Delegatable Anonymous Credentials
Meilicke, Christian	(PRUV) Multi-Attribute Decision Making using Weighted Description Logics
Meir, Nadav	(LC) On various strengthenings of the notion of indivisibility
Mejía, Diego A.	(LC) Matrix iterations and Cichoń's diagram
Melikhov, Sergey	(PSC) A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic
Melliès, Paul-André	(2FC) A cubical representation of local states (LOLA) Tensorial logic with algebraic effects (ITRS) Indexed linear logic and higher-order model checking (HOPA) The modal nature of colors in higher-order model-checking (RTA-TLCA) Local stores in string diagrams
Melquiond, Guillaume	(SMT) Automating the verification of floating-point algorithms
Mena, Eduardo	(ORE) Android Went Semantic: Time for Evaluation
Menezes de Morais, Eduardo	(PLP) Approximated Probabilistic Answer Set Programming
Mengel, Stefan	(SAT) Hypergraph Acyclicity and Propositional Model Counting
Mennicke, Roy	(AISS) Model Checking Communicating Finite-State Machines using Local Temporal Logics
Mens, Kim	(ICLP) Customisable Handling of Java References in Prolog Programs
Mereacre, Alexandru	(CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells
Mereuta, Radu	(RTA-TLCA) All-Path Reachability Logic
Merkle, Daniel	(EC2) Group Communication Patterns for High Performance Computing in Scala (FRIDA) Correctness and Performance Analysis of Distributed High Performance Programs in Scala
Mermelstein, Omer	(LC) Reducts of simple (non-collapsed) Fraisse-Hrushovski constructions
Merz, Stephan	(ARQNL) Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Meseguer, Jose	(RTA-TLCA) Predicate Abstraction of Rewrite Theories
Meseguer, Jose	(UNIF) Extensible Symbolic System Analysis
Mesnard, Frederic	(VSL) FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014) (WST) Non-termination of Dalvik bytecode via compilation to CLP
Metcalfe, George	(NCPROOFS) Admissibility and Exact Unification (GSB) Welcome (UNIF) From Admissibility to a New Hierarchy of Unification Types (LATD) First-Order Logics and Truth Degrees
Meumann, Thomas	(VERIFY) Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Meunier, Noémie	(CSL-LICS) Secure Equilibria in Weighted Games
Meyer, Philipp	(CAV) An SMT-Based Approach to Coverability Analysis
Meyer, Roland	(REORDER) Robustness against Power is PSpace-complete
Meyer, Thomas	(DL) Transition Constraints for Temporal Attributes (DL) Complexity of Temporal Query Abduction in DL-Lite (DL) DIP: A Defeasible-Inference Platform for OWL Ontologies
Meyer Zu Hörste, Michael	(VeriSure) Introducing Semi-Formal Specifications into a Distributed Development Process
Miao, Daniela	(KR4HC) Real Rules, Real Data -- Addressing Challenges of Reasoning HIPAA Privacy Rule in Health Information Exchange (HIE)
Michael, Loizos	(KR) Simultaneous Learning and Prediction (KR) A Psychology-Inspired Approach to Automated Narrative Text Comprehension (NMR) Non-Monotonic Reasoning and Story Comprehension
Michaliszyn, Jakub	(KR) Model Checking Unbounded Artifact-Centric Systems (KR) An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications
Michalowski, Martin	(KR4HC) Using First-Order Logic to Represent Clinical Practice Guidelines and to Mitigate Adverse Interactions
Michalowski, Wojtek	(KR4HC) Using First-Order Logic to Represent Clinical Practice Guidelines and to Mitigate Adverse Interactions
Micheli, Andrea	(CAV) The nuXmv Symbolic Model Checker
Miculan, Marino	(RTA-TLCA) A Model of Countable Nondeterminism in Guarded Type Theory
Middeldorp, Aart	(IWC) Normalization Equivalence of Rewrite Systems (ITP) A New and Formalized Proof of Abstract Completion (WST) Automating Elementary Interpretations (IFIP-WG16) Discussion on the International School on Rewriting (ISR) (IFIP-WG16) Basic Normalization (RTA-TLCA) Conditional Confluence (System Description)
Mierla, Laurentiu	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Might, Matthew	(HOPA) Environment Unrolling (HOPA) Strong Function Call
Mikirtumov, Ivan	(GeTFun) The procedural understanding of meaning and compositionality in formal semantics
Miksa, Mladen	(SAT) Long Proofs of (Seemingly) Simple Formulas (PC) From Small Space to Small Width in Resolution (PC) Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
Milani, Alfedo	(RCRA) A Discrete Differential Evolution Algorithm for the Total Flowtime Flowshop Scheduling Problem
Milani, Alfredo	(RCRA) Self Regulating Mechanisms for Network Immunization
Milano, Michela	(ICLP) Multi-criteria optimal planning for Energy policies in CLP
Milazzo, Paolo	(VEMDP) Identification of Components and Modular Verification of Biochemical Pathways
Mileo, Alessandra	(NMR) Probabilistic Inductive Logic Programming based on Answer Set Programming
Miller, Benjamin	(LC) Definable cardinals just beyond R / Q
Miller, Christian	(QBF) Incremental QBF Reasoning for the Verification of Partial Designs
Miller, Dale	(APPA) Foundational Proof Certificates (LATD) Combining Intuitionistic and Classical Logic: a proof system and semantics
Miller, Rob	(KR) A Psychology-Inspired Approach to Automated Narrative Text Comprehension (NMR) Non-Monotonic Reasoning and Story Comprehension
Miller, Russell	(LC) Coding graphs into fields (INFINITY) Functors in Computable Model Theory
Miller, Sheila	(LC) Budding Trees
Millet, Laure	(FRIDA) On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering
Millstein, Todd	(CAV) Automatic Atomicity Verification for Clients of Concurrent Data Structures
Mimram, Samuel	(TermGraph) An Introduction to Higher-Dimensional Rewriting Theory
Minarro-Giménez, José Antonio	(ORE) An update on Genomic CDS, a complex ontology for pharmacogenomics and clinical decision support
Miné, Antoine	(WST) To Infinity... and Beyond!
Mio, Matteo	(LATD) Coupling games for Lukasiewicz logic
Miquel, Alexandre	(CLC) TBC (LC) Tutorial on Classical Realizability and Forcing 3 (LC) Tutorial on classical realizability and forcing 1 (LC) Tutorial on Classical Realizability and Forcing 2
Mirek, Ryszard	(LC) Natural Deduction in Renaissance Geometry
Mishchenko, Alan	(VEMDP) Boolean modelling and formal verification of tiered-rate chemical reaction networks
Misra, Neeldhara	(PCCR) Backdoors into Heterogeneous Classes of SAT and CSP
Mitchell, David	(PRUV) Resolution and Clause Learning for Multi-Valued CNF Formulas (LaSh) Depart for Workshop Lunch
Mitra, Sayan	(CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells
Mnatsakanyan, Armen	(LC) On proof complexities of strong equal modal tautologies. (LC) The relation between the graphs structures and proof complexity of corresponding Tseitin graph tautologies
Mogavero, Fabio	(CAV) MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
Mohammadi, Esfandiar	(CSF) TUC: Time-sensitive and Modular Analysis of Anonymous Communication
Molick, Sanderson	(GeTFun) A survey on Suszko’s Thesis and its formal developments
Molinaro, Cristian	(PRUV) Answering Ontological Ranking Queries Based on Subjective Reports
Molnar, Attila	(LC) Modal logic of clocks: Modalizing a first-order theory of time to get a better understanding of relativity theories
Mombourquette, Brent	(KR) Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals
Monmege, Benjamin	(CSL-LICS) Logical Characterization of Weighted Pebble Walking Automata
Monniaux, David	(CAV) How do we get inductive invariants? (Part A) (CAV) How do we get inductive invariants? (Part B)
Montagna, Franco	(LATD) Poof Search and Co-NP completeness for Many-Valued Logics
Montalban, Antonio	(INFINITY) Classes of structures with no intermediate isomorphism problems
Montali, Marco	(KR) State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems
Montani, Stefania	(KR4HC) Knowledge-Intensive Medical Process Similarity
Moodley, Kody	(DL) DIP: A Defeasible-Inference Platform for OWL Ontologies
Moore, Brandon	(RTA-TLCA) All-Path Reachability Logic
Moore, J	(ITP) Rough Diamond: An Extension of Equivalence-based Rewriting (ITP) Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (ACL2) Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
Moore, Scott	(CSF) Declarative Policies for Capability Control
Morak, Michael	(DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs (ICLP) The Impact of Disjunction on Reasoning under Existential Rules
Morales, Jose F.	(ICLP) Towards Assertion-based Debugging of Higher-Order (C)LP Programs (CICLOPS-WLPE) Towards Pre-Indexed Terms
Moraschini, Tommaso	(LATD) Definability of truth predicates in abstract algebraic logic (LATD) On logics of varieties and logics of semilattices
Morawska, Barbara	(UNIF) Matching with respect to general concept inclusions in the Description Logic EL (DL) Matching with respect to general concept inclusions in the Description Logic EL
Morgado, Antonio	(SAT) On Reducing Maximum Independent Set to Minimum Satisfiability (RCRA) Maximal Falsifiability: Definitions, Algorithms, and Applications
Morgan, Carroll	(CSF) Additive and multiplicative notions of leakage, and their capacities
Morgenstern, Leora	(KR) Representing and Reasoning About Time Travel Narratives: Foundational Concepts
Morozov, Alexei A.	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
Morozov, Andrey	(LC) On the existential interpretability of structures
Morrisett, Greg	(Linearity) Type Classes for Lightweight Substructural Types
Morton, Wilmari	(LC) Canonical extensions and prime filter completions of poset expansions.
Moser, Georg	(LCC) Weighted Automata Theory for Complexity Analysis of Rewrite Systems (IFIP-WG16) Discussion on the Future of RTA (+ TLCA) (IFIP-WG16) Basic Normalization (WPTE) A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems (RTA-TLCA) Automated Complexity Analysis Based on Context-Sensitive Rewriting (RTA-TLCA) Amortised Resource Analysis and Typed Polynomial Interpretations
Moshier, M. Andrew	(LATD) Bitopological Duality and Three-valued Logic
Moss, Lawrence S.	(KR) Dynamic Epistemic Logic and Its Interaction with Knowledge Representation (Part II) (KR) Dynamic Epistemic Logic and Its Interaction with Knowledge Representation (Part I)
Mossakowski, Till	(ARQNL) Proof Support for Common Logic
Mostowski, Wojciech	(VSTTE) The KeY Platform for Verification and Analysis of Java Programs
Mota, Miguel Angel	(LC) Forcing with finite conditions and preserving CH
Motik, Boris	(DL) Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems
Moura, Joao	(NMR) Generalising Modular Logic Programs
Moura, Paulo	(ICLP) Customisable Handling of Java References in Prolog Programs (ICLP) Tabling, Rational Terms, and Coinduction Finally Together!
Mover, Sergio	(CAV) The nuXmv Symbolic Model Checker (CAV) Verifying LTL properties of hybrid systems with K-liveness
Mruczek-Nasieniewska, Krystyna	(LATD) Semantial and syntactial charaterisation of some extensions of the class of MV-algebras
Mu, Chunyan	(CSL-LICS) Asymptotic behaviour in temporal logic
Mueller, Moritz	(CSL-LICS) One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries (INFINITY) Set functions with small circuits (INFINITY) Cobham Recursive Set Functions
Mueller-Theys, Joachim	(LC) Metalogical Extensions--Part II: First-order Consequences and Gödel
Mugnier, Marie-Laure	(NMR) Revisiting Chase Termination for Existential Rules and their Extension to Nonmonotonic Negation
Muller, Jean-Michel	(NSV) Getting tight error bounds in floating-point arithmetic: illustration with complex functions, and the real x^n function
Munch-Maccagnoni, Guillaume	(CSL-LICS) Formulae-as-Types for an Involutive Negation
Munera, Danny	(ParSearchOpt) Towards a Parallel Hierarchical Adaptive Solver Tool
Murali, Vijayaraghavan	(VSTTE) What Gives? A Hybrid Algorithm for Error Explanation
Murano, Aniello	(CAV) MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
Muravitsky, Alexei	(LATD) Semantic information and fuzziness
Murawska, Agata	(LFMTP) Hybrid Extensions in a Logical Framework
Muroya, Koko	(LOLA) Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (CSL-LICS) Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects
Murray, John	(VeriSure) Quantification of Verification Progress (FWFM) Chekofv: Crowd-sourced Formal Verification
Murray, Toby	(ITP) An Isabelle Proof Method Language
Musliu, Nysret	(LaSh) Modeling High School Timetabling as PartialWeighted maxSAT
Muñoz, Pablo	(CSL-LICS) Graph Logics with Rational Relations: The Role of Word Combinatorics
Myllymäki, Petri	(RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
Myreen, Magnus O.	(ITP) HOL with Definitions: Semantics, Soundness, and a Verified Implementation (ITP) The reflective Milawa theorem prover is sound (down to the machine code that runs it) (ACL2) Machine-code verification: experience of tackling medium-sized case studies using 'decompilation into logic’ (HOL) Modernising HOL's documentation (HOL) Writing proof automation for HOL4 (QED) Towards Formally Verified Theorem Provers - Part I
Méndez, José M.	(LC) Blocking the routes to triviality with depth relevance
Mödersheim, Sebastian A.	(CSF) A Sound Abstraction of the Parsing Problem
Möller, Ralf	(DL) A Stream-Temporal Query Language for Ontology Based Data Access
Möller, Sebastian	(STAST) Using Statistical Information to Communicate Android Permission Risks to Users
Mörtberg, Anders	(ITP) A Coq Formalization of Finitely Presented Modules
Møgelberg, Rasmus Ejlers	(CSL-LICS) A type theory for productive coprogramming via guarded recursion
Møller, Anders	(HOPA) Program Analysis for JavaScript Web Applications
N
Nachmanson, Lev	(CAV) Monadic Decomposition
Nadathur, Gopalan	(LFMTP) A Framework for the Verified Transformation of Functional Programs (CICLOPS-WLPE) A Lambda Prolog Based Animation of Twelf Specifications
Nadel, Alexander	(CAV) Bit-Vector Rewriting with Automatic Rule Generation (SAT) Ultimately Incremental SAT
Nagai, Tomoharu	(RTA-TLCA) Reduction System for Extensional Lambda-mu Calculus
Nagashima, Masanori	(WPTE) Inverse Unfold Problem and Its Heuristic Solving
Nagele, Julian	(IWC) Certification of Confluence Proofs using CeTA (VSTTE) Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
Najvirt, Robert	(FRIDA) Towards binary circuit models that faithfully reflect physical (un)solvability
Nakazawa, Koji	(CLC) Extensional Models of Typed Lambda-mu Calculus (CLC) Confluence for classical logic through the distinction between values and computations (RTA-TLCA) Reduction System for Extensional Lambda-mu Calculus
Nalbandyan, Hakob	(LC) On proof complexities of strong equal modal tautologies.
Nalon, Cláudia	(IJCAR) Clausal Resolution for Modal Logics of Confluence (ARW-DT) A Resolution-Based Prover for Normal Modal Logics
Namjoshi, Kedar	(VeriSure) Witnessing an SSA Transformation
Nampally, Arun	(ICLP) Adaptive MCMC-Based Inference in Probabilistic Logic Programs
Narayan, Arjun	(CSF) Differential Privacy: An Economic Method for Choosing Epsilon
Narayan Kumar, K.	(CSL-LICS) Infinite-State Energy Games
Narboni, G.	(ICLP) Numerical Properties of Min-closed CSPs
Narendran, Paliath	(UNIF) Hierarchical Combination of Matching Algorithms (Extended Abstract) (UNIF) Unification Modulo Common List Functions (UNIF) On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
Narodytska, Nina	(CAV) Solving Games without Controllable Predecessor (SAT) Cores in Core based MaxSat Algorithms: an Analysis (iPRA) Practical CNF Interpolants Via BDDs (iPRA) Interpolants in Two-Player Games
Nassar, Muhammad	(PAAR) Automated Theorem Proving using the TPTP Process Instruction Language
Natarajan, Sriraam	(KR) Relational Logistic Regression
Naumann, David	(VSTTE) A logical analysis of framing for specifications with pure method calls (CSF) Information flow monitoring as abstract interpretation for relational logic
Navarro Perez, Juan	(CSL-LICS) A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates
Naves, Guyslain	(ITP) Balancing lists: a proof pearl
Nehmeier, Marco	(NSV) SetBased Decorated Intervals
Neider, Daniel	(CAV) ICE: A Robust Learning Framework for Synthesizing Invariants
Nemouchi, Yakoub	(Isabelle) Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
Nemytykh, Andrei	(VPT) A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal? (VPT) On Unfolding for Programs Using Strings as a Data Type
Nenov, Yavor	(DL) Pay-as-you-go Ontology Query Answering Using a Datalog Reasoner (DL) Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems (DL) Datalog Rewriting Techniques for Non-Horn Ontologies
Nepeivoda, Antonina	(VPT) Verification of Multi-Party Ping-Pong Protocols via Program Transformation
Nepejvoda, Nikolay	(FWFM) Algebraic description of restricted programming and elements of its logics
Neron, Pierre	(NSV) Certifying Square Root and Division Elimination
Nesbeth, Darren	(VEMDP) An Aspect Oriented Design and Modelling Framework for Synthetic Biology
Nestmann, Uwe	(FRIDA) Mechanical Verification of a Constructive Proof for FLP
Neuenstadt, Christian	(DL) A Stream-Temporal Query Language for Ontology Based Data Access
Neumann, René	(VSTTE) Using Promela in a Fully Verified Executable LTL Model Checker (SHORT)
Newsham, Zack	(SAT) Impact of Community Structure on SAT Solver Performance
Newton, Ryan	(DTP) Type-Directed Editing for Dependently-Typed Programs.
Ngo, Nhung	(iPRA) Interpolation and Domain Independence applied to Databases
Nguyen, Duc	(ICLP) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments (NMR) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments: Progress Report
Nguyen, Truc L.	(CAV) VAC - Verifier of Administrative Role-based Access Control Policies
Nguyen, Truong Khanh	(CAV) Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions
Nickles, Matthias	(NMR) Probabilistic Inductive Logic Programming based on Answer Set Programming
Nicolosi-Asmundo, Marianna	(ADDCT) On dual tableau-based decision procedures for relational fragments
Niehren, Joachim	(WPTE) Attractor Equivalence: An Observational Semantics for Reaction Networks
Nielebock, Sebastian	(VeriSure) A Graphical Notation for Probabilistic Specifications
Nielson, Flemming	(CSF) Automated Generation of Attack Trees
Nielson, Hanne Riis	(CSF) Automated Generation of Attack Trees
Nigam, Vivek	(ICLP) A Proof Theoretic Study of Soft Concurrent Constraint Programming (IJCAR) Quati: An Automated Tool for Proving Permutation Lemmas (FCS-FCC) Towards Timed Models for Cyber-Physical Security Protocols
Nigam, Vivek	(GeTFun) On subexponentials, focusing and modalities in concurrent systems
Niksic, Filip	(CAV) An SMT-Based Approach to Coverability Analysis
Nimal, Vincent	(CAV) Don't sit on the fence: A static analysis approach to automatic fence insertion
Nimkar, Kaustubh	(CAV) Proving Non-termination Using Max-SMT
Nipkow, Tobias	(ITP) Unified Decision Procedures for Regular Expression Equivalence (Isabelle) Isabelle tutorial for beginners (part 2) (Isabelle) Amortized Complexity Verified (Isabelle) Isabelle tutorial for beginners (part 1)
Nishida, Naoki	(IWC) On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation (WST) On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants (WPTE) On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings (WPTE) Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems (WPTE) Inverse Unfold Problem and Its Heuristic Solving
Nizamani, Abdul Rahim	(DL) Understandable Explanations in Description Logic
Nogatz, Falco	(CHR) From XML Schema to JSON Schema: Translation with CHR
Nogina, Elena	(LC) On Explicit-Implicit Reflection Principles.
Noguera, Carles	(LATD) Advances on elementary equivalence in model theory of fuzzy logics
Nordström, Jakob	(SAT) Long Proofs of (Seemingly) Simple Formulas (SAT) A (Biased) Proof Complexity Survey for SAT Practitioners (PC) From Small Space to Small Width in Resolution (PC) Narrow Proofs May Be Maximally Long (PC) Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds (PC) Size-Space Bounds and Trade-offs for CDCL Proofs (PC) A (Biased) Survey of Space Complexity and Time-Space Trade-offs in Proof Complexity
Norman, Timothy	(DL) Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information
Norrish, Michael	(PAAR) Beagle as a HOL4 external ATP method
Noschinski, Lars	(Isabelle) Pattern-based Subterm Selection In Isabelle (Isabelle) Towards Structured Proofs for Program Verification (Ongoing Work)
Nourani, Cyrus F	(LC) More On Completion with Horn Filters
Novikova, Tatyana	(UNIF) Two-sided unification is NP-complete
Novotný, Petr	(CAV) Minimizing Running Costs in Consumption Systems (CSL-LICS) Zero-Reachability in Probabilistic Multi-Counter Automata
Nowak, Thomas	(FRIDA) Towards binary circuit models that faithfully reflect physical (un)solvability
Nowé, Ann	(KR) Using Answer Set Programming for Solving Boolean Games
Nurse, Jason	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Németi, István	(LC) Weak Beth definability property for finite variable fragments.
O
O'Leary, John	(ACL2) Modeling Algorithms in SystemC and ACL2
O'Sullivan, Barry	(ParSearchOpt) A Constraint-based Parallel Local Search for Disjoint Rooted Distance-Constrained Minimum Spanning Tree Problem
Occhipinti, Annalisa	(HSB) Bayesian Design for Whole Cell Synthetic Biology Models
Ochremiak, Joanna	(CSL-LICS) Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity
Ogata, Kazuhiro	(WST) Specifying and verifying liveness properties of QLOCK in CafeOBJ
Ogawa, Mizuhito	(IWC) Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract) (SMT) raSAT: SMT for Polynomial Inequality
Oh, Chanseok	(iPRA) Fault Localization using Interpolation
Oitavem, Isabel	(LCC) Towards recursion schemata for the probablistic class PP
Okada, Mitsuhiro	(FCS-FCC) Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model
Oladimeji, Patrick	(VeriSure) Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project
Olarte, Carlos	(GeTFun) On subexponentials, focusing and modalities in concurrent systems
Olarte, Carlos	(ICLP) A Proof Theoretic Study of Soft Concurrent Constraint Programming
Olembo, Maina	(STAST) Modelling User Devices in Security Ceremonies
Olesen, Kerry	(IJCAR) Implementing Tableaux Calculi Using BDDs: BDDTab System Description
Oliva, Paulo	(GSB) On Affine Logic and Łukasiewicz Logic (PSC) Effective Bounds on the Podelski-Rybalchenko Termination Theorem (LATD) On Pocrims and Hoops
Oliveras, Albert	(CAV) Proving Non-termination Using Max-SMT (SAT) Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
Olivetti, Nicola	(NCPROOFS) Conditional logics: the quest for internal proof systems (IJCAR) NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics (DL) Rational closure in SHIQ
Olteanu, Dan	(DL) Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems
Oms, Sergi	(LC) Towards a Conditional for The Liar and the Sorites.
Ong, Luke	(KR) ∃GUARANTEENASH for Boolean Games Is NEXP-Hard (ITRS) Intersection Types, Game Semantics and Higher-Order Model Checking (CSL-LICS) Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees
Ongoma, E. A. Nasubo	(DL) Transition Constraints for Temporal Attributes
Ono, Hiroakira	(LC) Predicate Glivenko theorems and substructural aspects of negative translations
Ordyniak, Sebastian	(PCCR) Backdoors to Planning (PCCR) Backdoors into Heterogeneous Classes of SAT and CSP
Oren, Nir	(DL) Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information
Ortiz, Magdalena	(KR) Nested Regular Path Queries in Description Logics (DL) Planning Problems for Graph Structured Data in Description Logics
Ortmeier, Frank	(VeriSure) A Graphical Notation for Probabilistic Specifications
Ospichev, Sergey	(LC) Computable numberings in Ershov hierarchy
Otten, Jens	(IJCAR) MleanCoP: A Connection Prover for First-Order Modal Logic (ARQNL) ARQNL Workshop - Opening (ARQNL) Problem Libraries for Non-Classical Logics
Otto, Carsten	(IJCAR) Proving Termination of Programs Automatically with AProVE
Ouaknine, Joel	(VSL) FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (AISS) Decision Problems for Linear Recurrence Sequences
Ovchinnikova, Ekaterina	(KR) Natural Language Understanding with World Knowledge and Inference (Part II) (KR) Natural Language Understanding with World Knowledge and Inference (Part I)
Oveisi, Mehrdad	(KR) Belief Change and Base Dependence
Owens, Scott	(ITP) HOL with Definitions: Semantics, Soundness, and a Verified Implementation
Oyamaguchi, Michio	(IWC) Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract) (IWC) Confluence and Critical-Pair-Closing Systems
Ozaki Rivera Castillo, Ana	(KR) Exact Learning of Lightweight Description Logic Ontologies
P
Padovani, Luca	(CSL-LICS) Deadlock and lock freedom in the linear pi-calculus
Pagani, Michele	(WIR) Work in Progress: Algebraic Abstract Reduction Systems (DCM) Quantitative semantics for higher-order probabilistic and quantum computation
Pagnucco, Maurice	(KR) Forgetting in Action
Pakhomov, Fedor	(LC) Ordinal Notations and Fundamental Sequences in Caucal Hierarchy
Palacín, Daniel	(LC) The Fitting subgroup of a supersimple group
Palamidessi, Catuscia	(CSF) Additive and multiplicative notions of leakage, and their capacities
Palikareva, Hristina	(SMT) Multi-solver Support in Symbolic Execution
Palmigiano, Alessandra	(GSB) Display-type calculi and their cut elimination metatheorem
Palsberg, Jens	(CAV) Automatic Atomicity Verification for Clients of Concurrent Data Structures
Panangaden, Prakash	(LC) The place of logic in computer science education
Panny, Lorenz	(ITP) Truly Modular (Co)datatypes for Isabelle/HOL (Isabelle) Primitively (Co)recursive Definitions for Isabelle/HOL
Paoletti, Nicola	(CAV) Analyzing and Synthesizing Genomic Logic Functions
Paoletti, Nicola	(VEMDP) Guiding the development of DNA walker systems to guarantee reliability and performance
Papacchini, Fabio	(IJCAR) Terminating Minimal Model Generation Procedures for Propositional Modal Logics (ARW-DT) Models Minimal Modulo Subset-Simulation for Expressive Propositional Modal Logics
Papadimitriou, Christos	(VSL) VSL Keynote Talk: Computational Ideas and the Theory of Evolution
Papini, Odile	(NMR) Belief merging within fragments of propositional logic
Papp, Pal	(POS) Formula partitioning revisited
Paraskevopoulou, Zoe	(Coq) QuickChick: Property-Based Testing for Coq
Pardini, Giovanni	(VEMDP) Identification of Components and Modular Verification of Biochemical Pathways
Parent, Xavier	(KR) Aggregative Deontic Detachment for Normative Reasoning
Parikh, Rohit	(NLCS) Grice, Hoare and Nash: some comments on conversational implicature (LC) Elections and knowledge
Park, Jennifer	(LC) Coding graphs into fields
Parkinson, Matthew	(WST) Reducing Deadlock and Livelock Freedom to Termination
Parlato, Gennaro	(CAV) VAC - Verifier of Administrative Role-based Access Control Policies (CAV) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
Parsia, Bijan	(VSL) FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (DL) Temporalising EL Concepts with Time Intervals (DL) An Empirical Investigation of Difficulty of Subsets of Description Logic Ontologies (DL) Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure?
Parvizi, Artemis	(DL) Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information
Parys, Paweł	(CSL-LICS) Two-Way Cost Automata and Cost Logics over Infinite Trees
Paskevich, Andrei	(CAV) The Spirit of Ghost Code (VSTTE) Formalizing Semantics with an Automatic Program Verifier
Pass, Rafael	(KR) Axiomatizing Rationality
Passmore, Grant	(PAS) A note on real quantifier elimination by virtual term substitution of unbounded degree
Pathak, Shashank	(RCRA) Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies
Patoglu, Volkan	(RCRA) A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks
Patrick, Saint Dizier	(NLCS) Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts
Patrizi, Fabio	(KR) Action Theories over Generalized Databases with Equality Constraints (Extended Abstract)
Pattinson, Dirk	(IJCAR) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
Paulin-Mohring, Christine	(APPA) Calculus of Inductive Constructions
Paulson, Lawrence	(Isabelle) Proving Gödel’s Incompleteness Theorems
Pauly, Arno	(CLC) Relative Computability and Uniform Continuity of Non-Extensional (aka Multivalued) 'Functions' (CSL-LICS) Infinite sequential games with real-valued payoffs
Pavlinovic, Zvonimir	(ADDCT) Finding Minimum Type Error Sources
Payet, Étienne	(WST) Non-termination of Dalvik bytecode via compilation to CLP
Paykin, Jennifer	(Linearity) A Linear/Producer/Consumer model of Classical Linear Logic
Pearce, Adrian	(KR) Transforming Situation Calculus Action Theories for Optimised Reasoning
Pearce, David	(ASPOCP) Infinitary Equilibrium Logic
Pearson, Justin	(SMT) Protocol log analysis with constraint programming
Pease, Adam	(IJCAR) Knowledge Engineering for Large Ontologies with Sigma KEE 3.0
Pedrini, Andrea	(LATD) The space of directions of a polyhedron (LATD) Interpreting Lukasiewicz logic into Intuitionistic logic
Pelletier, Francis Jeffry	(KR) Belief Change and Base Dependence
Pellissier, Luc	(TermGraph) Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion
Peltier, Nicolas	(IJCAR) A Rewriting Strategy to Generate Prime Implicates in Equational Logic (ADDCT) A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic (PAAR) A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
Peltonen, Jaakko	(RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
Peppas, Pavlos	(KR) Belief Change and Semiorders
Perdrix, Simon	(DCM) Quantum Circuits for the Unitary Permutation Problem
Pereira, Fernando	(WST) Real-world loops are easy to predict : a case study
Pereira, Luiz Carlos	(LC) An intuitive semantics for {Full Intuitionistic Linear Logic}
Pereira, Luís Moniz	(ICLP) Properties of Stable Model Semantics Extensions (ICLP) Joint Tabling of Logic Program Abductions and Updates (ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect
Pereira, Mário	(ITRS) Liquid Intersection Types
Perez, Guillermo	(SYNT) AbsSynthe: abstract synthesis from succinct safety specifications
Perlmutter, Norman Lewis	(LC) Elementary epimorphisms between models of set theory
Perner, Matthias	(CSF) Noninterference under Weak Memory Models
Perrinel, Matthieu	(CLC) Stratified Nested Linear Logic (CSL-LICS) On Context Semantics for Interaction Nets
Perrussel, Laurent	(KR) A Dynamic Logic Framework for Abstract Argumentation
Peschanenko, Vladimir	(PAS) New predicate transformer for symbolic modeling
Peters, Kirstin	(FRIDA) Mechanical Verification of a Constructive Proof for FLP
Petrank, Erez	(EC2) Wait-Freedom Made Practical
Petric Maretic, Grgur	(CSL-LICS) Anchored LTL Separation
Petrisan, Daniela	(CSL-LICS) Coinduction Up-To in a Fibrational Setting
Petrolo, Mattia	(LC) Natural deduction for intuitionistic differential linear logic
Pettorossi, Alberto	(VPT) Program Verification using Constraint Handling Rules and Array Constraint Generalizations
Peñaloza, Rafael	(KR) Decidable Gödel Description Logics without the Finitely-Valued Model Property (KR) Answering Instance Queries Relaxed by Concept Similarity (IJCAR) The Bayesian Description Logic BEL (DL) Brave and Cautious Reasoning in EL (DL) Bayesian Description Logics (DL) Mary, What's Like All Cats? (DL) DeaLing with Ontologies using CODs (DL) Certain Answers in a Rough World (DL) Gödel Description Logics with General Models (DL) Towards Parallel Repair: An Ontology Decomposition-based Approach (DL) Gödel FL_0 with Greatest Fixed-Point Semantics (PRUV) Many-valued Horn Logic is Hard
Pfandler, Andreas	(QBF) Conformant Planning as a Case Study of Incremental QBF Solving (PCCR) Backdoors to Planning (PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets
Pfenning, Frank	(ICLP) A Linear Logic Programming Language for Concurrent Programming over Graph Structures
Philipp, Tobias	(POS) Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers (POS) Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers
Phillips, Andrew	(VEMDP) Computational design of DNA strand displacement systems
Piazza, Carla	(HSB) Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models
Pich, Ján	(LC) Circuit lower bounds in bounded arithmetics (PC) Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic
Pichardie, David	(ITP) Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
Pichler, Reinhard	(DL) Expressive Identification Constraints to Capture Functional Dependencies in Description Logics (PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets
Pientka, Brigitte	(LFMTP) Welcome Remarks (RTA-TLCA) Unnesting of Copatterns
Pierce, Benjamin C.	(Coq) QuickChick: Property-Based Testing for Coq (CSF) Differential Privacy: An Economic Method for Choosing Epsilon
Pieris, Andreas	(KR) Datalog+/–: Questions and Answers (KR) Polynomial Combined Rewritings for Existential Rules (DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs
Piessens, Frank	(CSF) Stateful Declassification Policies for Event-Driven Programs (CSF) Towards a Zero-Software Trusted Computing Base for Extensible Systems
Piette, Cédric	(POS) Dolius: A Distributed Parallel SAT Solving Framework
Pimentel, Elaine	(ICLP) A Proof Theoretic Study of Soft Concurrent Constraint Programming (GeTFun) On subexponentials, focusing and modalities in concurrent systems (Linearity) Modalities and Linearity
Pinosio, Riccardo	(LG) Game Semantics for Conditional Logic
Pinto, Alexandre	(CSF) Attribute-based Encryption for Access Control Using Elementary Operations
Pinto, Luís	(CLC) Confluence for classical logic through the distinction between values and computations
Piro, Robert	(DL) Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems
Pirró, Giuseppe	(KR) Knowledge Maps of Web Graphs
Piskac, Ruzica	(CAV) Automating Separation Logic with Trees and Data
Pistone, Paolo	(LC) Type equations and second order logic
Pitcher, Corin	(CSF) Certificates for Verifiable Forensics
Piterman, Nir	(CAV) Finding instability in biological models (WST) Fairness for Infinite-State Systems
Pizani Flor, João Paulo	(DTP) An Embedded Hardware Description Language using Dependent Types
Place, Thomas	(CSL-LICS) Separating Regular Languages with First-Order Logic
Plaisted, David	(UNIF) Constraint Manipulation in SGGS (IFIP-WG16) Semantically-Guided Goal-Sensitive Theorem Proving (PAAR) SGGS Theorem Proving: an Exposition
Planes, Jordi