Days: Sunday, June 4th Monday, June 5th Tuesday, June 6th Wednesday, June 7th Thursday, June 8th Friday, June 9th
View this program: with abstractssession overviewtalk overview
Registration
The 14th International Workshop on the Implementation of Logics
09:00-09:30 Simon Schwarz "Gröbner Bases for Boolean Function Minimization”
09:30-10:00 David Fuenmayor and Christoph Benzmüller "Searching for> Wormholes in Proof-Space"
Break
The 14th International Workshop on the Implementation of Logics
10:30-11:00 Jack McKeown "A Framework for Running Reinforcement Learning Experiments in E"
11:00-11:30 Geoff Sutcliffe, Jack McKeown and Alexander Steen "A Chat with Bard"
11:30-12:30 Panel "Implementation of Logics in the Face of the New AI"
Lunch (provided at UN La Nubia)
Break
Welcome reception
View this program: with abstractssession overviewtalk overview
Registration
Break
SMT / Constraint Solving
| 10:30 | On the Complexity of Convex and Reverse Convex Prequadratic Constraints (abstract)  |
| 11:00 | SMT Solving over Finite Field Arithmetic (abstract) PRESENTER: Thomas Hader |
| 11:30 | Refining Unification with Abstraction (abstract) |
| 12:00 | Experiments on Infinite Model Finding in SMT Solving (abstract) PRESENTER: Cezary Kaliszyk |
Lunch (provided at UN La Nubia)
Practical Aspects of First-Order reasoning and Beyond
| 14:00 | Keep me out of the loop: a more flexible choreographic projection (abstract)  PRESENTER: Robert R. Rasmussen |
| 14:30 | An Interactive SMT Tactic in Coq using Abductive Reasoning (abstract) |
| 15:00 | A Mathematical Benchmark for Inductive Theorem Provers (abstract) PRESENTER: Thibault Gauthier |
| 15:30 | Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic (abstract) |
Break
Short Papers
| 16:30 | Efficient and Verified Continuous Double Auctions (abstract) |
| 16:50 | HoRStify: Sound Security Analysis of Smart Contracts (abstract) |
Conference Dinner - El Refugio, Morrogacho
Welcome from the Dean of the Faculty of Exact and Natural Sciences, Carlos Acosta
View this program: with abstractssession overviewtalk overview
Registration
Break
Verification and Applications I
| 10:30 | Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification (abstract) |
| 11:00 | Trace-based Deductive Verification (abstract) |
| 11:30 | A Fast and Accurate ASP Counting Based Network Reliability Estimator (abstract) PRESENTER: Mohimenul Kabir |
| 12:00 | Mechanising Hall’s Theorem for Countable Graphs (abstract) |
Lunch (on your own)
Verification and Applications II
| 14:00 | Collaborative Inference of Combined Invariants (abstract) |
| 14:30 | Scalable Probabilistic Routes (abstract) |
| 15:00 | Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties (abstract) |
| 15:30 | Model Checking Omega-Regular Hyperproperties with AutoHyperQ (abstract) |
Break
Optional excursion to Chipre to see the sunset. Enquire at the registration desk.
View this program: with abstractssession overviewtalk overview
View this program: with abstractssession overviewtalk overview
Invited Talk - Marijn Heule
| 09:00 | Computer-aided Mathematics: Successes, Advances, and Trust (abstract) |
Break
SAT Solving
| 10:30 | Toward Optimal Radio Colorings of Hypercubes via SAT-solving (abstract) |
| 11:00 | Analyzing Multiple Conflicts in SAT: An Experimental Evaluation (abstract) |
Local Participants' Active Research
- 11:30-11:50 Foot Segmentation for Regional Analgesia Monitoring using Convolutional Random Fourier Features, Juan Carlos Aguirre, M.Eng. student
- 11:50-12:10 Mutual Information-based Inter-Channel Correlation of Motor Imagery Responses, Marcos Loaiza, M.Eng. student
- 12:10-12:30 Interpretable Deep Learning for EEG-based Motor Imagery, Diego Collazos, Ph.D.
Lunch with Locals (Participant Active Researchers)
First-order Logic Reasoning
| 14:00 | Exploring Partial Models with SCL (abstract) |
| 14:30 | How Much Should This Symbol Weigh? A GNN-Advised Clause Selection (abstract) PRESENTER: Filip Bártek |
| 15:00 | Guiding an Instantiation Prover with Graph Neural Networks (abstract) |
| 15:30 | An excursion to the border of decidability: between two- and three-variable logic (abstract) PRESENTER: Oskar Fiuk |
Break
Local Participants' Active Research
- 16:30-16:50 Deep Alignment for Sonification of Emotional States from EEG Data, Hernán Pérez, M.Eng student
- 16:50-17:10 Soundscape Analysis using Acoustic Features and Non-negative Matrix Factorization Methods, Fernando Martínez, Ph.D. student
Local Professor's Active Research
| 17:10 | Software Formal Verification by Rewriting Logic and Declarative Programming (abstract) |
Optional excursion to Termales to swim in the hot springs. Enquire at the registration desk.
View this program: with abstractssession overviewtalk overview
Break
Non-traditional Logics
| 10:30 | On the computation of conditioning in weighted belief bases (abstract) |
| 11:00 | Embedding Intuitionistic into Classical Logic (abstract) |
| 11:30 | Counterfactuals Modulo Temporal Logics (abstract) PRESENTER: Julian Siber |
| 12:00 | LDL: the Logic of Differentiable Logics (abstract) |
Lunch (provided at a restuarant)
Farewell Banquet - Hotel Resort del café by Varuna, Chinchiná-La Manuela (passwd "resort')