Program for Thursday, July 17th, 2014: Talk View

VSL 2014: VIENNA SUMMER OF LOGIC 2014

VSL PROGRAM INDEXES

VSL | FLoC | CAV | CSF | CSL-LICS | ICLP | IJCAR | ITP | RTA-TLCA | SAT | LC | LATD | KR | DL | NMR | 2FC | ACL2 | ADDCT | AISS | APPA | ARQNL | ARW-DT | ASA | ASPOCP | Automatheo | CHR | CICLOPS-WLPE | CLC | Coq | CSPSAT | DCM | DTP | EC2 | FCS-FCC | FRIDA | FWFM | GeTFun | GSB | HCVS | HOL | HOPA | HOR | HSB | IFIP-WG16 | INFINITY | iPRA | ITRS | IWC | Isabelle | KInAR | KR4HC | LaSh | LCC | LFMTP | LG | Linearity | LOLA | LSB | NCPROOFS | NLCS | NLSR | NSV | ORE | PAAR | ParSearchOpt | PAS | PC | PCCR | PLP | POS | PRUV | PSC | QBF | QED | QUANTIFY | RCRA | REORDER | RS | SMT | SD | SSV | STAST | SYNT | TermGraph | UITP | UNIF | Vampire | VEMDP | VERIFY | VeriSure | VPT | VSTTE | WING | WIR | WPTE | WST | WWV

PROGRAM FOR THURSDAY, JULY 17TH, 2014: TALK VIEW

Days:

View: with abstracts session overview

9:00

9:30

10:00

10:30

11:00

11:30

12:00

12:30

13:00

13:30

14:00

14:30

15:00

15:30

16:00

16:30

17:00

17:30

18:00

18:30

19:00

19:30

20:00

20:30

21:00

21:30

22:00

22:30

23:00

23:30

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-10:15

FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change?

Nina Amla, Georg Gottlob, Falk Reckling, Sweitze Roffel, Andrei Voronkov

08:45-09:15

Non-termination of Dalvik bytecode via compilation to CLP

Étienne Payet, Fred Mesnard

09:15-09:45

Geometric Series as Nontermination Arguments for Linear Lasso Programs

Jan Leike, Matthias Heizmann

09:45-10:15

Non-termination using Regular Languages

Joerg Endrullis, Hans Zantema

08:45-09:45

Proofs for Optimality of Sorting Networks by Logic Programming

Michael Codish, Luís Cruz-Filipe, Michael Frank, Peter Schneider-Kamp

09:45-10:15

Everyone

08:45-09:15

Undecidability of consequence relation in Full Non-associative Lambek Calculus

Karel Chvalovský

09:15-09:45

Canonical formulas for k-potent residuated lattices

Luca Spada, Nick Bezhanishvili, Nick Galatos

09:45-10:15

On satisfiability of terms in FLew-algebras

Zuzana Hanikova, Petr Savicky

08:45-09:15

Five-valued LTL for Runtime Verification

Ming Chai

09:15-09:45

A method for generalizing finite automata arising from Stone-like dualities

Stefano Aguzzoli, Denisa Diaconescu, Tommaso Flaminio

09:45-10:15

An application of distance-based approximate reasoning for diagnostic questionnaires in healthcare

Thomas Vetterlein, Anna Zamansky

08:45-09:45

Atomicity Refinement for Verified Compilation

Suresh Jagannathan

09:45-10:15

Concolic Testing of Concurrent Programs

Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith

08:45-08:55

Nicos Angelopoulos

08:55-09:50

First-order representations for integer programming

James Cussens

09:50-10:15

PageRank, ProPPR and Stochastic Logic Programs

Dries Van Daele, Angelika Kimmig, Luc De Raedt

08:45-09:00

Opening remarks

Marta Kwiatkowska

09:00-09:50

Computational design of DNA strand displacement systems

Andrew Phillips

09:50-10:15

A domain-level DNA strand displacement reaction enumerator allowing arbitrary non-pseudoknotted secondary

Casey Grun, Karthik Sarma, Brian Wolfe, Seung Woo Shin, Erik Winfree

08:45-09:15

Nonmonotonic Reasoning as a Temporal Activity

Daniel Schwartz

09:15-09:45

Probabilistic Inductive Logic Programming based on Answer Set Programming

Matthias Nickles, Alessandra Mileo

09:45-10:15

A Plausibility Semantics for Abstract Argumentation Frameworks

Emil Weydert

08:45-08:50

Summer School Opening

Gopal Gupta

08:50-10:15

Constraint Logic Programming I

Roman Bartak

08:50-09:00

Welcome Remarks

Brigitte Pientka

09:00-09:25

Proof-Theoretic Foundations of Indexing in Logic Programming

Iliano Cervesato

09:25-09:50

Hybrid Extensions in a Logical Framework

Taus Brock-Nannestad, Nicolas Guenot, Agata Murawska, Carsten Schürmann

09:50-10:15

Variable Arity for LF

John Boyland, Tian Zhao

09:00-10:00

Invited talk: Proof and Refutations for Horn-clause Encodings of Reachability Problems

Daniel Kröning

09:00-10:15

Digging deeper: mole looking for potential weak memory related bugs in Debian

Michael Tautschnig

09:00-10:00

Hierarchical reasoning and quantifier elimination for the verification of parametric reactive and hybrid

Viorica Sofronie-Stokkermans

09:00-10:00

Laure Vieu

09:00-09:15

Philipp Rümmer

09:15-10:15

SMT: Where do we go from here?

Clark Barrett

09:15-10:05

Getting tight error bounds in floating-point arithmetic: illustration with complex functions, and the real x^n

Jean-Michel Muller

09:15-10:15

Definable cardinals just beyond R / Q

Benjamin Miller

09:15-10:15

The TPTP Process Instruction Language, with Applications

Geoff Sutcliffe

09:15-10:15

Excluded Middle Considered as a Mathematical Problem (Invited Talk)

Martin Escardo

10:45-11:15

Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems

Jerome Leroux, M. Praveen, Grégoire Sutre

11:15-11:45

Preservation and Decomposition Theorems for Bounded Degree Structures

Frederik Harwath, Lucas Heimberg, Nicole Schweikardt

11:45-12:15

On the Succinctness of Query Rewriting over OWL 2 QL Ontologies with Bounded Chase

Stanislav Kikot, Roman Kontchakov, Vladimir Podolskii, Michael Zakharyaschev

12:15-12:45

MSO Queries on Trees: Enumerating Answers under Updates

Katja Losemann, Wim Martens

10:45-11:15

Transition systems over games

Paul Blain Levy, Sam Staton

11:15-11:45

Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects

Naohiko Hoshino, Koko Muroya, Ichiro Hasuo

11:45-12:15

Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees

Takeshi Tsukada, Luke Ong

12:15-12:45

On the Hoare Theory of Monadic Recursion Schemes

Konstantinos Mamouras

10:45-11:15

Formalized, effective domain theory in Coq

Robert Dockins

11:15-11:45

Completeness and Decidability Results for CTL in Coq

Christian Doczkal, Gert Smolka

11:45-12:15

Universe Polymorphism in Coq

Matthieu Sozeau, Nicolas Tabareau

12:15-12:45

Compositional Computational Reflection

Gregory Malecha, Adam Chlipala, Thomas Braibant

12:45-13:00

Formal C semantics: CompCert and the C standard

Robbert Krebbers, Xavier Leroy, Freek Wiedijk

10:45-11:15

Tree Automata with Height Constraints between Brothers

Carles Creus, Guillem Godoy

11:15-11:45

Reduction System for Extensional Lambda-mu Calculus

Koji Nakazawa, Tomoharu Nagai

11:45-12:15

Proof terms for infinitary rewriting

Carlos Lombardi, Alejandro Rios, Roel de Vrijer

12:15-12:45

Near semi-rings and lambda calculus

Richard Statman

10:45-13:00

Constraint Logic Programming II

Roman Bartak

10:45-11:15

Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions

Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell, Albert Rubio

10:45-11:15

Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics

Geoffrey C. Hulette, Robert C. Armstrong, Jackson R. Mayo, Joseph R. Ruthruff

11:15-11:45

Transformation of a PID Controller for Numerical Accuracy

Alexandre Chapoutot, Nasrine Damouche, Matthieu Martel

11:45-12:15

Policy iteration in finite templates domain

Assale Adje

10:45-11:15

Tinker, tailor, solver, proof

Gudmund Grov, Aleks Kissinger, Yuhui Lin

11:15-11:45

How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem

Sarah Grebing, Bernhard Beckert, Florian Böhl

11:45-12:15

Advanced Proof Viewing in PROOFTOOL

Tomer Libal, Martin Riener, Mikheil Rukhaia

12:15-12:45

The Certification Problem Format

Christian Sternagel, René Thiemann

10:45-11:45

Termination of Biological Programs

Jasmin Fisher

11:45-12:15

On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop

Naoki Nishida, Takumi Kataoka

12:15-12:45

Automatic Termination Analysis for GPU Kernels

Jeroen Ketema, Alastair Donaldson

12:45-13:00

Everyone

10:45-11:35

Session Types Meet Separation Logic

Jesper Bengtson

10:45-11:15

Refining definitions with unknown opens using XSB for IDP3

Joachim Jansen, Gerda Janssens

11:15-11:45

A Lambda Prolog Based Animation of Twelf Specifications

Gopalan Nadathur, Mary Southern

11:45-12:15

A System for Embedding Global Constraints into SAT

Md Solimul Chowdhury, Jia-Huai You

12:15-12:45

Towards Pre-Indexed Terms

Jose F. Morales, Manuel V. Hermenegildo

12:45-13:00

Everyone

10:45-13:00

Please consult the program at http://vsl2014.at/hcvs

T.B.A

10:45-11:45

Reordering and Verification in the Linux Kernel

Paul McKenney

11:45-12:15

Reasoning about the C/C++ Weak Memory Model

Viktor Vafeiadis

10:45-11:45

Reordering and Verification in the Linux Kernel

Paul McKenney

11:45-12:15

Reasoning about the C/C++ Weak Memory Model

Viktor Vafeiadis

10:45-11:30

An Attempt to Formalize Popper's Logic of Scientific Discovery

Wei Li

11:30-12:00

A Model Theory for R-calculus without Cut

Jie Luo, Wei Li

12:00-12:30

RCK: A Software Toolkit for R-calculus

Xiaoyu Chen, Jie Luo

10:45-11:45

Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems

Orna Grumberg

11:45-12:10

A Model for Capturing and Replaying Proof Strategies

Leo Freitas, Cliff B. Jones, Andrius Velykis, Iain Whiteside

12:10-12:35

A Verification Condition Visualizer

Madiha Jami, Andrew Ireland

12:35-13:00

What Gives? A Hybrid Algorithm for Error Explanation

Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, Satish Chandra

10:45-11:45

Invited Talk: New Perspectives on Query Reformulation

Michael Benedikt

11:45-12:10

Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs

Pierre Bourhis, Michael Morak, Andreas Pieris

12:10-12:35

Complexities of Nominal Schemas

Markus Krötzsch, Sebastian Rudolph

12:35-12:38

Comparing the Expressiveness of Description Logics

Ali Rezaei Divroodi

12:38-12:41

An Empirical Investigation of Difficulty of Subsets of Description Logic Ontologies

Nicolas Matentzoglu, Bijan Parsia, Uli Sattler

12:41-12:44

Predicting OWL Reasoners: Locally or Globally?

Viachaslau Sazonau, Uli Sattler, Gavin Brown

12:44-12:47

Bridging the Gap between Tableau and Consequence-Based Reasoning

Yevgeny Kazakov, Pavel Klinov

12:47-12:50

Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability

Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger

12:50-12:53

How to Best Nest Regular Path Queries

Pierre Bourhis, Markus Krötzsch, Sebastian Rudolph

12:53-12:56

Typed Higher-Order Variant of SROIQ - Why Not?

Martin Homola, Jan Kluka, Vojtěch Svátek, Miroslav Vacura

12:56-12:59

Practical query answering over Hi (DL-LiteR) knowledge bases

Maurizio Lenzerini, Lorenzo Lepore, Antonella Poggi

10:45-11:15

How to do things with types

Robin Cooper

11:15-11:45

Mereological Comparatives in Delineation Semantics

Heather Burnett

11:45-12:15

Proof-Theoretic Semantics for intensional transitive verbs

Nissim Francez

12:15-12:45

Grice, Hoare and Nash: some comments on conversational implicature

Rohit Parikh

10:45-11:45

Combining Intuitionistic and Classical Logic: a proof system and semantics

Dale Miller

11:45-12:45

Tutorial 2/2: The more, the less, and the much more: An introduction to Lukasiewicz logic as a logic of vague propositions, and to its

Vincenzo Marra

10:45-11:15

Speeding Up SMT-Based Quantitative Program Analysis

Daniel J. Fremont, Sanjit A. Seshia

11:15-11:45

Multi-solver Support in Symbolic Execution

Hristina Palikareva, Cristian Cadar

11:45-12:15

Protocol log analysis with constraint programming

Mats Carlsson, Olga Grinchtein, Justin Pearson

12:15-12:45

Reasoning About Set Comprehensions

Edmund Soon Lee Lam, Iliano Cervesato

10:45-11:30

Constructive completeness and exploding models

Christian Espindola, Henrik Forssell

11:30-12:15

Computing with Gödel’s completeness theorem

Hugo Herbelin, Danko Ilik

10:45-12:00

SAT-Based Model Checking with Interpolation

Orna Grumberg

12:00-12:30

Interpolants in Two-Player Games

Niklas Een, Alexander Legg, Nina Narodytska, Leonid Ryzhyk

12:30-13:00

Fault Localization using Interpolation

Chanseok Oh, Martin Schäf, Daniel Schwartz-Narbonne, Thomas Wies

10:45-11:00 Opening

10:45-11:15

Prefix and infix probability computation in PRISM

Ryosuke Kojima, Taisuke Sato

11:15-11:45

Compiling Probabilistic Logic Programs into Sentential Decision Diagrams

Jonas Vlasselaer, Joris Renkens, Guy Van den Broeck, Luc De Raedt

11:45-12:15

cProbLog: Restricting the Possible Worlds of Probabilistic Logic Programs

Dimitar Shterionov, Gerda Janssens

12:15-12:45

Approximated Probabilistic Answer Set Programming

Eduardo Menezes de Morais

10:45-11:40

Molecular computers for molecular robots as hybrid systems

Masami Hagiya

11:40-12:10

DNA-based circuits in well-mixed and spatially organized systems

Lulu Qian

12:10-12:35

Verifying Polymer Reaction Networks using Bisimulation

Robert F. Johnson, Erik Winfree

12:35-13:00

Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench

Konur, Ladroue, Fellermann, Sanassy, Mierla, Ipate, Kalvala, Gheorghe, Krasnogor

10:45-11:30

Verification of Multi-Party Ping-Pong Protocols via Program Transformation

Antonina Nepeivoda

11:30-12:15

Program Verification using Constraint Handling Rules and Array Constraint Generalizations

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

12:15-13:00

A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal?

Alexei Lisitsa, Andrei Nemytykh

10:45-11:15

An Approach to Forgetting in Disjunctive Logic Programs that Preserves Strong Equivalence

James P. Delgrande, Kewen Wang

11:15-11:45

Three Semantics for Modular Systems

Shahab Tasharrofi, Eugenia Ternovska

11:45-12:15

Generalising Modular Logic Programs

Joao Moura, Carlos Viegas Damásio

10:50-11:20

Optimal Neighborhood Preserving Visualization by Maximum Satisfiability

K. Bunte, M. Järvisalo, J. Berg, P. Myllymäki, J. Peltonen, S. Kaski

11:20-11:50

Maximal Falsifiability: Definitions, Algorithms, and Applications

Alexey Ignatiev, Antonio Morgado, Jordi Planes, Joao Marques-Silva

11:50-12:10

Latin Squares with Graph Properties

Hans Zantema

11:00-12:00

Tutorial on classical realizability and forcing 1

Alexandre Miquel

12:00-13:00

Cardinal invariants and template iterations

Vera Fischer

11:00-12:00

Fixed-Parameter Algorithms for Reasoning Problems in NP and Beyond

Stefan Szeider

11:15-11:45

An Ising Model inspired Extension of the Product-based MP Framework for SAT

Oliver Gableske

11:45-12:15

Approximating highly satisfiable random 2-SAT

Andrei Bulatov, Cong Wang

12:15-12:45

Hypergraph Acyclicity and Propositional Model Counting

Florent Capelli, Arnaud Durand, Stefan Mengel

11:45-12:10

Internal Adequacy of Bookkeeping in Coq

Alberto Ciaffaglione, Ivan Scagnetto

12:10-12:35

A Generic Approach to Proofs about Substitution

Abhishek Anand, Vincent Rahli

12:35-13:00

A Framework for Implementing Logical Frameworks

Florian Rabe

12:00-12:30

A Parameterized Complexity Analysis of Generalized CP-Nets

Martin Kronegger, Martin Lackner, Andreas Pfandler, Reinhard Pichler

12:30-13:00

Backdoors to Planning

Martin Kronegger, Sebastian Ordyniak, Andreas Pfandler

12:10-12:40

Efficient Computation of the Well-Founded Semantics over Big Data

Ilias Tachmazidis, Grigoris Antoniou, Wolfgang Faber

12:40-13:00

Declarative Specification of Benchmark Sessions via ASP

Mario Alviano, Bernardo Cuteri, Francesco Ricca

12:15-12:37

The Multi-engine ASP Solver ME-ASP: Progress Report

Marco Maratea, Luca Pulina, Francesco Ricca

12:37-12:59

Preliminary Report on WASP 2

Mario Alviano, Carmine Dodaro, Francesco Ricca

14:00-14:30

Reasoning about Fences in C11 Weak Memory Model

Marko Doko

14:30-15:00

Robustness against Power is PSpace-complete

Roland Meyer

15:00-15:30

Simulating, exploring and formalising the OpenCL 2.0 memory model

John Wickerson

15:30-16:00

Testing GPU Memory Models

Daniel Poetzl

14:30-15:00

Decidability of Weak Logics with Deterministic Transitive Closure

Witold Charatonik, Emanuel Kieronski, Filip Mazowiecki

15:00-15:30

The Complexity of Admissibility in Omega-Regular Games

Romain Brenguier, Jean-Francois Raskin, Mathieu Sassolas

15:30-16:00

Pattern Logics and Auxiliary Relations

Diego Figueira, Leonid Libkin

14:30-15:00

Niels Bjørn Bugge Grathwohl, Dexter Kozen, Konstantinos Mamouras

15:00-15:30

On the characterization of models of H*

Flavien Breuvart

15:30-16:00

Functional Reactive Types

Alan Jeffrey

14:30-15:00

A New and Formalized Proof of Abstract Completion

Nao Hirokawa, Aart Middeldorp, Christian Sternagel

15:00-15:30

Hypermap Specification and Certified Linked Implementation using Orbits

Jean-François Dufourd

15:30-16:00

Implicational Rewriting Tactics in HOL

Vincent Aravantinos, Sofiene Tahar

14:30-16:00 RTA/TLCA business meeting

14:30-16:00

Horn Clauses and Verification I

Andrey Rybalchenko

14:30-16:00 Report on Competitions

14:30-15:00

Certifying Square Root and Division Elimination

Pierre Neron

15:00-15:30

Computational complexity of iterated maps on points and sets

Christoph Spandl

15:30-16:00

SetBased Decorated Intervals

Jürgen Wolff von Gudenberg, Marco Nehmeier

14:30-15:30

Asynchronous Processing of Formal Documents in Coq

Enrico Tassi

14:30-15:00

To Infinity... and Beyond!

Caterina Urban, Antoine Miné

15:00-15:30

Real-world loops are easy to predict : a case study

Raphael Rodrigues, Péricles Alves, Fernando Pereira, Laure Gonnord

15:30-16:00

Type Introduction for Runtime Complexity Analysis

Martin Avanzini, Bertram Felgenhauer

14:30-15:20

A Framework for the Verified Transformation of Functional Programs

Gopalan Nadathur

14:30-15:00

Extending the Finite Domain Solver of GNU Prolog

Vincent Bloemen, Daniel Diaz, Machiel van der Bijl, Salvador Abreu

15:00-15:30

SWI-Prolog version 7 extensions

Jan Wielemaker

15:30-16:00

A Portable Prolog Predicate for Printing Rational Terms

Theofrastos Mantadelis, Ricardo Rocha

14:30-15:30

Invited talk: Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods

Michael Leuschel

14:30-15:30

Invited talk: Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods

Michael Leuschel

14:30-15:00

The Theorema Approach to Mathematics

Bruno Buchberger

15:00-15:30

A note on real quantifier elimination by virtual term substitution of unbounded degree

Kristjan Liiva, Grant Passmore, Paul Jackson

14:30-14:55

Efficient Refinement Checking in VCC

Sumesh Divakaran, Deepak D'Souza, Nigamanth Sridhar

14:55-15:20

Formalizing Semantics with an Automatic Program Verifier

Martin Clochard, Jean-Christophe Filliatre, Claude Marché, Andrei Paskevich

15:20-15:45

The KeY Platform for Verification and Analysis of Java Programs

Ahrendt et.al

15:45-16:00

Using Promela in a Fully Verified Executable LTL Model Checker (SHORT)

René Neumann

14:30-14:55

Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs

D. Carral, C. Feier, A. Armas Romero, B. Cuenca-Grau, P. Hitzler, I. Horrocks

14:55-15:20

Abstraction Refinement for Ontology Materialization

Birte Glimm, Yevgeny Kazakov, Thorsten Liebig, Trung-Kien Tran, Vincent Vialard

15:20-15:45

Shape and Content: Incorporating Domain Knowledge into Shape Analysis

Diego Calvanese, Tomer Kotek, Mantas Simkus, Helmut Veith, Florian Zuleger

15:45-15:48

An ABox Revision Algorithm for the Description Logic EL_\bot

Liang Chang, Uli Sattler, Tianlong Gu

15:48-15:51

Instance-driven TBox Revision in DL-Lite

Zhe Wang, Kewen Wang, Guilin Qi, Zhiqiang Zhuang, Yuefeng Li

15:51-15:54

Rational Elimination of DL-Lite TBox Axioms

Zhiqiang Zhuang, Zhe Wang, Kewen Wang, Grigoris Antoniou

15:54-15:57

Rational closure in SHIQ

Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato

15:57-16:00

DIP: A Defeasible-Inference Platform for OWL Ontologies

Kody Moodley, Thomas Meyer, Uli Sattler

14:30-15:30

Anne Abeille

15:30-16:00

Computing Italian clitic and relative clauses with tupled pregroups

Claudia Casadio, Aleksandra Kislak-Malinowska

14:30-15:00

Embeddings into BiFL-algebras and conservativity

Nikolaos Galatos, Agata Ciabattoni, Revantha Ramanayake

15:00-15:30

The lattice of varieties generated by small residuated lattices

Peter Jipsen

15:30-16:00

Quasivarieties of MV-algebras and structurally complete Lukasiewicz logics

Joan Gispert

14:30-15:00

Boolean-valued judgment aggregation

Daniel Eckert, Frederik Herzberg

15:00-15:30

Constructing many-valued logical functions with small influence of their variables

Tomáš Kroupa, Tomáš Valla

15:30-16:00

Coupling games for Lukasiewicz logic

Matteo Mio, Alex Simpson

14:30-15:30

Abstractions for Relaxed Memory Models

Eran Yahav

15:30-16:00

Group Communication Patterns for High Performance Computing in Scala

Felix Hargreaves, Daniel Merkle, Peter Schneider-Kamp

14:30-15:00

Weakly Equivalent Arrays

Juergen Christ, Jochen Hoenicke

15:00-15:30

Decision Procedures for Flat Array Properties

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

15:30-16:00

Extending SMT-LIB v2 with lambda-terms and polymorphism

Richard Bonichon, David Déharbe, Cláudia Tavares

14:30-15:15

A typed lambda-calculus with call-by-name and call-by-value iteration

Herman Geuvers

15:15-16:00

Effective Bounds on the Podelski-Rybalchenko Termination Theorem

Stefano Berardi, Paulo Oliva, Silvia Steila

14:30-15:45

Feasible Interpolation in Proof Systems based on Integer Linear Programming

Pavel Pudlak

15:45-16:00

Laura Kovacs, Georg Weissenbacher

14:30-15:00

Intuitionistic modal logics: efficient fragments and parameterized complexity

R. Ramanujam, S P Suresh

14:30-15:00

Exploring probabilistic grammars of symbolic music using PRISM

Samer Abdallah, Nicolas Gold

15:00-15:30

An OpenCL implementation of a forward sampling algorithm for CP-logic

Wiebe Van Ranst, Joost Vennekens

15:30-16:00

Lifted Inference for Probabilistic Logic Programs

Wannes Meert, Guy Van den Broeck, Adnan Darwiche

14:30-15:20

Morphisms of reaction networks that couple structure to function

Luca Cardelli

15:20-15:45

Verifying CRN Implementations: A Pathway Decomposition Approach

Seung Woo Shin, Chris Thachuk, Erik Winfree

15:45-16:00

Lightning talks for posters/demos

Chris Thachuk

14:30-15:00

A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility

Esra Erdem, Volkan Patoglu, Peter Schüller

15:00-15:30

A Discrete Differential Evolution Algorithm for the Total Flowtime Flowshop Scheduling Problem

Valentino Santucci, Marco Baioletti, Alfedo Milani

14:30-15:30

Four Floors for the Theory of Theory Change

Hans Rott

15:00-16:00

Generalizations of Hilbert's Tenth Problem

Kirsten Eisentraeger

15:00-16:00 Open problems

15:20-15:45

Automatically Deriving Schematic Theorems for Dynamic Contexts

Olivier Savary Bélanger, Kaustuv Chaudhuri

15:30-16:00

PIDE for Asynchronous Interaction with Coq

Carst Tankink

15:30-16:00

On Strong and Default Negation in Logic Program Updates

Martin Slota, Martin Baláž, Joao Leite

15:30-16:00

Please consult the program at http://vsl2014.at/hcvs

T.B.A

16:00-16:50 Poster Session (with coffee break)

16:30-17:20

Verifying Parameterized Software Models in Computational Data Science against Behavioral

Sumit Kumar Jha

16:30-17:00

System description: Isabelle/jEdit in 2014

Makarius Wenzel

17:00-17:30

A Logic-Independent IDE

Florian Rabe

17:30-18:00

UTP2: Higher-Order Equational Reasoning by Pointing

Andrew Butterfield

16:30-17:00

Ordering Networks

Lars Hellström

17:00-17:30

Everyone

16:30-17:20

Idris: Implementing a Dependently Typed Programming Language

Edwin Brady

16:30-18:00

Please consult the program at http://vsl2014.at/hcvs

T.B.A

16:30-18:00

Panel Session

16:30-17:00

Successfully Coping with Scalability of Symbolic Analysis in Timing Analysis

Jens Knoop, Laura Kovacs, Jakob Zwirchmayr

17:00-17:30

Confluence of Pattern-Based Calculi with Finitary Matching

Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia

17:30-18:00

The Verification of Conversion Algorithms between Finite Automata

Dongchen Jiang

18:00-18:30

Source code profiling and classification for automated detection of logical errors

George Stergiopoulos, Panagiotis Katsaros, Dimitris Gritzalis

16:30-17:00

Algebraic Effects and Handlers in Natural Language Interpretation

Jiří Maršík, Maxime Amblard

17:00-17:30

Solving Partee's Temperature Puzzle in an EFL-Ontology

Kristina Liefke

17:30-18:00

Toward a Logic of Cumulative Quantification

Makoto Kanazawa, Junri Shimada

16:30-17:00

Densification via polynomial extensions

Nikolaos Galatos, Rostislav Horcik

17:00-17:30

Introducing an exotic MTL-chain

Felix Bou

17:30-18:00

On Pocrims and Hoops

Rob Arthan, Paulo Oliva

16:30-17:00

Ordinal foundation for Lukasiewicz semantics

Rossella Marrano

17:00-17:30

Advances on elementary equivalence in model theory of fuzzy logics

Pilar Dellunde, Àngel García-Cerdaña, Carles Noguera

17:30-18:00

Trakhtenbrot theorem and first-order axiomatic extensions of MTL

Matteo Bianchi

16:30-17:30

Verifiable Concurrent Systems Programming: A Garbage Collector Case Study

Serdar Tasiran

16:30-17:15

Observational Equivalence for Behavioural Differential Equations

Henning Basold, Helle Hvid Hansen

17:15-18:00

Multi-agent justification logic

Tatiana Yavorskaya, Nadezhda Ruhlyadko

16:30-18:00 Discussions on demand

16:30-17:00

On Enumerating Query Plans via Interpolants from Tableau Proofs (abstract)

David Toman, Grant Weddell

17:00-17:30

Application Patterns of Projection/Forgetting

Christoph Wernhard

17:30-18:00

Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems

Ahmed Mahdi, Martin Fränzle

16:30-17:00

A unified approach to generative and discriminative modeling

Taisuke Sato

17:00-17:30

Inference and learning for PLP

Fabrizio Riguzzi

17:30-18:00

C.R. Ramakrishnan

18:00-18:30

Wannes Meert

18:30-19:00

Discussion on the implementation of PLP systems.

P.L.P. Chairs

16:30-17:00

A unified approach to generative and discriminative modeling

Taisuke Sato

17:00-17:30

Inference and learning for PLP

Fabrizio Riguzzi

17:30-18:00

C.R. Ramakrishnan

18:00-18:30

Wannes Meert

18:30-19:00

Discussion on the implementation of PLP systems.

P.L.P. Chairs

16:30-16:55

Boolean modelling and formal verification of tiered-rate chemical reaction networks

Karthik, Soloveichik, Ray, Sterin, Mishchenko, Brayton, Roychowdhury

16:55-17:20

Formal mean field theories for graph rewriting

Vincent Danos

17:20-17:45

Rule based modelling of DNA repair

Jean Krivine

16:30-17:00

Inference in the FO(C) Modelling Language

Bart Bogaerts, Joost Vennekens, Marc Denecker, Jan Van den Bussche

17:00-17:30

FO(C) and Related Modelling Paradigms

Bart Bogaerts, Joost Vennekens, Marc Denecker, Jan Van den Bussche

17:30-18:00

Belief merging within fragments of propositional logic

Nadia Creignou, Odile Papini, Stefan Rümmele, Stefan Woltran

18:00-18:30

Belief Revision and Trust

Aaron Hunter

16:30-18:30

Horn Clauses and Verification II

Andrey Rybalchenko

16:50-17:15

Goal-Directed Tracing of Inferences in EL Ontologies

Yevgeny Kazakov, Pavel Klinov

17:15-17:40

Brave and Cautious Reasoning in EL

Michel Ludwig, Rafael Peñaloza

17:40-18:05

Matching with respect to general concept inclusions in the Description Logic EL

Franz Baader, Barbara Morawska

18:05-18:30

Contextualized Knowledge Repositories with Justifiable Exceptions

Loris Bozzato, Thomas Eiter, Luciano Serafini

17:20-17:45

Some constructions on ω-groupoids

Thorsten Altenkirch, Nuo Li, Ondrej Rypacek

17:45-18:10

Gentle Formalisation of Stoughton’s Lambda Calculus Substitution

Alvaro Tasistro, Ernesto Copello, Nora Szasz

17:45

DyNAMiC Workbench: Automated design and verification of dynamic DNA nanosystems

Casey Grun

17:45

An Aspect Oriented Design and Modelling Framework for Synthetic Biology

Philip Boeing, Darren Nesbeth, Anthony Finkelstein, Chris P Barnes

17:45

Guiding the development of DNA walker systems to guarantee reliability and performance

Frits Dannenberg, Milan Ceska, Nicola Paoletti, Marta Kwiatkowska

17:45

Software tools for analysing the chemical master equation

Neil Dalchau

17:45

Identification of Components and Modular Verification of Biochemical Pathways

Paolo Milazzo, Giovanni Pardini

19:00-20:00 LICS Business Meeting

19:00-21:00 DL/NMR Welcome Reception

19:30-21:00 ITP Steering and Program Committee Dinner

10:15-10:45 Coffee Break

13:00-14:30 Lunch Break

16:00-16:30 Coffee Break

16:30-17:30

Foundations and Technology Competitions Award Ceremony

Kurt Gödel Research Prize Fellowships Program

17:30-18:15

FLoC Olympic Games Award Ceremony 1

Floc Olympic Games

18:15-18:30

FLoC Closing Week 1

Helmut Veith

21:00-23:59 VSL Student Reception 1

Disclaimer | Powered by EasyChair Smart Program