LPAR-16 program
Monday, April 26th
10:00‑11:00 Session 1
10:00 Opening
11:00‑11:30 Coffee Break
11:30‑12:30 Session 2
Chair: Andrei Voronkov
11:30 Geoff Sutcliffe (University of Miami)
The TPTP World - Infrastructure for Automated Reasoning
12:30‑14:00 Lunch
14:00‑15:30 Session 3
Chair: Margus Veanes
14:00 Harald Zankl and Aart Middeldorp
Satisfiability of Non-Linear (Ir)rational Arithmetic
14:30 Michael Codish and Moshe Ivri-Zazon
Pairwise Cardinality Networks
15:00 Fausto Spoto
The Nullness Analyser of Julia
15:30‑16:00 Coffee Break
16:30‑18:00 Session 4
Chair: Michael Codish
16:30 Margus Veanes, Nikolai Tillmann and Jonathan de Halleux
Qex: Symbolic SQL Query Explorer
17:00 Reinhard Pichler, Stefan Rümmele and Stefan Woltran
Counting and Enumeration Problems with Bounded Treewidth
17:30 John Fearnley
Non-oblivious Strategy Improvement
19:30‑23:59 Welcoming party
Tuesday, April 27th
09:00‑10:50 Session 5
Chair: Michael Gabbay
09:00 Michel Parigot (University of Paris VII)
Deep inference: why and how?
10:00 Dougherty Daniel and Liquori Luigi
Logic and computation in a lambda calculus with intersection and union types
10:30 Babacar Diouf
Presentation note of Senegal
10:50‑11:00 Coffee Break
11:30‑12:30 Session 6
Chair: Orna Kupferman
11:30 Regis Blanc, Thomas Henzinger, Thibaud B. Hottelier and Laura Kovacs
ABC: Algebraic Bound Computation for Loops
12:00 Rustan Leino
Dafny: An Automatic Program Verifier for Functional Correctness
12:30‑14:00 Lunch
14:00‑15:30 Session 7
Chair: Geoff Sutcliffe
14:00 Jiri Vyskocil, David Stanovsky and Josef Urban
Automated proof shortening by invention of new definitions
14:30 Bruno Woltzenlogel Paleo
Atomic Cut Introduction by Resolution: Proof Structuring and Compression
15:00 Matthias Horbach
Disunification for Ultimately Periodic Interpretations
15:30‑16:00 Coffee Break
16:00‑17:00 Session 8
Chair: Rustan Leino
16:00 Lennart Beringer, Robert Grabowski and Martin Hofmann
Verifying Pointer and String Analyses with Region Type Systems
16:30 Yoichi Hirai
An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory
Wednesday, April 28th
10:00‑23:59 LPARty
Thursday, April 29th
09:30‑10:30 Session 9
Chair: Michel Parigot
09:30 Michael Gabbay and Murdoch Gabbay
A simple class of Kripke-style models in which logic and computation have equal standing
10:00 Didier Galmiche and Yakoub Salhi
Label-free Proof Systems for Modal Intuitionistic Logic IS5
10:30‑11:00 Coffee Break
11:00‑12:30 Session 10
Chair: Laura Kovacs
11:00 Orna Kupferman and Moshe Vardi
Synthesis for trigger properties
11:30 Laura Bozzelli, Axel Legay and Sophie Pinchinat
Hardness of preorder checking for basic formalisms
12:00 Orna Kupferman and Tami Tamir
Coping with Selfish On-going Behaviors
12:30‑14:00 Lunch
14:00‑15:30 Session 11
Chair: Aart Middeldorp
14:00 Fabio Mogavero, Aniello Murano and Moshe Y. Vardi
Relentful Strategic Reasoning in Alternating-Time Temporal Logic
14:30 Gilles Barthe, marion DAUBIGNARD, Bruce Kapron, Yassine Lakhnech and Vincent Laporte
An equational logic for probabilistic terms
15:00 Martin Berger and Laurence Tratt
Program Logics for Homogeneous Meta-Programming
15:30‑16:00 Coffee Break
16:00‑18:00 Session 12
Chair: Moshe Vardi
16:00 Gourinath Banda and John Gallagher
Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation
16:30 Marco Faella, Margherita Napoli and Mimmo Parente
Graded Alternating-Time Temporal Logic
17:00 Amir Aavani, shahab tasharrofi, Gulay Unel, Eugenia Ternovska and David Mitchell
Speed-up Techniques for Negation in Grounding
17:30 Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot
A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
Friday, April 30th
09:00‑10:10 Short papers
09:00 Antonina Kolokolova, Liu Yongmei, David Mitchell and Eugenia Ternovska
On the Complexity of Model Expansion
09:10 Michael Gabbay
A proof-theoretic treatment of lamda-reduction: lambda-calculus as a logic programming language
09:20 Shahab Tasharrofi and Eugenia Ternovska
Built-in Arithmetic in Knowledge Representation Languages
09:30 Gregory Wheeler
AGM Belief Revision in Monotone Modal Logics
09:40 Choh Man Teng and Gregory Wheeler
Robustness of Evidential Probability
09:50 Amir Aavani , Xiongnan (Newman) Wu, David Mitchell and Eugenia Ternovska
Grounding Count Aggregates
10:00 Yannick Chevalier and Mounira Kourjieh
Decidability of Ground Entailment Problems for Saturated Sets of Clauses
10:30‑11:00 Coffee Break
18:00‑23:59 Farewell party