VSL 2014: VIENNA SUMMER OF LOGIC 2014

PROGRAM FOR FRIDAY, JULY 18TH: TALK VIEW

Days:
previous day
next day
all days

View: with abstractssession overview

iPRA
QUANTIFY
STAST
ParSearchOpt
LATD
ICLP
IJCAR
VPT
HOPA
WST
ASA
WWV
ITRS
NSV
APPA
PCCR
PAS
SAT
CAV
CSL-LICS
SMT
LaSh
Coq
VSTTE
NLSR
ITP
NMR
PSC
EC2
QED
CHR
VSL
ADDCT
LC
FCS-FCC
RTA-TLCA
CSPSAT
CICLOPS-WLPE
FLoC
RCRA
AISS
NLCS
CSF
DL
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-09:15
Presentation of Three Neat Tricks in Coq 8.5
Jason Gross
09:15-09:45
Towards a better-behaved unification algorithm for Coq
Beta Ziliani, Matthieu Sozeau
09:45-10:15
Proof-relevant rewriting strategies in Coq
Matthieu Sozeau
08:45-10:15
How do we get inductive invariants? (Part A)
David Monniaux
08:45-08:50
Summer School Opening
Gopal Gupta
08:50-10:15
Probabilistic Logic Programming I
C.R. Ramakrishnan
08:45-10:15 CAV Tutorial: How do we get inductive invariants?
08:45-09:15
Fairness for Infinite-State Systems
Byron Cook, Heidy Khlaaf, Nir Piterman
09:15-09:45
Reducing Deadlock and Livelock Freedom to Termination
Byron Cook, Stephen Magill, Matthew Parkinson, Thomas Stroeder
09:45-10:15
Specifying and verifying liveness properties of QLOCK in CafeOBJ
Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi
08:45-09:10
Store Buffer Reduction with MMUs
Mikhail Kovalev, Ernie Cohen, Geng Chen
09:10-09:35
Separation Kernel Verification: the XtratuM Case Study
David Sanan, Andrew Butterfield, Michael Hinchey
09:35-10:00
Separation algebras for C verification in Coq
Robbert Krebbers
10:00-10:15
Automatically verified implementation of data structures based on AVL trees (SHORT)
Martin Clochard
08:45-09:00
LaSh and QUANTIFY Openings
Lash, Quantify
09:00-10:00
Instantiation-based reasoning, EPR encodings and all that
Konstantin Korovin
08:45-09:00
LaSh and QUANTIFY Openings
Lash, Quantify
09:00-10:00
Instantiation-based reasoning, EPR encodings and all that
Konstantin Korovin
08:45-09:45
Tutorial (tentative): TBA
Enrico Giunchiglia
09:45-10:15
SAT Compilation for Constraints over Finite Structured Domains
Alexander Bau
08:45-09:15
Relatively filtral quasivarieties
James Raftery
09:15-09:45
On logics of varieties and logics of semilattices
Josep Maria Font, Tommaso Moraschini
09:45-10:15
Congruential deductive systems associated with equationally orderable varieties
Ramon Jansana
08:45-09:15
Semantial and syntactial charaterisation of some extensions of the class of MV-algebras
Krystyna Mruczek-Nasieniewska
09:15-09:45
The space of directions of a polyhedron
Vincenzo Marra, Daniel McNeill, Andrea Pedrini
09:45-10:15
Interpreting Lukasiewicz logic into Intuitionistic logic
Vincenzo Marra, Daniel Mcneill, Andrea Pedrini
08:45-09:45
Invited Talk
Hermann Schichl
08:45-09:45
Cryptosense: Formal Analysis of Security APIs from Research to Spin-Off
Graham Steel
08:45-09:45
Cryptosense: Formal Analysis of Security APIs from Research to Spin-Off
Graham Steel
08:45-09:45
Invited Talk: Fragments of Logic, Language, and Computation
Patrick Blackburn
09:45-10:15
On the Non-Monotonic Description Logic ALC+Tmin
Oliver Fernandez Gil
08:45-09:45
Invited Talk: Fragments of Logic, Language, and Computation
Patrick Blackburn
09:45-10:15
On the Non-Monotonic Description Logic ALC+Tmin
Oliver Fernandez Gil
08:45-09:00 Workshop Opening
08:45-09:45
Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)
Klaus von Gleissenthall, Andrey Rybalchenko, Santiago Zanella-Béguelin
09:00-09:15 Workshop opening
09:00-10:00
Coherent Logic and Applications
Marc Bezem
09:00-10:00
Coherent Logic and Applications
Marc Bezem
09:00-10:00
Decision Problems for Linear Recurrence Sequences
Joel Ouaknine
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014)
Birte Glimm, Nicolas Matentzoglu, Bijan Parsia, Andreas Steigmiller
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-18:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014)
David Cok, David Deharbe, Tjark Weber
09:00-09:30
Satisfiability Solvers
Marijn Heule
09:30-10:15
Proofs in Satisfiability Modulo Theories
Clark Barrett, Pascal Fontaine, Leonardo De Moura
09:00-10:15
Interpolation in Description Logic: A Survey
Frank Wolter
09:00-10:00
Machine Translation: Green, Yellow, and Red (abstract)
Aarne Ranta
09:00-10:00
Machine Translation: Green, Yellow, and Red (abstract)
Aarne Ranta
09:00-10:15
Tackling the Awareness-Behaviour Divide in Security: (step 1) Understand the User
Lynne Coventry
09:00-09:35
QED: a grand unified theory?
John Harrison
09:35-10:15
How to prove the odd order from the four color theorem
Georges Gonthier
09:15-10:15
Trade-Off Analysis Meets Probabilistic Model Checking
Christel Baier, Clemens Dubslaff, Sascha Klueppelholz
09:15-10:15
Intersection Types, Game Semantics and Higher-Order Model Checking
Luke Ong
09:15-10:15
Synthesis for monadic logic over the reals
Mark Reynolds
09:15-10:15
Test-Input Generation using Computational Real Algebraic Geometry
Hoon Hong
09:15-10:15
Does Wait-Freedom Matter?
Kapil Vaswani
09:15-10:15
Automating the verification of floating-point algorithms
Guillaume Melquiond
09:15-10:15
Program extraction in Church's simple theory of types (invited talk)
Ulrich Berger, Tie Hou
09:15-10:15
CSPs and fixed-parameter tractability
Dániel Marx
09:15-09:45
A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary
Amroun Kamal, Habbas Zineb, Aggoune-Mtalaa Wassila
09:45-10:15
Dispensable Instantiations in Constraint Satisfaction Problems
Eugene Freuder, Diarmuid Grimes, Richard Wallace
09:15-10:15
TBA
Grigore Rosu
09:45-10:25
Nuances of the JavaCard API on the cryptographic smart cards - JCAlgTest project
Petr Svenda
09:45-10:15
A Hybrid Analysis for Security Protocols with State
John D Ramsdell, Daniel Dougherty, Joshua Guttman, Paul D Rowe
10:45-11:15
Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
Christoph Haase
11:15-11:45
On the Discriminating Power of Passivation and Higher-Order Interaction
Marco Bernardo, Davide Sangiorgi, Valeria Vignudelli
11:45-12:15
Asymptotic behaviour in temporal logic
Eugene Asarin, Michel Bockelet, Aldric Degorre, Cătălin Dima, Chunyan Mu
12:15-12:45
Weight Monitoring with Linear Temporal Logic: Complexity and Decidability
Christel Baier, Joachim Klein, Sascha Klueppelholz, Sascha Wunderlich
10:45-11:15
On Context Semantics for Interaction Nets
Matthieu Perrinel
11:15-11:45
The Geometry of Synchronization
Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo, Akira Yoshimizu
11:45-12:15
A new correctness criterion for MLL proof nets
Thomas Ehrhard
12:15-12:45
Non-Elementary Complexities for Branching VASS, MELL, and Extensions
Ranko Lazić, Sylvain Schmitz
10:45-11:45
What is Homotopy Type Theory?
Daniel Licata
11:45-12:15
QuickChick: Property-Based Testing for Coq
M. Dénès, C. Hritcu, L. Lampropoulos, Z. Paraskevopoulou, B.C. Pierce
12:15-12:45
Proof-Pattern Search in Coq/SSReflect
Jónathan Heras, Ekaterina Komendantskaya
10:45-12:15
How do we get inductive invariants? (Part B)
David Monniaux
10:45-13:00
Probabilistic Logic Programming II
C.R. Ramakrishnan
10:45-12:45 CAV Tutorial: How do we get inductive invariants?
10:45-11:15
A Finite Model Property for Intersection Types
Richard Statman
11:15-11:45
On Isomorphism of "Functional'' Intersection and Union Types
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, Maddalena Zacchi
10:45-11:15
Automating Elementary Interpretations
Harald Zankl, Sarah Winkler, Aart Middeldorp
11:15-11:45
A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion
Haruhiko Sato, Sarah Winkler
11:45-12:15
Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling
Alexander Bau, René Thiemann, Johannes Waldmann
12:15-12:45
A Solution to Endrullis-08 and Similar Problems
Alfons Geser
12:45-13:00
Discussion
Everyone
10:45-11:30
Quantifier handling in calculi for quantified Boolean formulas
Uwe Egly
11:30-12:00
Encoding Reachability with Quantification
Michael Cashmore, Maria Fox, Enrico Giunchiglia
12:00-12:30
EPR Encodings of Bit-Vector Problems Even With Quantifiers
Gergely Kovásznai, Andreas Fröhlich, Armin Biere
12:30-13:00
Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction
Hubie Chen
10:45-11:15
Parameterized Model Checking of Rendezvous Systems
Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, Helmut Veith
11:15-11:45
Model Checking Communicating Finite-State Machines using Local Temporal Logics
Roy Mennicke
11:45-12:15
Unary Pushdown Automata and Straight-Line Programs
Dmitry Chistikov, Rupak Majumdar
12:15-12:45
Of stacks (of stacks (...) with blind counters) with blind counters
Georg Zetzsche
10:45-11:15
First-Order Automated Theorem Provers
Stephan Schulz
11:15-11:45
Higher-Order Automated Theorem Provers
Christoph Benzmüller
10:45-11:15
Synthesis of Algorithms on Sets Represented as Monotone Lists
Isabela Dramnesc
11:15-11:45
New predicate transformer for symbolic modeling
A. Letichevsky, O. Letychevskyi, V. Peschanenko, T. Weigert
11:45-12:15
VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
H. Huang, F. Song, Z. Qian, K. Li, J. Chen, S. Guan, W. Huang
12:15-12:45
Symbolic Problem Solving With Bidirectional Executable Representations
Jakob Praher
10:45-11:45
Up and Out: Scaling Formal Analysis Using Model-Based Development and Architecture Modeling
Michael Whalen
11:45-12:10
A logical analysis of framing for specifications with pure method calls
Anindya Banerjee, David Naumann
12:10-12:35
A certifying frontend for (sub)polyhedral abstract domains
Alexis Fouilhe, Sylvain Boulmé
12:35-13:00
Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
Julian Nagele, René Thiemann, Sarah Winkler
10:45-11:15
Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine
B. Bogaerts, J. Jansen, B. De Cat, G. Janssens, M. Bruynooghe, M. Denecker
11:15-11:45
Logical Machinery of Heuristics (Preliminary Report)
Shahab Tasharrofi, Eugenia Ternovska
11:45-12:15
Modeling High School Timetabling as PartialWeighted maxSAT
Emir Demirović, Nysret Musliu
12:15-12:45
Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability
Jeremias Berg, Matti Järvisalo, Brandon Malone
12:45-13:00
Depart for Workshop Lunch
Lash
10:45-11:45
Invited talk: MaxSat and SoftCSPs
Fahiem Bacchus
11:45-12:15
Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms
El Mouelhi Achref, Philippe Jegou, Cyril Terrioux, Bruno Zanuttini
12:15-12:45
BreakIDGlucose: on the importance of row symmetry
Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe
10:45-11:45
The Range of Realization Which modal logics have explicit counter parts
Melvin Fitting
11:45-12:45
Tutorial: Fuzzy Description Logics (Part 1)
Franz Baader
10:45-11:15
Exposing Predictive Analytics through Natural Language Dialog
Jeroen Van Grondelle, Christina Unger, Frank Smit
11:15-11:45
Natural Language Access to Data
C. Condoravdi, K. Richardson, V. Sikka, A. Suenbuel, R. Waldinger
10:45-11:15
A Portfolio Based Parallel SAT Solver with Multiple Deletion Strategies
Long Guo, Said Jabbour, Jerry Lonlac, Lakhdar Sais
11:15-11:45
Towards a Parallel Hierarchical Adaptive Solver Tool
Salvador Abreu, Danny Munera, Daniel Diaz
11:45-12:15
On the Parallelization of Randomized Propagation-based Constraint Solving
Alejandro Arbelaez, Charlotte Truchet, Philippe Codognet
12:15-12:45
A Constraint-based Parallel Local Search for Disjoint Rooted Distance-Constrained Minimum Spanning Tree
Alejandro Arbelaez, Deepak Mehta, Barry O'Sullivan, Luis Quesada
10:45-11:25
Banking security Wish list: notes from the edge
George French
11:25-12:05
Well-typed generic smart-fuzzing for APIs
Thomas Braibant, Jonathan Protzenko, Gabriel Scherer
12:05-12:45
Caetus tool
Josef Hertl
10:45-11:10
Towards Practical Deletion Repair of Inconsistent DL-programs
Thomas Eiter, Michael Fink, Daria Stepanova
11:10-11:35
An Argumentation System for Reasoning with Conflict-minimal Paraconsistent ALC
Wenzhao Qiao, Nico Roos
11:35-12:00
Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics
Camille Bourgaux, Meghyn Bienvenu, François Goasdoué
10:45-11:10
Towards Practical Deletion Repair of Inconsistent DL-programs
Thomas Eiter, Michael Fink, Daria Stepanova
11:10-11:35
An Argumentation System for Reasoning with Conflict-minimal Paraconsistent ALC
Wenzhao Qiao, Nico Roos
11:35-12:00
Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics
Camille Bourgaux, Meghyn Bienvenu, François Goasdoué
10:45-11:45
Wait-Freedom Made Practical
Erez Petrank
11:45-12:15
A new reduction for event-driven distributed programs
Ankush Desai, Pranav Garg, P. Madhusudan
10:45-11:15
Leveraging Linear and Mixed Integer Programming for SMT
Tim King, Clark Barrett, Cesare Tinelli
11:15-11:45
raSAT: SMT for Polynomial Inequality
To Van Khanh, Vu Xuan Tung, Mizuhito Ogawa
11:45-12:15
Better Answers to Real Questions
Marek Kosta, Thomas Sturm, Andreas Dolzmann
12:15-12:45
Towards Conflict-Driven Learning for Virtual Substitution
Konstantin Korovin, Marek Kosta, Thomas Sturm
10:45-11:30
Extracting Monadic Parsers from Proofs
Ulrich Berger, Alison Jones, Monika Seisenberger
11:30-12:15
Intuitionistic Ancestral Logic
Liron Cohen, Robert Constable
10:45-11:15
Resolution Based Uniform Interpolation for Expressive Description Logics
Patrick Koopmann, Renate A. Schmidt
11:15-11:45
Practical CNF Interpolants Via BDDs
Alexander Legg, Nina Narodytska, Leonid Ryzhyk
11:45-12:15
Interpolation and Domain Independence applied to Databases
Enrico Franconi, Paolo Guagliardo, Volha Kerhet, Nhung Ngo
12:15-12:45
Tree-based Modular SMT Solving
Georg Schadler, Georg Hofferek
10:45-11:45
Constructive Cryptography and Security Proofs
Ueli Maurer
10:45-11:15
Connection matrices of finite rank instead of definability in Monadic Second Order Logic
Nadia Labai, Johann Makowsky
11:15-11:45
Backdoors into Two Occurrences
Jan Johannsen
10:45-11:30
Decision justifications for wireless network selection
Debora Jeske, Lynne Coventry, Pam Briggs
11:30-12:15
Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Oliver Buckley, Jason Nurse, Philip Legg, Michael Goldsmith, Sadie Creese
12:15-13:00
Modelling User Devices in Security Ceremonies
Taciane Martimiano, Jean Everson Martina, Maina Olembo, Marcelo Carlos
10:45-11:15
Neighbourhood SAC for Preprocessing and Search
Richard Wallace
10:45-11:45
A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic
Nicolas Peltier
10:45-11:15
Automated Test Case Generation and Model Checking with CHR
Ralf Gerlich
11:15-11:45
From XML Schema to JSON Schema: Translation with CHR
Falco Nogatz, Thom Fruehwirth
11:45-12:15
Constraint Handling Rules with Multiset Comprehension Patterns
Edmund Soon Lee Lam, Iliano Cervesato
12:15-12:45
Discussion
Everyone
10:45-11:15
Automated Test Case Generation and Model Checking with CHR
Ralf Gerlich
11:15-11:45
From XML Schema to JSON Schema: Translation with CHR
Falco Nogatz, Thom Fruehwirth
11:45-12:15
Constraint Handling Rules with Multiset Comprehension Patterns
Edmund Soon Lee Lam, Iliano Cervesato
12:15-12:45
Discussion
Everyone
10:45-11:30
On Unfolding for Programs Using Strings as a Data Type
Andrei Nemytykh
11:30-12:15
Branching Processes of Conservative Nested Petri Nets
Daniil Frumin, Irina Lomazova
12:15-13:00
Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem
Geoff Hamilton, Morten Heine Sørensen
10:45-11:20
25 years of the Mizar Mathematical Library
Adam Grabowski
11:20-11:55
The seL4 microkernel verification
Gerwin Klein
11:55-12:15
Towards Formally Verified Theorem Provers - Part I
Magnus Myreen
12:15-12:30
Towards Formally Verified Theorem Provers - Part II
Ramana Kumar
12:30-13:00
TBA
Claudio Sacerdoti Coen
10:45-11:45
Program Analysis for JavaScript Web Applications
Anders Møller
11:45-12:15
Analyzing JavaScript: The Bad Parts
Nicholas Labich
12:15-12:45
Saturation of Concurrent Collapsible Pushdown Systems (Extended Abstract)
Matthew Hague
11:00-12:00
On local induction schemes
Andres Cordón-Franco
12:00-13:00
Tutorial on Classical Realizability and Forcing 2
Alexandre Miquel
11:20-11:50
Concept Learning by a Monte-Carlo Tree Search of Argumentations
Regis Riveret, Pasquale Caianiello, Stefania Costantini, Moez Draief
11:50-12:20
Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies
Shashank Pathak, Luca Pulina, Armando Tacchella
12:20-12:40
Self Regulating Mechanisms for Network Immunization
Luca Mancini, Alfredo Milani, Valentina Poggioni, Andrea Chiancone
12:40-13:00
A Controlled Stability Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock
Slimane Abou-Msabah
11:45-12:00 Break
11:45-12:15
Transfer Semantics for the Clear Parser
Richard Crouch
12:15-12:45
Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts
Juyeon Kang, Saint Dizier Patrick
12:00-12:30
Uniform Proofs of Normalisation and Approximation for Intersection Types
Kentaro Kikuchi
12:30-13:00
Indexed linear logic and higher-order model checking
Charles Grellois, Paul-André Melliès
12:00-12:30
Interactive Theorem Provers from the perspective of Isabelle/Isar
Makarius Wenzel
12:30-13:00
Calculus of Inductive Constructions
Christine Paulin-Mohring
12:00-12:25
Temporal OBDA with LTL and DL-Lite
A. Artale, R. Kontchakov, A. Kovtunova, V. Ryzhikov, F. Wolter, M. Zakharyaschev
12:25-12:50
Complexity of Temporal Query Abduction in DL-Lite
Szymon Klarman, Thomas Meyer
12:50-12:53
Temporalising EL Concepts with Time Intervals
Jared Leo, Ulrike Sattler, Bijan Parsia
12:53-12:56
Transition Constraints for Temporal Attributes
E. A. Nasubo Ongoma, C. Maria Keet, Thomas Meyer
12:56-12:59
A Stream-Temporal Query Language for Ontology Based Data Access
Özgür Lütfü Özcep, Ralf Möller, Christian Neuenstadt
12:00-12:20
A tool for automating the computationally complete symbolic attacker
Hubert Comon-Lundh, Veronique Cortier, Guillaume Scerri
12:20-12:40
Towards a Coinductive Characterization of Computational Indistinguishability
Alberto Cappai, Ugo Dal Lago
12:40-13:00
Actual Causes of Security Violations
Anupam Datta, Dilsun Kaynar, Divya Sharma, Arunesh Sinha
12:00-12:30
Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction
Robert Ganian, Stefan Szeider, M.S. Ramanujan
12:00-12:30
Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
Paula Chocron, Pascal Fontaine, Christophe Ringeissen
12:30-13:00
Finding Minimum Type Error Sources
Zvonimir Pavlinovic, Tim King, Thomas Wies
12:00-12:30
Some thoughts about benchmarks for NMR
Daniel Le Berre
12:30-13:00
Towards a Benchmark of Natural Language Arguments
Elena Cabrio, Serena Villata
12:15-13:00 Discussion
14:30-15:00
Formalization of Error-correcting Codes using SSReflect
Reynald Affeldt, Jacques Garrigue
15:00-15:30
Autosubst: Automation for de Bruijn Substitutions
Steven Schäfer, Tobias Tebbi, Gert Smolka
15:30-16:00
Automating Abstract Logics
Gregory Malecha, Jesper Bengtson, Adam Chlipala
14:30-15:00
Regular Combinators for String Transformations
Rajeev Alur, Adam Freilich, Mukund Raghothaman
15:00-15:30
On Periodically Iterated Morphisms
Joerg Endrullis, Dimitri Hendriks
15:30-16:00
Finite-Memory Strategy Synthesis for Robust Multidimensional Mean-Payoff Objectives
Yaron Velner
14:30-15:00
A type theory for productive coprogramming via guarded recursion
Rasmus Ejlers Møgelberg
15:00-15:30
Formulae-as-Types for an Involutive Negation
Guillaume Munch-Maccagnoni
15:30-16:00
Eilenberg-MacLane Spaces in Homotopy Type Theory
Daniel R. Licata, Eric Finster
14:30-16:00
Hardware Model Checking (Part A)
Fabio Somenzi
14:30-16:00
Answer Set Programming I
Martin Gebser
14:30-15:00
Lucretia — intersection type polymorphism for scripting languages
Marcin Benke, Viviana Bono, Aleksy Schubert
15:00-15:30
Liquid Intersection Types
Mário Pereira, Sandra Alves, Mário Florido
14:30-15:15
Frege on mathematical progress
Patricia Blanchette
15:15-16:00
On Bernays' Generalization of Cantor's Theorem
Gabriel Uzquiano
14:30-15:15
Large cardinals, forcing axioms, and the theory of subsets of \omega_1
Daisuke Ikegami
15:15-16:00
Locally definable well-orders
Philipp Lücke
14:30-15:00
On the derivational complexity of Kachinuki orderings
Dieter Hofbauer
15:00-15:30
Kurth's Criterion H Revisited
Alfons Geser
15:30-16:00
Another Proof for the Recursive Path Ordering
Nachum Dershowitz
14:30-15:30
Algorithmic Paradigms for Solving QBF
Fahiem Bacchus
15:30-16:00
Projective Quantifier Elimination for Equational Constraint Solving
Javier Álvez, Montserrat Hermo, Paqui Lucio
14:30-15:30
Playing with Automata and Trees
Olivier Serre
15:30-16:00
Quantitative Automatic Structures
Martin Lang
14:30-15:30
Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian Emmes, Carsten Fuhs
15:30-16:00
Discussion
Everyone
14:30-15:30
Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
Jürgen Giesl, Thomas Ströder, Peter Schneider-Kamp, Fabian Emmes, Carsten Fuhs
15:30-16:00
Discussion
Everyone
14:30-15:00
Foundational Proof Certificates
Dale Miller
15:00-15:30
Deduction Modulo
Gilles Dowek
15:30-16:00
Mathematical Proof Analysis
Alexander Leitsch
14:30-15:30
Automated verification of security protocols and services
Michael Rusinowitch
15:30-16:00
Building explicit induction schemas for cyclic induction reasoning
Sorin Stratulat
14:30-14:55
Model Checking Parameterized Timed Systems
Luca Spalazzi, Francesco Spegni
14:55-15:20
Timed Refinements for Verification of Real-Time Object Code Programs
Mohana Asha Latha Dubasi, Sudarshan Srinivasan, Vidura Wijayasekara
15:20-15:45
Formal Modeling and Verification of CloudProxy
Wei Yang Tan, Rohit Sinha, John Manferdelli, Sanjit Seshia
14:30-15:30
Laziness is next to Godliness
Peter Stuckey
15:30-16:10
Lazy Model Expansion: Interleaving Grounding with Search
Broes De Cat, Marc Denecker, Peter Stuckey, Maurice Bruynooghe, Bart Bogaerts
14:30-15:00
A low-level treatment of quantifiers in categorical compositional distributional semantics
Ondrej Rypacek, Mehrnoosh Sadrzadeh
15:00-15:30
Divergence in Dialogues
Christophe Fouquere, Myriam Quatrini
15:30-16:00
Modelling implicit dynamic introduction of function symbols in mathematical texts
Marcos Cramer
14:30-15:30
First-Order Logics and Truth Degrees
George Metcalfe
15:30-16:00
Classification of germinal MV-algebras
Leonardo Manuel Cabrer
14:30-15:30
General Panel Discussion
All Workshop Presenters
15:30-16:00
Towards a complete constraint solver on GPU
F. Campeotto, A. Dal Palù, A. Dovier, F. Fioretto, E. Pontelli
14:30-15:10
Application Oriented Low Cost Security Modules
Dan Cvrcek
15:10-15:50
Security APIs for Device Enrolment
Mike Bond
14:30-14:55
Gödel FL_0 with Greatest Fixed-Point Semantics
Stefan Borgwardt, José A. Leyva Galano, Rafael Peñaloza
14:55-15:20
Fuzzy DLs over Finite Lattices with Nominals
Stefan Borgwardt
15:20-15:23
A MILP-based decision procedure for the (Fuzzy) Description Logic ALCB
Fernando Bobillo, Umberto Straccia
15:23-15:26
Complexity sources in FDL
Marco Cerami, Umberto Straccia
15:26-15:29
Gödel Description Logics with General Models
Stefan Borgwardt, Felix Distel, Rafael Peñaloza
15:29-15:32
Certain Answers in a Rough World
Rafael Peñaloza, Veronika Thost, Anni-Yasmin Turhan
15:32-15:35
Bayesian Description Logics
Ismail Ilkan Ceylan, Rafael Peñaloza
15:35-15:38
Reasoning about Belief Uncertainty in DL-Lite N bool
Ala Djeddai, Hassina Seridi, Tarek Khadir
15:38-15:41
Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information
F. Cerutti, G. de Mel, T. Norman, N. Oren, A. Parvizi, P. Sullivan, A. Toniolo
15:41-15:44
Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure?
Tahani Alsubait, Bijan Parsia, Uli Sattler
15:44-15:47
Mary, What's Like All Cats?
Andreas Ecke, Rafael Peñaloza, Anni-Yasmin Turhan
14:30-16:00 SMT-COMP and SMT-EVAL Presentations
14:30-15:15
Proof-search in natural deduction calculi for IPL
Mauro Ferrari, Camillo Fiorentini
15:15-16:00
A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic
Sergey Melikhov
14:30-15:00
Using Interpolation for the Verification of Security Protocols (Extended Abstract)
Marco Rocchetto, Luca Viganò, Marco Volpe
15:00-15:30
Interpolation Strategies
Kenneth McMillan
15:30-16:00
Towards Craig Interpolation for String Constraints
P.A. Abdulla, M.F. Atig, Y.-F. Chen, L. Holik, A. Rezine, P. Ruemmer, J. Stenman
14:30-15:00
Adversary Gain vs. Defender Loss in Quantified Information Flow
Piotr Mardziel, Mario Alvim, Michael Hicks
15:00-15:30
Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis
Abhishek Bichhawat, Vineet Rajani, Deepak Garg, Christian Hammer
15:30-15:50
Micro-Policies: Formally Verified Low-Level Tagging Schemes for Safety and Security (Short Paper)
Catalin Hritcu
14:30-15:30
Structural Decomposition Methods: How They Matter
Georg Gottlob
14:30-15:15
The Social Engineering Personality Framework
Sven Uebelacker, Susanne Quiel
15:15-16:00
Modeling Human Behaviour with Higher Order Logic: Insider Threats
Jaap Boender, Marieta Georgieva Ivanova, Florian Kammueller, Giuseppe Primiero
14:30-15:00
Decidability of Iteration-free PDL with Parallel Composition
Joseph Boudou, Philippe Balbiani
15:00-15:30
Axiomatic and Tableau-Based Reasoning for Kt(H,R)
Renate A. Schmidt, John Stell, David Rydeheard
15:30-16:00
On dual tableau-based decision procedures for relational fragments
Domenico Cantone, Joanna Golinska-Pilarek, Marianna Nicolosi-Asmundo
14:30-15:00
Epsilon-semantics and hybrid automata
Tommaso Dreossi
15:00-15:30
Verifying Floating-Point Implementations of Nonlinear Functions
Sicun Gao
15:30-16:00
Correctness of Parallel Interval Computations
Philippe Theveny
14:30-15:00
TBA
Thomas C. Hales
15:00-15:30
Mixing proofs and computations
Michael Beeson
15:30-16:00
The Naproche system: Proof-checking mathematical texts in controlled natural language
Marcos Cramer
14:30-15:15
Weak well orders and related inductions
Gerhard Jaeger
15:15-16:00
Automating inductive proof
Alan Bundy
14:30-15:15
Weak well orders and related inductions
Gerhard Jaeger
15:15-16:00
Automating inductive proof
Alan Bundy
14:30-15:30
Automatic Detection of Webpage Candidates for Site-Level Web Template Extraction
Josep Silva
14:30-15:30
Automatic Detection of Webpage Candidates for Site-Level Web Template Extraction
Josep Silva
14:30-15:00
Analysis of Dialogical Argumentation via Finite State Machines
Anthony Hunter
15:00-15:30
Abduction in Argumentation: Dialogical Proof Procedures and Instantiation
Richard Booth, Dov Gabbay, Souhila Kaci, Tjitze Rienstra, Leendert Van Der Torre
15:30-16:00
Non-Monotonic Reasoning and Story Comprehension
Irene-Anna Diakidoy, Antonis Kakas, Loizos Michael, Rob Miller
14:30-15:00
Environment Unrolling
Steven Lyde, Matthew Might
15:00-15:30
Strong Function Call
Steven Lyde, Matthew Might
15:30-16:00
The modal nature of colors in higher-order model-checking
Charles Grellois, Paul-André Melliès
15:30-16:00
Backdoors into Heterogeneous Classes of SAT and CSP
S. Gaspers, N. Misra, S. Ordyniak, S. Szeider, S. Zivny
15:50-16:40 Poster Session (with coffee break)
16:30-17:00
Asynchronous interaction for Coq
Carst Tankink
17:00-17:30
Coqoon: towards a modern IDE for Coq
Alexander Faithfull, Jesper Bengtson
17:30-18:00
Update on Coq 8.5
Matthieu Sozeau
16:30-18:00
Hardware Model Checking (Part B)
Fabio Somenzi
16:30-17:00
Citations for the Test-of-Time Award from 1994
Dexter Kozen
16:30-18:30
Answer Set Programming II
Martin Gebser
18:30-18:35
Summer School Closing
Gopal Gupta
16:30-17:00
Semantic Types for Classes and Mixins
Ugo De Liguoro, Tzu-Chun Chen
17:00-17:30
Delegation-based Mixin Composition Synthesis
Jan Bessai, Boris Düdder, Andrej Dudenhefner, Moritz Martens
16:30-17:15
Restrictiveness relative to notions of interpretation
Luca Incurvati, Benedikt Loewe
17:15-18:00
Reflection, Trust, Entitlement
Leon Horsten
16:30-17:15
Definable valuation rings
Jochen Königsmann
17:15-18:00
The Fitting subgroup of a supersimple group
Daniel Palacín
16:30-17:30
Discussion and Business Meeting
Everyone
16:30-17:00
Efficiently Solving Quantified Bit-Vectors
Christoph Wintersteiger
17:00-17:30
Quantifier Projection
Nikolaj Bjorner
17:30-18:00
Finding Conflicting Instances of Quantified Formulas in SMT
Andrew Reynolds, Cesare Tinelli, Leonardo De Moura
16:30-17:30
Simulation for infinite state systems.
Piotr Hofman
17:30-18:00
Simulation Over One-Counter Nets is PSPACE-Complete
Patrick Totzke
16:30-17:00
Intelligent Visual Surveillance Logic Programming: Implementation Issues
Alexei A. Morozov, Alexander F. Polupanov
17:00-17:30
A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs
Flavio Cruz, Ricardo Rocha, Seth Goldstein
17:30-18:00
Discussion
Everyone
16:30-17:00
Intelligent Visual Surveillance Logic Programming: Implementation Issues
Alexei A. Morozov, Alexander F. Polupanov
17:00-17:30
A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs
Flavio Cruz, Ricardo Rocha, Seth Goldstein
17:30-18:00
Discussion
Everyone
16:30-17:00
Program Verification (B Method)
Jean-Raymond Abrial
17:00-17:30
Security
Gilles Barthe
17:30-18:00
Deep Inference
Alessio Guglielmi
16:30-17:00
A hybrid path constraint solver combined with meta-heuristic search
Xiaomei Hou, Mengxiang Lin, Tahir Jameel
17:00-17:30
Automatic App Testing of LTL Properties
Farn Wang, Pin Hsiuan Chen, Wen-Hong Chiang
17:30-18:00
Programming Language Aggregation with Applications in Equivalence Checking
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
16:30-18:00 Verified Software Competition (VSCOMP 2014)
16:30-17:10
The D-FLAT System for Dynamic Programming on Tree Decompositions
M. Abseher, B. Bliem, G. Charwat, F. Dusberger, M. Hecher, S. Woltran
17:10-17:50
Cross-Translating Answer Set Programs
Tomi Janhunen
16:30-17:00
Program Extraction Applied to Monadic Parsing
Ulrich Berger, Alison Jones, Monika Seisenberger
17:00-17:30
On Translating Context-Free Grammars into Lambek Categorial Grammars
Stepan Kuznetsov
16:30-17:00
Cut-free calculus for second-order {G\"odel} logic
Ori Lahav, Arnon Avron
17:00-17:30
Poof Search and Co-NP completeness for Many-Valued Logics
Franco Montagna, Mattia Bongini, Agata Ciabattoni
17:30-18:00
Cut and completion?
Sam van Gool, Rosalie Iemhoff
16:30-17:00
Definability of truth predicates in abstract algebraic logic
Tommaso Moraschini
17:00-17:30
Generalizing the Leibniz and Suszko operators
Hugo Albuquerque, Josep Maria Font, Ramon Jansana
17:30-18:00
Church-style type theories over finitary weakly implicative logics
Libor Behounek
16:30-18:00 SMT-LIB Discussion and Business Meeting
16:30-17:00
Specification Synthesis via Generalized Abduction
Aws Albarghouthi, Isil Dillig, Arie Gurfinkel, Marsha Chechik
17:00-17:30
Interpolation from Clausal Proofs
Yakir Vizel, Arie Gurfinkel
17:30-18:00
Concluding discussions
Laura Kovacs, Georg Weissenbacher
16:30-16:50
Protocol Indistinguishability and the Computationally Complete Symbolic Attacker
Gergei Bana, Hubert Comon-Lundh
16:50-17:10
On Well-Founded Security Protocols
Sibylle Froeschle
17:10-17:30
Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model
Gergei Bana, Mitsuhiro Okada
17:30-18:00
Towards Timed Models for Cyber-Physical Security Protocols
Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, Carolyn Talcott
16:30-17:30 PCCR panel
16:30-17:15
What You Enter Is What You Sign: input integrity in an online banking environment
Sven Kiljan, Harald Vranken, Marko van Eekelen
17:15-18:00
Using Statistical Information to Communicate Android Permission Risks to Users
Lydia Kraus, Ina Wechsung, Sebastian Möller
16:30-17:15
Numerical Challenges in Simulation-guided Dynamical System Analysis
Jim Kapinski
16:30-17:00
QED and the TPTP World
Geoff Sutcliffe
17:00-17:30
MathHub.info: Active Mathematics
Michael Kohlhase
17:30-18:00
Hammering towards QED
Cezary Kaliszyk
16:30-17:00
Static Enforcement of Role-Based Access Control
Asad Ali, Maribel Fernandez
17:00-17:30
A Local Logic for Realizability in Web Service Choreographies
R. Ramanujam, S. Sheerazuddin
16:30-17:30 Panel Session: The W3C Web Crypto API
16:40-17:05
Datalog Rewriting Techniques for Non-Horn Ontologies
Mark Kaminski, Yavor Nenov, Bernardo Cuenca Grau
17:05-17:30
Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries
Meghyn Bienvenu, Stanislav Kikot, Vladimir Podolskii
17:00-17:30
The Ackermann Award 2014
Anuj Dawar
17:00-18:00 NMR Social Event
17:30-17:45 Workshop closing
17:30-17:45 Workshop closing
17:30-18:00
Formal Replay of Translation Validation for Highly Optimised C
Thomas Sewell
18:00-18:10 Workshop Closing
18:00-23:30 DL/NMR Social Event and Dinner
18:15-18:35
A completeness theorem for general relativity
Judit X. Madarász, Gergely Székely
18:35-18:55
More On Completion with Horn Filters
Cyrus F Nourani
18:15-18:35
Predicative Mathematics via Safety Relations
Liron Cohen, Arnon Avron
18:35-18:55
Natural Deduction in Renaissance Geometry
Ryszard Mirek
18:55-19:15
Aristotle’s conception of demonstration and modern proof theory
Olga Antonova
18:15-18:35
Modelling Inference in Fiction
Alba Massolo, Luis Urtubey
18:35-18:55
Metalogical Extensions--Part II: First-order Consequences and Gödel
Joachim Mueller-Theys
18:15-18:45
Panel Discussion
John Harrison
10:15-10:45 Coffee Break
13:00-14:30 Lunch Break
16:00-16:30 Coffee Break
Disclaimer | Powered by EasyChair Smart Program