VSL 2014: VIENNA SUMMER OF LOGIC 2014

PROGRAM FOR THURSDAY, JULY 17TH: TALK VIEW

Days:
previous day
next day
all days

View: with abstractssession overview

CSL-LICS
CAV
SAT
SMT
PSC
VSTTE
ITP
NMR
LC
PLP
VSL
EC2
REORDER
NLCS
RCRA
FLoC
CICLOPS-WLPE
DL
CSF
RTA-TLCA
iPRA
UITP
HCVS
WST
ICLP
LATD
IJCAR
VPT
VEMDP
LFMTP
NSV
PAS
PCCR
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
Discussion
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
Welcome
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
TBA
Laure Vieu
09:00-09:15
Welcome
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
Discussion
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
Discussion
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 Schä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
KAT + B!
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
TBA
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
Discussions
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
Discussion
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
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
TBA
C.R. Ramakrishnan
18:00-18:30
TBA
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
TBA
C.R. Ramakrishnan
18:00-18:30
TBA
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