GLOBAL AUTHOR INDEX

All Volumes All Papers Global Author Index Global Keyword Index

Shortcuts: A B C D E F G H I J K L M N O P Q R S T U V W X Y Z Á Ö Č

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