Schedule of Papers and Events

Summary

The conference and workshops will be held at the Universidad de Los Andes in the Facultad de Ingenieria in the "Nucleo La Hechicera". This is within easy walking distance from the Hotel La Terazza. There will also be a shuttle bus from and back to the hotel.
Day   Morning   Afternoon   Evening
Friday, 9th     Registration  
Saturday, 10th   IWIL Workshop   IWIL Workshop  
Sunday, 11th   Conference   Conference   Reception
Monday, 12th   Conference   Conference  
Tuesday, 13th   Excursion   Excursion  
Wednesday, 14th   Conference   Conference  
Thursday, 15th   Conference   Conference   Banquet

Friday, 9th March

Registration desk
4:00pm‑6:00pm Registration and information

Saturday, 10th March - IWIL Workshop

Registration desk
8:00am‑6:00pm Registration and information
 
Session 1: Invited Talk - Chair: Eugenia Ternovska
9:45‑10:00am Opening Remarks
Eugenia Ternovska, Konstantin Korovin
 
10:00am‑11:00am Craig Interpolation for the Integers: Results, Implementation, and Experiences
Philipp Ruemmer
 
11:00am‑11:30am Break
 
Session 2: Papers - Chair: Geoff Sutcliffe
11:30am‑12:00am Efficient Rule-Matching for Hyper-Tableaux
Bjarne Holen, Dag Hovland, Martin Giese
12:00am‑12:30am Implementing Connection Calculi for First-order Modal Logics
Jens Otten
 
12:30pm‑2:30pm Lunch
 
Session 3: Invited Talk & a Paper - Chair: Konstantin Korovin
2:30pm‑3:30pm Engineering Theories with Z3
Nikolaj Bjørner
3:30pm‑4:00pm Understanding LEO-II's Proofs
Nik Sultana, Christoph Benzmüller

Sunday, 11th March

Registration desk
8:00am‑6:00pm Registration and information
 
Session 1: Invited Talk - Chair: Geoff Sutcliffe
9:00am‑10:00am Matrix Interpretations for Polynomial Derivational Complexity of Rewrite Systems
Aart Middeldorp
 
10:00am‑10:30am Break
 
Session 2: Rewriting - Chair: Konstantin Korovin
10:30am‑11:00am Confluence of Non-Left-Linear TRSs via Relative Termination
Dominik Klein, Nao Hirokawa
11:00am‑11:30am On the Domain and Dimension Hierarchy of Matrix Interpretations
Friedrich Neurauter, Aart Middeldorp
11:30am‑12:00am Backward Trace Slicing for Conditional Rewrite Theories
María Alpuente, Demis Ballis, Francisco Frechina, Daniel Romero
12:00am‑12:30am Ordinals and Knuth-Bendix Orders
Sarah Winkler, Harald Zankl, Aart Middeldorp
 
12:30pm‑2:30pm Lunch
 
Session 3: Temporal Logics - Chair: Mikael Møller
2:30pm‑3:00pm An Asymptotically Correct Finite Path Semantics for LTL
Andreas Morgenstern, Manuel Gesell, Klaus Schneider
3:00pm‑3:30pm Labelled Superposition for PLTL
Martin Suda, Christoph Weidenbach
3:30pm‑3:45pm System Description: Solving Graded/Probabilistic Modal Logic via Linear Inequalities
William Snell, Dirk Pattinson, Florian Widmann
 
4:00pm‑4:30pm Break
 
Session 4: Proofs - Chair: Harald Zankl
4:30pm‑5:00pm Towards Algorithmic Cut-Introduction
Stefan Hetzl, Alexander Leitsch, Daniel Weller
5:00pm‑5:30pm Querying Proofs
David Aspinall, Ewen Denney, Christoph Lüth
5:30pm‑5:45pm System Description: Automated and Human Proofs in General Mathematics: An Initial Comparison
Jesse Alama, Daniel Kuehlwein, Josef Urban

Monday, 12th March

Registration desk
8:00am‑6:00pm Registration and information
 
Session 5: Invited Talk - Chair: Nikolaj Bjorner
9:00am‑10:00am Deductive Generalization, or What can you Learn from your Theorem Prover
Ken McMillan
 
10:00am‑10:30am Break
 
Session 6: SMT - Chair: Laura Kovacs
10:30am‑11:00am E-Matching with Free Variables
Philipp Ruemmer
11:00am‑11:30am Automatic Verification Of TLA+ Proof Obligations With SMT Solvers
Stephan Merz, Hernän Vanzetto
11:30am‑12:00am Lazy Abstraction with Interpolants for Arrays
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina
 
12:30pm‑2:30pm Lunch
 
Session 7: SAT and Constraints - Chair: Philipp Ruemmer
2:30pm‑3:00pm Conflict Anticipation in the Search for Graph Automorphisms
Hadi Katebi, Karem A. Sakallah, Igor L. Markov
3:00pm‑3:15pm System Description: Enfragmo: A System for Modelling and Solving Search Problems with Logic
Amir Aavani, Xiongnan Newman Wu, Shahab Tasharrofi, Eugenia Ternovska, David Mitchell
3:15pm‑3:30pm System Description: iSat: Structure Visualization for SAT Problems
Ezequiel Orbe, Carlos Areces, Gabriel Infante-Lopez

Wednesday, 14th March

Registration desk
8:00am‑6:00pm Registration and information
 
Session 9: Invited Talk - Chair: Karem Sakkalah
9:00am‑10:00am Automatic Inference of Resource Consumption Bounds
Elvira Albert (and Puri Arenas, Samir Genaim, Miguel Gomez-Zamalloa, German Puebla)
 
10:00am‑10:30am Break
 
Session 10: Structure - Chair: Aart Middeldorp
10:30am‑11:00am Linear Constraints Over Infinite Trees
Dulma Rodriguez, Martin Hofmann
11:00am‑11:30am Regular Expressions for Data Words
Leonid Libkin and Domagoj Vrgoc
11:30am‑12:00am Finding Finite Herbrand Models
Stefan Borgwardt, Barbara Morawska
 
12:30pm‑2:30pm Lunch
 
Session 11: Time - Chair: Manuel Gesell
2:30pm‑3:00pm Automatic Generation of Invariants for Circular Derivations in SUP(LA)
Arnaud Fietzke, Evgeny Kruglov, Christoph Weidenbach
3:00pm‑3:30pm Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic
Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen, Amelie Stainer
3:30pm‑4:00pm Dual-Priced Modal Transition Systems with Time Durations
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Mikael H. Möller, Jiri Srba
 
4:00pm‑4:30pm Break
 
Session 12: Lambdas - Chair: David Aspinall
4:30pm‑5:00pm The Permutative Lambda-calculus
Beniamino Accattoli, Delia Kesner
5:00pm‑5:30pm Smart Testing of Functional Programs in Isabelle
Lukas Bulwahn

Thursday, 15th March

Registration desk
8:00am‑6:00pm Registration and information
 
Session 13: Invited Talk - Chair: Andrei Voronkov
9:00am‑10:00am Parameterized Complexity and Fixed-Parameter Tractability of Description Logic Reasoning
Boris Motik
 
10:00am‑10:30am Break
 
Session 14: Description and Non-classical Logics - Chair: Boris Motik
10:30am‑11:00am Solving Language Equations and Disequations with Applications to Disunification in Description Logics and Monadic Set Constraints
Franz Baader, Alexander Okhotin
11:00am‑11:30am Forgetting for Defeasible Logic
Grigoris Antoniou, Thomas Eiter, Kewen Wang
11:30am‑12:00am Moral Reasoning Under Uncertainty
The Anh Han, Ari Saptawijaya, Luís Moniz Pereira
12:00am‑12:30am Duality Between Merging Operators and Social Contraction Operators
Jose Luis Chacon, Ramon Pino Perez
 
12:30pm‑2:30pm Lunch
 
Session 15: Reasoning Systems - Chair: Jose Aguilar
2:30pm‑3:00pm The TPTP Typed First-order Form with Arithmetic
Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Peter Baumgartner
3:00pm‑3:15pm System Description: Random: R-based Analyzer for Numerical DOMains
Francesca Scozzari, Gianluca Amato
3:15pm‑3:30pm System Description: r-TuBound: Loop Bounds for WCET Analysis
Jakob Zwirchmayr, Laura Kovacs, Jens Knoop
3:30pm‑3:45pm Short Paper: A Reference Model and a Theory for Multiagent, Information Systems
Virginia Padilla Sifontes, Jacinto Davila