loading...

UC.PT

International Joint Conference on Automated Reasoning

Programme

All session will be in room Pedro Nunes, 1st floor, the coffee break will be in the atrium of the 2nd floor. (Programme in PDF format, program.pdf).

The presentations are (will be) included as soon as the authors provide the PDF file.


Monday June 27:

09:15--09:30  Opening
09:30--10:30  Invited Talk
 Sumit Gulwani.  Programming by Examples: Applications, Algorithms, and Ambiguity Resolution

10:30--11:00  Break

11:00--12:30  Session Satisfiability of Boolean Formulas

11:00--11:30
 Benjamin Kiesl, Martina Seidl, Hans Tompits and Armin Biere. Super-Blocked Clauses
11:30--12:00
 Jasmin Christian Blanchette, Mathias Fleury and Christoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

12:00--14:00  Lunch

14:00--15:40  Session First-Order Theorem Proving

14:00--14:30
 Giles Reger, Martin Suda, Andrei Voronkov and Krystof Hoder. Selecting the Selection
14:30--15:00
 Stephan Schulz and Martin Mohrmann. Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
15:00--15:20  [SD]
 Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner and Sebastian Zivota. System Description: GAPT 2.0
15:20--15:40  [SD]
 Jens Otten. NanoCoP: A Non-clausal Connection Prover

15:40--16:10  Break

16:10--17:30  Session Verification I

16:10--16:40  
 Taolue Chen, Xincai Gu and Zhilin Wu. A complete decision procedure for linearly compositional separation logic with data constraints
16:40--17:10
 Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt and Juergen Giesl. Lower Runtime Bounds for Integer Programs
17:10--17:30  [SD]
 Francisco Duran, Steven Eker, Santiago Escobar, Narciso Marti-Oliet, Jose Meseguer and Carolyn Talcott. Built-in Variant Generation and Unification, and their Applications in Maude 2.7

17:30--17:45  Break

17:45--18:45  Awards (Herbrand Award and Best Paper Award)
19:00--          Welcome reception

Tuesday June 28:

09:00--10:00  Invited Talk
 Gilles Barthe.  Verification of differential private computations
10:00--10:30  
 Joseph Boudou. Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition

10:30--11:00  Break

11:00--12:30  Session  Non-classical Logics

11:00--11:30
 Diana Costa and Manuel A. Martins. A Tableau System for Quasi-Hybrid Logic
11:30--12:00
 Simon Docherty and David Pym. Intuitionistic layered graph logic
12:00--12:30
 Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron and Pietro Sala. Interval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments

12:30--14:00  Lunch

14:00--15:40  Session  Modal Logics

14:00--14:30
 Jeremy Dawson, James Brotherston and Rajeev Gore. Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi
14:30--15:00
 Revantha Ramanayake. Inducing syntactic cut-elimination for indexed nested sequents
15:00--15:20  [SD]
 Yoni Zohar and Anna Zamansky. Gen2sat: an Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi
15:20--15:40  [SD]
 Claudia Nalon, Ullrich Hustadt and Clare Dixon. KSP: A resolution-based prover for multimodal K

15:40--16:10  Break

16:10--16:40  Session First-Order Logic and Proof Theory

16:10--16:40
 David Cerna and Alexander Leitsch. Schematic Cut elimination and the Ordered Pigeonhole Principle
16:40--17:10
 Viorica Sofronie-Stokkermans. On Interpolation and Symbol Elimination in Theory Extensions
17:10--17:30 [SD]
 Takahito Aoto and Kentaro Kikuchi. Nominal Confluence Tool


Wednesday June 29:

09:00--10:00  Invited Talk
 Arnon Avron.  A logical framework for developing and mechanizing set theories
10:00--10:30  
 Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai and Noriko Arai. Race against the Teens -- Benchmarking Mechanized Math on Pre-university Problems

10:30--11:00  Break

11:00--12:30  Session Verification II

11:00--11:30
 Francesco Alberti, Silvio Ghilardi and Elena Pagani. Counting Constraints in Flat Array Fragments
11:30--12:00
 Benjamin Aminof and Sasha Rubin. Model Checking Parameterised Multi-Token Systems via the Composition Method
12:00--12:30
 Konstantinos Athanasiou, Peizun Liu and Thomas Wahl. Unbounded-Thread Program Verification using Thread-State Equations

12:30--14:00  Lunch

14:00--15:45  Business Meetings

16:00--          Social Program

Thursday June 30:

09:00--10:00  Invited Talk
 André Platzer.  Logic and proofs for cyber-physical systems
10:00--10:30  
 Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur and Mingshuai Chen. Interpolation synthesis for quadratic polynomial inequalities and combination with EUF

10:30--11:00  Break

11:00--12:30  Session Satisfiability-Module Theories

11:00--11:30
 Leonardo de Moura and Daniel Selsam. Congruence Closure in Intensional Type Theory
11:30--12:00
 Roberto Sebastiani. Colors Make Theories Hard
12:00--12:30
 Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes and Cesare Tinelli. Model Finding for Recursive Functions in SMT

12:30--14:00  Lunch

14:00--15:40  Session  Satisfiability Modulo Theories and Rewriting

14:00--14:30
 Martin Bromberger and Christoph Weidenbach. Fast Cube Tests for LIA Constraint Solving
14:30--15:00
 Kshitij Bansal, Clark Barrett, Andrew Reynolds and Cesare Tinelli.  A new decision procedure for finite sets and cardinality in SMT
15:00--15:20 [SD]
 Vu Xuan Tung, To Van Khanh and Mizuhito Ogawa. raSAT : SMT Solver for Polynomial Constraints
15:20--15:50
 Hans De Nivelle. Subsumption Algorithms for Three-Valued Geometric Resolution

15:50--16:10  Break

16:10--17:20  Session Higher-order logic

16:10--16:40
 Michael Färber and Chad Brown. Internal guidance for Satallax
16:40--17:00 [SD]
 Max Wisniewski, Alexander Steen, Kim Kern and Christoph Benzmueller. Effective Normalization Techniques for HOL
17:00--17:20 [SD]
 Lars Hupel and Viktor Kuncak. Translating Scala Programs to Isabelle/HOL