FLOC 2022: FEDERATED LOGIC CONFERENCE 2022
PROGRAM

Days: Sunday, July 31st Monday, August 1st Tuesday, August 2nd Wednesday, August 3rd Thursday, August 4th Friday, August 5th Saturday, August 6th Sunday, August 7th Monday, August 8th Tuesday, August 9th Wednesday, August 10th Thursday, August 11th Friday, August 12th

Sunday, July 31st

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 1A (BCORE)
Location: Ullmann 308
09:00
Tutorial: Belief Change, Ontology Repair and Evolution (Part 1) (abstract)
09:00-10:00 Session 1B (DECFOML)
Location: Ullmann 104
09:00
Decidability Questions beyond Satisfiability for First-order Modal Logics (abstract)
09:00-10:30 Session 1C: DatalogMTL tutorial, part 1/2 (DatalogMTL)

Tutorial on DatalogMTL (https://datalogmtl.github.io/), part 1/2: motivations, introduction to DatalogMTL, and explanation of reasoning techniques.

Location: Ullmann 300
09:00
DatalogMTL (abstract)
09:00-10:30 Session 1D (FoMLAS)

FoMLAS Session 1

Chair:
Location: Ullmann 201
09:00
Why Robust Natural Language Understanding is a Challenge (abstract)
PRESENTER: Marco Casadio
09:30
An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (abstract)
PRESENTER: Matan Ostrovsky
10:00
Neural Networks in Imandra: Matrix Representation as a Verification Choice (abstract)
PRESENTER: Remi Desmartin
09:00-10:30 Session 1E (IFIP-WG1.6)
Location: Ullmann 306
09:00
Inversion and Determinization in Term Rewriting (abstract)
10:00
RLooP (the Rewriting List of open Problems)
09:00-10:30 Session 1F (LogTeach)
Location: Ullmann 301
09:00
Why and how to teach logic for CS undergraduates
10:00
How to teach logic for CS-undergraduate? Step-by-step! (abstract)
09:00-09:40 Session 1G: Invited talk -- dr. Ruth Hoffmann (ModRef)
Location: Ullmann 310
09:00
Constraint modelling and solving: Learning from observing people (abstract)
09:00-09:50 Session 1I (VardiFest)
Location: Taub 1
09:00
On the unusual effectiveness of automata in logic (abstract)
09:00-10:30 Session 1J (WiL)
Location: Ullmann 307
09:00
Embedding Quantitative Properties of Call-by-Name and Call-by-Value into Call-by-Push-Value (abstract)
10:00
The essence of type-theoretic elaboration (abstract)
09:00-10:30 Session 1K (XLoKR)

XLoKR Session 1

Location: Ullmann 202
09:00
Invited Talk: Explaining and Arguing with Facts and Rules (abstract)
10:00
Using Abstraction for Interpretable Robot Programs in Stochastic Domains (abstract)
PRESENTER: Till Hofmann
09:15-10:30 Session 2: Teaching logic (FOMEO)

5 talks, each roughly 10 minutes plus 5 minutes for discussion and questions.

Location: Ullmann 205
09:15
First-Order Logic Workbook (abstract)
PRESENTER: Ján Kľuka
09:30
Towards Graphical Feedback in the DiMo Learning Tool (abstract)
PRESENTER: Maurice Herwig
09:45
Iltis: Teaching Logic in the Web (abstract)
10:00
Experiences on Online Teaching of Formal Methods to Systems Engineering Students (abstract)
10:15
DOMtutor -- Competitive Programming as Teaching Tool (abstract)
09:30-10:30 Session 3A (ASL)

Keynote Talk 1

Location: (virtual only)
09:30
Exact Separation Logic (abstract)
09:30-10:30 Session 3B: Invited Talk (WPTE)
Location: Ullmann 305
09:30
Transforming Text to (and from) XML (abstract)
09:40-10:30 Session 4: Paper presentations (ModRef)
Location: Ullmann 310
09:40
Solving XCSP3 constraint problems using tools from software verification (abstract)
10:05
Constraint-based Part-of-Speech Tagging (abstract)
09:50-10:30 Session 5 (VardiFest)
Location: Taub 1
09:50
Data Path Queries over Embedded Graph Databases (abstract)
10:00
LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work (abstract)
10:10
Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (abstract)
10:20
SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces (abstract)
10:00-10:30 Session 6 (DECFOML)
Location: Ullmann 104
10:00
Are Bundles Good Deals for FOML? (abstract)
10:30-11:00Coffee Break
10:30-12:00 Session 7 (ASL)

Theories of Separation

Location: (virtual only)
10:30
Two Results on Separation Logic With Theory Reasoning (abstract)
PRESENTER: Nicolas Peltier
11:00
Labelled Tableaux for Linear Time Bunched Implication Logic (abstract)
PRESENTER: Daniel Mery
11:30
On the Expressiveness of a Logic of Separated Relations (abstract)
PRESENTER: Radu Iosif
10:45-12:30 Session 9: Extensions of ASP (ASPOCP)

Extensions of ASP

Location: Ullmann 311
10:45
Constrained Default Logic Programming (abstract)
PRESENTER: Shutao Zhang
11:05
On the generalization of learnt constraints in ASP solving for temporal domains (abstract)
PRESENTER: Klaus Strauch
11:25
Conflict Handling in Product Configuration using Answer Set Programming (abstract)
PRESENTER: Konstantin Herud
11:45
Hard Variants of Stable Marriage Problems: An Empirical Comparison of ASP with Other Computing Paradigms
11:00-12:30 Session 10A (BCORE)
Location: Ullmann 308
11:00
Tutorial: Belief Change, Ontology Repair and Evolution (Part 2) (abstract)
11:00-12:00 Session 10B (DECFOML)
Location: Ullmann 104
11:00
Terminating sequent calculi for decidable fragments of FOML (abstract)
11:00-12:30 Session 10C: DatalogMTL tutorial, part 2/2 (DatalogMTL)

Tutorial on DatalogMTL (https://datalogmtl.github.io/), part 2/2: reasoning systems (MeTeoR and Ontop), demos, and conclusions.

Location: Ullmann 300
11:00
DatalogMTL (abstract)
11:00-12:30 Session 10D: Teaching formal methods (FOMEO)

5 talks, each roughly 10 minutes plus 5 minutes for discussion and questions.

In the end, we have an additional 15 minutes for discussion, talks running a bit longer or getting to the buffet early.

We kindly ask presenters from the first two sessions to be in the gather in the final 15 minutes so that remote participants can ask questions and discuss with them.

Location: Ullmann 205
11:00
Tableaunoir: an online blackboard for teaching formal methods and making slides (abstract)
11:15
Teaching Concurrency with pseuCo Book (abstract)
11:30
Teaching Formal Languages with Iltis - A Preview (abstract)
11:45
Automata Tutor (abstract)
12:00
Visualization of structural operational semantics over programs of simple imperative language. (abstract)
PRESENTER: Ján Perháč
11:00-12:30 Session 10E (FoMLAS)

FoMLAS Session 2

Chair:
Location: Ullmann 201
11:00
Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations (abstract)
PRESENTER: Jianglin Lan
11:30
A Cascade of Checkers for Run-time Certification of Local Robustness (abstract)
PRESENTER: Ravi Mangal
12:00
RoMA: a Method for Neural Network Robustness Measurement and Assessment (abstract)
PRESENTER: Natan Levy
11:00-12:30 Session 10F (HoTT/UF)
Location: Ullmann 303
11:00
TBA
12:00
Elementary Simplicial Collapses in Cubical Agda
11:00-12:30 Session 10H: learning interpretable ML models (LMML)
Location: Ullmann 101
11:00
Building Optimal Decision Trees (abstract)
11:45
SAT-Based Induction of Explainable Decision Trees (abstract)
11:00-12:30 Session 10I (LogTeach)
Location: Ullmann 301
11:00
Position Paper: Mathematical Logic through Python (abstract)
PRESENTER: Noam Nisan
12:00
Whom to teach logic? (abstract)
11:00-12:30 Session 10J: Paper presentations (ModRef)
Location: Ullmann 310
11:00
A portfolio-based analysis method for competition results (abstract)
11:25
Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract) (abstract)
PRESENTER: Emilio Gamba
11:50
Automatic Generation of Dominance Breaking Nogoods for Constraint Optimization (abstract)
PRESENTER: Allen Z. Zhong
11:00-12:30 Session 10K (PCCR)
Location: Ullmann 203
11:00
Parameterized Approximations and CSPs (abstract)
12:00
Kemeny Rank Aggregation: Width Measure and Diversity Notion (abstract)
11:00-11:30 Session 10L (VardiFest)
Location: Taub 1
11:00
Formal Aspects of Strategic Reasoning in MAS (abstract)
11:10
Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic (abstract)
PRESENTER: Stefan Leue
11:20
Modelling with Reconfigurable Communication Interfaces (abstract)
11:00-12:30 Session 10M: Talks (1) (WPTE)
Chair:
Location: Ullmann 305
11:00
Program Equivalence in a Typed Probabilistic Call-by-Need Functional Language (abstract)
PRESENTER: David Sabel
11:30
A Machine-Checked Formalisation of Erlang Modules (abstract)
PRESENTER: Péter Bereczky
12:00
Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems (abstract)
PRESENTER: Kasper Hagens
11:00-12:30 Session 10N (WiL)
Location: Ullmann 307
11:00
Monoidal Width -- Extended Abstract (abstract)
PRESENTER: Elena Di Lavore
11:20
Hypertrace Logic (abstract)
11:40
A goal-oriented proof system for epistemic modal logic (abstract)
12:00
A Mixed Linear and Graded Logic-Extended Abstract (abstract)
PRESENTER: Victoria Vollmer
11:00-12:30 Session 10P (XLoKR)

XLoKR Session 2

Location: Ullmann 202
11:00
Explaining Description Logic Entailments in Practice with Evee and Evonne (abstract)
PRESENTER: Stefan Borgwardt
11:20
Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract) (abstract)
PRESENTER: Stefan Borgwardt
11:40
An API for DL Abduction Solvers (abstract)
12:00
Modular Provenance in Multi-Context Systems (abstract)
PRESENTER: Matthias Knorr
11:35-12:05 Session 11 (VardiFest)
Location: Taub 1
11:35
On the Extraordinary Effectiveness of Logic in Strategic Reasoning (abstract)
11:45
Automated Synthesis of Mechanisms (abstract)
11:55
Synthesis of plans for teams of manufacturing robots (abstract)
12:10-12:40 Session 12A (DECFOML)
Location: Ullmann 104
12:10
The Quantified Reflection Calculus as a Modal Logic (abstract)
12:10-12:40 Session 12B (VardiFest)
Location: Taub 1
12:10
That's All I know: On the Effectiveness of Logic in Game Theory (abstract)
12:20
Between Determinism and Nondeterminism (abstract)
12:30
A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (abstract)
12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

12:30-12:40 Session 13: Spotlight talks (LMML)
Location: Ullmann 101
12:30
MCP: Capturing Big Data by Satisfiability (abstract)
PRESENTER: Miki Hermann
14:00-15:00 Session 14A (ASL)

Keynote Talk 2

Location: (virtual only)
14:00
Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris (abstract)
14:00-15:30 Session 14B: Counting/Probabilistic ASP & Synthesis (ASPOCP)

Counting/Probabilistic ASP & Synthesis

Location: Ullmann 311
14:00
A Semantics For Probabilistic Answer Set Programs With Incomplete Stochastic Knowledge (abstract)
PRESENTER: David Tuckey
14:20
plingo: A system for probabilistic reasoning in clingo based on lpmln (abstract)
PRESENTER: Nicolas Ruehling
14:40
Automatic Synthesis of Boolean Networks from Biological Knowledge and Data (abstract)
15:00
ASP in Industry, here and there (abstract)
14:00-15:30 Session 14C (CHANGE)

This is a KR-2022 tutorial on Sunday July 31st: two 1.5h sessions in afternoon with a break: 14:00-15:30 and 16:00-17:30. See details at  https://www.cs.ryerson.ca/~mes/HTSC-Tutorial-KR2022/

Location: Ullmann 200
14:00
Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (abstract)
14:00-14:30 Session 14D (DECFOML)
Location: Ullmann 104
14:00
Forward Guarded Fragment: A tamed higher-arity extension of ALC (abstract)
14:00-15:00 Session 14E: Teaching proofs (FOMEO)

4 talks, each roughly 10 minutes plus 5 minutes for discussion and questions.

We kindly ask presenters of this session to be in the gather after 15:00 so that remote participants can ask questions and discuss with them.

Location: Ullmann 205
14:00
LogInd, a tool for supporting students in mastering structural induction (abstract)
PRESENTER: Josje Lodder
14:15
Prooffold: a prototype for displaying structured proofs (abstract)
14:30
Formal Methods Online: Sequent Calculus Verifier (SeCaV) (abstract)
14:45
SIVA: Simulation and visualization of the DL tableau algorithm (abstract)
14:00-15:30 Session 14F (FoMLAS)

FoMLAS Session 3

Chair:
Location: Ullmann 201
14:00
VNN-COMP 2022 (abstract)
PRESENTER: Mark Müller
14:00-15:30 Session 14G (HoTT/UF)
Location: Ullmann 303
14:00
Towards computing cohomology of dependent abelian groups
14:30
A Library of Monoidal Categories for Display and Univalence
PRESENTER: Kobe Wullaert
15:00
The internal AB axioms
14:00-15:30 Session 14H: computation of explanations for black-box ML models (LMML)
Location: Ullmann 101
14:00
A Rate-Distortion Framework for Explaining Model Decisions and Application to CartoonX (abstract)
14:45
The Exciting Theory of Formal Explanations (abstract)
14:00-15:30 Session 14I (LogTeach)
Location: Ullmann 301
14:00
Undergraduate Logic Teaching in Computing: Why, What, How? (abstract)
15:00
Introducing Logic by Stealth to Computer Science Students (abstract)
PRESENTER: Liam O'Reilly
14:00-14:40 Session 14J: Invited talk -- dr. Nguyen Dang (ModRef)
Location: Ullmann 310
14:00
A Constraint-Based Tool for Generating Benchmark Instances (abstract)
14:00-15:30 Session 14K (PC)
Location: Ullmann 309
14:00
Towards higher order proof complexity (abstract)
PRESENTER: Anupam Das
14:30
Proof complexity of CSP (abstract)
15:00
Proof complexity of natural formulas via communication arguments (abstract)
PRESENTER: Dmitry Itsykson
14:00-15:30 Session 14L (PCCR)
Location: Ullmann 203
14:00
Resolving Inconsistency of Linear Equations (abstract)
14:30
Towards Tractable QSAT for Structural Parameters Below Treewidth (abstract)
15:00
Learning Small Decision Trees (abstract)
14:00-15:30 Session 14P: Talks (2) (WPTE)
Location: Ullmann 305
14:00
On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting (abstract)
PRESENTER: Naoki Nishida
14:30
On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs (abstract)
PRESENTER: Shujun Zhang
15:00
On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms (abstract)
PRESENTER: Naoki Nishida
14:00-15:30 Session 14Q (WiL)
Location: Ullmann 307
14:00
A normalized edit distance on finite and infinite words (abstract)
15:00
Automated Logic-Based Reasoning for Analyzing Prime Video Code (abstract)
14:00-15:30 Session 14R (XLoKR)

XLoKR Session 3

Location: Ullmann 202
14:00
On interactive explanations as reasoning (abstract)
14:20
Should counterfactual explanations always be data instances? (abstract)
PRESENTER: Francesca Toni
14:40
Dialogue-Based Explanations of Reasoning in Rule-based Systems (abstract)
PRESENTER: Joe Collenette
15:00
Clustering-Based Approaches for Symbolic Knowledge Extraction (abstract)
PRESENTER: Roberta Calegari
14:30-15:30 Session 15A (DECFOML)
Location: Ullmann 104
14:30
From Modal Logic to Fluted logic (abstract)
14:30-15:30 Session 15B (TLLA-LINEARITY)
Location: Ullmann 302
14:30
Recursive Session Logical Relations (abstract)
14:50-15:30 Session 17 (VardiFest)
Location: Taub 1
14:50
Automata-Based Quantitative Reasoning (abstract)
15:00
LTLf Synthesis Under Environment Specifications (abstract)
15:10
Boolean Synthesis via Decision Diagrams (abstract)
15:20
Strategy synthesis for Global Window PCTL (abstract)
PRESENTER: Shibashis Guha
15:00-16:30 Session 18 (ASL)

Heaps and Concurrency

Location: (virtual only)
15:00
Proving Logical Atomicity using Lock Invariants (abstract)
PRESENTER: Shengyi Wang
15:30
Deciding Separation Logic with Heap Lists (abstract)
16:00
Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection (abstract)
PRESENTER: Alexandre Moine
15:30-16:00Coffee Break
16:00-17:30 Session 19A: Modelling and Applications (ASPOCP)

Modelling and Applications

Location: Ullmann 311
16:00
Computing H-Partitions in ASP and Datalog (abstract)
PRESENTER: Nicolas Lecomte
16:20
Translating Definitions into the Language of Logic Programming: A Case Study (abstract)
16:40
A normative model of explanation for binary classification legal AI and its implementation on causal explanations of Answer Set Programming (abstract)
17:00
Assumable Answer Set Programming (abstract)
16:00-17:30 Session 19B (CHANGE)

This is a KR-2022 tutorial on Sunday July 31st: two 1.5h sessions in afternoon with a break: 14:00-15:30 and 16:00-17:30

Location: Ullmann 200
16:00
Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (abstract)
16:00-16:30 Session 19C (DECFOML)
Location: Ullmann 104
16:00
Decidable Fragments of Term Modal Logic (abstract)
16:00-17:00 Session 19D (FoMLAS)

FoMLAS Session 4

Location: Ullmann 201
16:00
Counter-Example Guided Neural Network Compression Refinement (CEG4N) (abstract)
16:30
Goal-Aware RSS for Complex Scenarios via Program Logic (abstract)
16:00-17:30 Session 19E (HoTT/UF)
Location: Ullmann 303
16:00
Internal languages of diagrams of ∞-toposes (abstract)
17:00
An Experiment with 2LTT Features in Agda
16:00-17:30 Session 19F (IFIP-WG1.6)

Business Meeting (IFIP-WG 1.6)

Location: Ullmann 306
16:00-17:30 Session 19G: verification of black-box ML models (LMML)
Location: Ullmann 101
16:00
Verification of Binarized Neural Networks: Challenges and Opportunities (abstract)
16:45
Verification of Realistic Neural Networks (abstract)
16:00-17:30 Session 19H (LogTeach)
Location: Ullmann 301
16:00
Logic for CS Undergraduates: A Sketch (abstract)
16:30
Logic for Students of Modern Artificial Intelligence (abstract)
16:00-17:30 Session 19I (PC)
Location: Ullmann 309
16:00
Strong proof systems based on algebraic circuits (abstract)
17:00
On combinatorial principles coming from semi-algebraic proof systems
16:00-17:00 Session 19J (PCCR)
Location: Ullmann 203
16:00
The Tournament Fixing Problem (abstract)
16:00-17:30 Session 19K (TLLA-LINEARITY)
Location: Ullmann 302
16:00
Copromotion and Taylor Approximation (Work in Progress) (abstract)
PRESENTER: Jean-Simon Lemay
16:30
Denotational semantics driven simplicial homology? (abstract)
17:00
Bottom-Up Sequentialization of Unit-Free MALL Proof Nets (abstract)
PRESENTER: Rémi Di Guardia
16:00-16:40 Session 19L (VardiFest)
Location: Taub 1
16:00
Logic and Languages for Representation Learning (abstract)
16:10
Natural Autoencoding (abstract)
PRESENTER: Assaf Marron
16:20
From Logic to Neurosymbolic AI (abstract)
16:30
An Epistemic Logic for modelling Cooperative Agents (abstract)
16:00-17:30 Session 19M: Talks (3) (WPTE)
Location: Ullmann 305
16:00
Towards Corecursion Without Corecursion in Coq (abstract)
PRESENTER: Vlad Rusu
16:30
Towards a Refactoring Tool for Dependently-Typed Programs (work in progress) (abstract)
16:45
Refactoring Steps for P4 (work in progress) (abstract)
PRESENTER: Máté Tejfel
16:00-17:00 Session 19N (WiL)
Location: Ullmann 307
16:00
Fixed-Template Promise Model Checking Problems (abstract)
PRESENTER: Silvia Butti
16:20
Two Dimensional Bounded Model Checking for Unbounded Client-Server Systems (abstract)
PRESENTER: Tephilla Prince
16:40
A note on Türing 1936 (abstract)
16:00-18:00 Session 19P (XLoKR)

XLoKR Session 4

Location: Ullmann 202
16:00
Invited Talk: Explanation Generation in Applications of Answer Set Programming (abstract)
17:00
Explaining Soft-Goal Conflicts through Constraint Relaxations (abstract)
PRESENTER: Rebecca Eifler
17:20
Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract) (abstract)
PRESENTER: Ignace Bleukx
16:45-17:05 Session 20 (VardiFest)
Location: Taub 1
16:45
On the Effectiveness of Logic in Algorithmic Graph Theory (abstract)
16:55
Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982) (abstract)
17:00-17:30 Session 21A (ASL)

Report on SL-COMP

Chair:
Location: (virtual only)
17:00
Report on SL-COMP
17:10-18:00 Session 22 (VardiFest)

Invited Talk by Orna Kupferman

Location: Taub 1
17:10
On how the past illuminates the future (abstract)
17:30-18:30 Session 24A: CAUSAL and EELP (ASPOCP)

CAUSAL and EELP

Location: Ullmann 311
17:30
Correct Causal Inference in Probabilistic Logic Programming
17:50
A Casual Perspective on AI Deception
18:10
Epistemic Logic Programs: a Novel Perspective and some Extensions
17:30-19:00 Session 24C (LogTeach)
Location: Ullmann 301
17:30
The Herbrand Manifesto: Thinking Inside the Box (abstract)
PRESENTER: Vinay Chaudhri
18:30
Teaching logic to CS undergraduates (abstract)
PRESENTER: Thomas Zeume
Monday, August 1st

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 26A (FoMLAS)

FoMLAS Session 5

Location: Ullmann 201
09:00
Scalable Verification of GNN-based Job Schedulers (abstract)
PRESENTER: Haoze Wu
09:30
VPN: Verification of Poisoning in Neural Networks (abstract)
PRESENTER: Youcheng Sun
10:00
Verification-Aided Deep Ensemble Selection (abstract)
PRESENTER: Guy Amir
09:00-10:30 Session 26B: Foundations (GDE)

Welcome ceremony to the 2nd workshop on Goal-directed Execution of Answer Set Programs (GDE 2022) followed by a tutorial (40 minutes) and two talks, each roughly 20 minutes plus 5 minutes for discussion and questions.

Location: Ullmann 310
09:00
Tutorial: Automating Commonsense Reasoning (abstract)
09:40
A Query Evaluation Method for ASP with Abduction (abstract)
10:05
First order logic and commonsense reasoning: a path less travelled (abstract)
PRESENTER: Tanel Tammet
09:00-10:30 Session 26C: Confluence criteria and completeness (IWC)
Location: Ullmann 306
09:00
Development Closed Critical Pairs: Towards a Formalized Proof (abstract)
PRESENTER: Aart Middeldorp
09:30
On Confluence of Parallel-Innermost Term Rewriting (abstract)
PRESENTER: Carsten Fuhs
10:00
Uniform Completeness (abstract)
09:00-10:30 Session 26D (LogTeach)
Location: Ullmann 301
09:00
Teaching Logic (abstract)
10:00
Logic for computer science: starting earlier, at school (abstract)
09:00-10:30 Session 26E: Joint QBF Session (PC and QBF)
Location: Ullmann 309
09:00
QBF Solvers and their Proof Systems (abstract)
10:00
QCDCL with Cube Learning or Pure Literal Elimination – What is best? (abstract)
PRESENTER: Benjamin Böhm
09:00-10:30 Session 26F (PCCR)
Location: Ullmann 203
09:00
Parameterized algorithmics in access control: linking theory and practice (abstract)
10:00
MaxSAT: Parameterized, Parallel, Absolute (abstract)
09:00-10:30 Session 26G: Applications (POS)
Location: Ullmann 311
09:00
Towards an Efficient CNF Encoding of Block Ciphers (abstract)
09:30
Calculating Sufficient Reasons for Random Forest Classifiers (abstract)
10:00
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification (abstract)
PRESENTER: Jakob Nordstrom
09:00-10:30 Session 26H: Joint PC/QBF Session (QBF)

This session will be held jointly with the Proof Complexity (PC) Workshop.

Location: Ullmann 309
09:00
QBF Solvers and their Proof Systems (abstract)
09:00-10:30 Session 26I: Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22, Part I) (REAI)

Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22, Part I)

Location: Ullmann 102
09:00
Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22 https://cs.uwaterloo.ca/~david/kr22/) (abstract)
09:00-10:30 Session 26J (TERMGRAPH)

Invited Talk by Delia Kesner

Location: Ullmann 101
09:00
A Computational Interpretation of Girard’s Intuitionistic Proof-Nets (abstract)
09:00-09:50 Session 26K (VardiFest)
Location: Taub 1
09:00
On the Effectiveness of Logic in Robotics (abstract)
09:00-10:30 Session 26L: Doctoral Program (CP)
Location: Taub 4
09:00
Opening
09:05
Industrial Research Career Path as a Sequence of Constraint Satisfaction Problems
10:00
Solving the Non-Crossing MAPF for non point-sized robots (abstract)
PRESENTER: Xiao Peng
10:20
Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (abstract)
PRESENTER: Louis Popovic
10:23
Extended Abstract: Sequence Variables for Routing Problems (abstract)
10:26
Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (abstract)
PRESENTER: Daphné Lafleur
09:15-10:30 Session 27 (Mentoring Workshop)
Location: Taub 7
09:15
Welcome
09:30
Advancing Science with Platforms and Driving Scenarios: a perspective from a researcher at Microsoft Research (abstract)
09:30-10:30 Session 28A (LFMTP)

Invited talk

Location: Taub 3
09:30
Metatheory of Proto-Quipper in Hybrid: Context Relations Revisited (abstract)
09:30-10:30 Session 28B (PLP)

Invited talk: Alexander Artikis & Periklis Mantenogloy (University of Piraeus, Greece) - 

Online Reasoning under Uncertainty with the Event Calculus

Location: Ullmann 305
09:30
Online Reasoning under Uncertainty with the Event Calculus (abstract)
09:50-10:30 Session 29 (VardiFest)
Location: Taub 1
09:50
The Safety Fragment of LTL (abstract)
PRESENTER: Nicola Gigante
10:00
An Automata-Theoretic Approach to Model-Free Reinforcement Learning (abstract)
PRESENTER: Mateo Perez
10:10
Strategy Logic: Origin, Results, and Open Questions (abstract)
10:20
Rewriting of Regular Path Queries: The first paper of the four Italians (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 31A (FoMLAS)

FoMLAS Session 6

Chair:
Location: Ullmann 201
11:00
Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract) (abstract)
PRESENTER: Doron Peled
11:30
Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (abstract)
PRESENTER: Luca Arnaboldi
12:00
Differentiable Logics for Neural Network Verification (abstract)
PRESENTER: Natalia Ślusarz
11:00-12:30 Session 31B: Modelling with s(CASP) (GDE)

Session focused on the use of s(CASP) for modeling: 3 regular talks (20 minutes presentation) and a short talk (10 minutes presentation) plus 5 minutes of Q&A each one.

Location: Ullmann 310
11:00
Integration of Logical English and s(CASP) (abstract)
PRESENTER: Galileo Sartor
11:25
Embedding s(CASP) in Prolog (abstract)
PRESENTER: Jan Wielemaker
11:50
Modeling Administrative Discretion Using Goal-Directed Answer Set Programming (abstract)
PRESENTER: Joaquin Arias
12:15
An s(CASP) In-Browser Playground based on Ciao Prolog (abstract)
PRESENTER: Jose F. Morales
11:00-12:30 Session 31C (HoTT/UF)
Location: Ullmann 303
11:00
Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
11:30
Towards Directed Higher Observational Type Theory
12:00
The Compatibility of MF with HoTT
PRESENTER: Michele Contente
11:00-12:30 Session 31D: Invited talk and equivalence (IWC)
Location: Ullmann 306
11:00
Seven Confluence Criteria for Solving COPS #20 (abstract)
12:00
Formalized Signature Extension Results for Equivalence (abstract)
11:00-12:30 Session 31E (LFMTP)

Workshop papers

Location: Taub 3
11:00
A positive perspective on term representation: work in progress (abstract)
PRESENTER: Jui-Hsuan Wu
11:45
An Implementation of Set Theory with Pointed Graphs in Dedukti (abstract)
11:00-12:30 Session 31F (LogTeach)
Location: Ullmann 301
11:00
What Should Students of a Course in Logic Know at Its End? (abstract)
12:00
My Experience Teaching Logic in Undergraduate AI at NYU} (abstract)
11:00-12:30 Session 31G (Mentoring Workshop)
Location: Taub 7
11:00
Managing a life that also includes research (abstract)
11:45
How logic-based approaches can be used in data management
11:00-12:30 Session 31H: Joint QBF Session (PC)
Location: Ullmann 309
11:00
Strategy Extraction and Proof
12:00
QCDCL with Cube Learning or Pure Literal Elimination – What is best? (II)
11:00-12:30 Session 31I (PCCR)
Location: Ullmann 203
11:00
The Parameterized Complexity of SAT (abstract)
12:00
Parameterized Algorithmics and Counting: Treewidth in Practice (abstract)
11:00-12:30 Session 31J (PLP)
Location: Ullmann 305
11:00
On Projectivity in Markov Logic Networks (abstract)
PRESENTER: Sagar Malhotra
11:30
Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming (abstract)
11:00-12:30 Session 31K: SAT and Parallel Solving (POS)
Location: Ullmann 311
11:00
Dinosat: A SAT Solver with Native DNF Support (abstract)
PRESENTER: Markus Iser
11:30
DPS: A Framework for Deterministic Parallel SAT Solvers (abstract)
12:00
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (abstract)
PRESENTER: Armin Biere
11:00-12:30 Session 31L: Joint PC/QBF Session (QBF)

This session will be held jointly with the Proof Complexity (PC) Workshop.

Location: Ullmann 309
11:00
Strategy Extraction and Proof (abstract)
12:00
QCDCL with Cube Learning or Pure Literal Elimination - Part 2 (abstract)
11:00-12:30 Session 31M: Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22, Part II) (REAI)

Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22, Part II)

Location: Ullmann 102
11:00
Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22) (abstract)
11:00-12:30 Session 31N (TERMGRAPH)

Regular submissions, morning session

Location: Ullmann 101
11:00
Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star (abstract)
11:30
Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting (abstract)
12:00
A PBPO+ Graph Rewriting Tutorial (abstract)
PRESENTER: Roy Overbeek
11:00-12:30 Session 31P (TLLA-LINEARITY)
Location: Ullmann 302
11:00
Dissymetrical Linear Logic (abstract)
11:30
Parametric Chu Translation (abstract)
12:00
Peano Arithmetic and muMALL: An extended abstract (abstract)
PRESENTER: Dale Miller
11:00-11:30 Session 31Q (VardiFest)
Location: Taub 1
11:00
Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (abstract)
11:10
Bisimulation Games Played in Fibered Categories (abstract)
11:20
Capturing abscondings (abstract)
11:00-12:30 Session 31R: Doctoral Program (CP)
Location: Taub 4
11:00
Interdisciplinary Research -- Cost Function Network for Life Sciences
11:55
Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (abstract)
PRESENTER: Marco Dalla
12:15
Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (abstract)
12:18
Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (abstract)
PRESENTER: Isaac Rudich
12:21
Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (abstract)
PRESENTER: Vianney Coppé
12:24
CNF Encodings of Binary Constraint Trees (Extended Abstract) (abstract)
PRESENTER: Ruiwei Wang
11:35-12:05 Session 32 (VardiFest)
Location: Taub 1
11:35
From Kochen-Specker to Feder-Vardi (abstract)
11:45
Data Complexity and Expressive Power of Ontological Reasoning Formalisms (abstract)
11:55
Logic-driven approaches for smart, safe and energy-efficient aviation (abstract)
12:10-12:40 Session 33 (VardiFest)
Location: Taub 1
12:10
Divide-and-Conquer Determinization for B\"uchi Automata (abstract)
12:20
Little Tricky Logic: Misconceptions in the Understanding of LTL (abstract)
PRESENTER: Ben Greenman
12:30
Comments from Giuseppe, Kuldeep, and Kristin
12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:30 Session 34A (ABR)

Tutorial: Assumption-Based Nonmonotonic Reasoning - Alexander Bochman

Location: Ullmann 104
Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 1) (abstract)
14:00-15:30 Session 34B (FoMLAS)

FoMLAS Session 7

Location: Ullmann 201
14:00
Neural Network Verification with Proof Production (abstract)
PRESENTER: Omri Isac
14:30
Efficient Neural Network Verification using Branch and Bound (abstract)
14:00-15:30 Session 34C: s(CASP) extensions and applications I (GDE)

Session focused on the most recent applications of s(CASP) and the description of the functionalities incorporated in s(CASP) that have made them possible: 3 regular talks (20 minutes presentation) and a short talk (10 minutes presentation) plus 5 minutes of Q&A each one.

Location: Ullmann 310
14:00
Automating Defeasible Reasoning in Law with Answer Set Programming (abstract)
PRESENTER: Avishkar Mahajan
14:25
Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming (abstract)
14:50
Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy (abstract)
PRESENTER: Elmer Salazar
15:15
LTL Model Checking using Coinductive Answer Set programming (abstract)
14:00-15:30 Session 34D (HoTT/UF)
Location: Ullmann 303
14:00
TBA
15:00
Semantics for two-dimensional type theory
PRESENTER: Benedikt Ahrens
14:00-15:30 Session 34E: Conditional rewriting (IWC)
Location: Ullmann 306
14:00
On local confluence of conditional rewrite systems (abstract)
14:30
A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems (abstract)
PRESENTER: Takahito Aoto
15:00
Proving Confluence with CONFident (abstract)
PRESENTER: Raúl Gutiérrez
14:00-15:00 Session 34F (LFMTP)

Frank Pfenning special session: invited talk

Location: Taub 3
14:00
A modal analysis of dependently typed metaprogramming (abstract)
14:00-15:30 Session 34G (LogTeach)
Location: Ullmann 301
14:00
Possible Desiderata for Logic in the CS Curriculum (abstract)
15:00
Teaching Logic for Computer Science Students: Proof Assistants and Related Tools (abstract)
14:00-15:30 Session 34H (Mentoring Workshop)
Location: Taub 7
14:00
Navigating through the academic jungle (abstract)
14:45
From PhD to industry: A recent graduate’s perspective (abstract)
14:00-15:30 Session 34I (PC)
Location: Ullmann 309
14:00
Hard Inputs from Kolmogorov Randomness---Can Merlin Tame Open Problems? (abstract)
14:30
Simulations between proof systems (abstract)
15:00
Are Hitting Formulas Hard for Resolution? (abstract)
PRESENTER: Tomáš Peitl
14:00-15:30 Session 34J (PCCR)
Location: Ullmann 203
14:00
Decompositions and algorithms for interpretations of sparse graphs (abstract)
15:00
Tractable Abstract Argumentation via Backdoor-Treewidth (abstract)
PRESENTER: Matthias König
14:00-15:30 Session 34K (PLP)
Location: Ullmann 305
14:00
Semantics for Hybrid Probabilistic Logic Programs with Function Symbols: Technical Summary (abstract)
PRESENTER: Fabrizio Riguzzi
14:30
Statistical Statements in Probabilistic Logic Programming (abstract)
PRESENTER: Fabrizio Riguzzi
14:00-15:30 Session 34L: Proofs I (POS)
Location: Ullmann 311
14:00
TBUDDY: A Proof-Generating BDD Package (abstract)
14:30
Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (abstract)
PRESENTER: Mate Soos
15:00
Towards the shortest DRAT proof of the Pigeonhole Principle (abstract)
PRESENTER: Marijn Heule
14:00-15:30 Session 34M (QBF)
Location: Ullmann 205
14:00
Moving Definition Variables in Quantified Boolean Formulas (Extended Abstract) (abstract)
PRESENTER: Joseph Reeves
14:30
Advances in Quantified Integer Programming (abstract)
15:00
A Data-Driven Approach for Boolean Functional Synthesis (abstract)
14:00-15:30 Session 34N (TERMGRAPH)

Invited talk by Jörg Endrullis

Location: Ullmann 101
14:00
PBPO+ Graph Rewriting in Context (abstract)
14:00-15:30 Session 34P (TLLA-LINEARITY)
Location: Ullmann 302
14:00
The Call-by-Value Lambda-Calculus from a Linear Logic Perspective (abstract)
15:00
Cloning and Deleting Quantum Information from a Linear Logical Point of View (abstract)
14:00-14:55 Session 34Q (VardiFest)
Location: Taub 1
14:00
Descriptive complexity and inexpressibly proofs (abstract)
14:25
A Brief Glimpse of the Skolem Landscape (abstract)
14:35
Approximations of Certain Answers in First-Order Logic (abstract)
14:45
Towards Algebraic Techniques for Descriptive Complexity (abstract)
14:00-15:30 Session 34R: Doctoral Program (CP)
Location: Taub 4
14:00
Aggressive Bound Descent for Constraint Optimization (abstract)
PRESENTER: Thibault Falque
14:20
Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (abstract)
PRESENTER: Auguste Burlats
14:40
Finding Counterfactual Explanations through Constraint Relaxations (abstract)
PRESENTER: Sharmi Dev Gupta
15:00
Symmetry breaking and Knowledge Compilation (abstract)
PRESENTER: Andrea Balogh
15:20
Improved Sample Complexity Bounds for Branch-and-Cut (abstract)
PRESENTER: Siddharth Prasad
15:23
Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (abstract)
PRESENTER: Allen Z. Zhong
15:26
Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (abstract)
PRESENTER: Jheisson López
15:00-15:30 Session 35A (LFMTP)

Frank Pfenning special session: contributed talks

Location: Taub 3
15:00
Associativity or Non-Associativity, Local or Global! (abstract)
PRESENTER: Eben Blaisdell
15:00-15:40 Session 35B (VardiFest)
Location: Taub 1
15:00
Fixpoint Logics, Relational Machines, and Computational Complexity (abstract)
15:10
To Count or Not to Count: A Personal Perspective (abstract)
15:20
Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration (abstract)
PRESENTER: Eli Singerman
15:30
A Toast for Moshe at the FLoC VardiFest (abstract)
15:30-16:00Coffee Break
16:00-17:30 Session 37A (ABR)

Tutorial: Assumption-Based Nonmonotonic Reasoning

Location: Ullmann 104
Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 2) (abstract)
16:00-17:00 Session 37B (FoMLAS)

FoMLAS Session 8

Location: Ullmann 201
16:00
Minimal Multi-Layer Modifications of Deep Neural Networks (abstract)
PRESENTER: Idan Refaeli
16:30
Self-Correcting Neural Networks For Safe Classification (abstract)
PRESENTER: Ravi Mangal
16:00-17:30 Session 37C: s(CAPS) extensions and applications II (GDE)

Session focused on the latest applications of s(CASP): 2 regular talks (20 minutes plus 5 minutes of Q&A), followed by a panel to discuss the present and future of goal-directed execution of answer set programs (40 minutes).

Location: Ullmann 310
16:00
Summary on "Hybrid Neuro-Symbolic Approach for Text-Based Games using Inductive Logic Programming" (abstract)
16:25
Blawx: Web-based user-friendly Rules as Code (abstract)
16:50
GDE of ASP: applications, potential and future directions (abstract)
16:00-17:30 Session 37D (HoTT/UF)
Location: Ullmann 303
16:00
Models of homotopy type theory from the Yoneda embedding
16:30
A type-theoretic model structure over cubes with one connection presenting spaces
PRESENTER: Evan Cavallo
17:00
Groupoidal Realizability: Formalizing the Topological BHK Interpretation
16:00-18:00 Session 37E: Higher-order rewriting and CoCo (IWC)
Location: Ullmann 306
16:00
Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus (abstract)
16:30
Checking Confluence of Rewrite Rules in Haskell (abstract)
17:00
Confluence Competition
16:00-17:00 Session 37F (LFMTP)

Frank Pfenning special session: invited talk

Location: Taub 3
16:00
Reasoning about Specifications in LF (abstract)
16:00-17:30 Session 37I (PC)
Location: Ullmann 309
16:00
On vanishing sums of roots of unity in polynomial calculus and sum-of-squares (abstract)
PRESENTER: Ilario Bonacina
17:00
Exponential separations using guarded extension variables (abstract)
PRESENTER: Emre Yolcu
16:00-17:00 Session 37J (PLP)
Location: Ullmann 305
16:00
Explainability, causality and computational and-or graphs (abstract)
16:00-17:00 Session 37K: Proofs II (POS)
Location: Ullmann 311
16:00
SATViz: Real-Time Visualization of Clausal Proofs (abstract)
PRESENTER: Tim Holzenkamp
16:30
Certified Symmetry and Dominance Breaking for Combinatorial Optimisation (abstract)
PRESENTER: Jakob Nordstrom
16:00-17:30 Session 37L (QBF)
Location: Ullmann 205
16:00
From QBF to the Dynamic Logic of Propositional Assignments and back: a computational perspective (abstract)
16:30
Lower Bounds for QBFs of Bounded Treewidth (abstract)
16:00-17:30 Session 37M (TERMGRAPH)

Regular papers, afternoon session, including discussion

Location: Ullmann 101
16:00
Formalization and analysis of BPMN using graph transformation systems (abstract)
PRESENTER: Tim Kräuter
16:30
Ideograph: A Language for Expressing and Manipulating Structured Data (abstract)
PRESENTER: Stephen Mell
16:00-16:40 Session 37Q (VardiFest)
Location: Taub 1
16:00
Understandable Proofs of Unsatisfiability (abstract)
16:10
Moshe Y. Vardi's First Love (abstract)
16:35
A Comment to Moshe by Ron Fagin
16:00-17:30 Session 37R: Doctoral Program (CP)
Location: Taub 4
16:00
Optimized Code Generation against Power Side Channels (abstract)
16:20
Boolean Functional Synthesis and its Applications (abstract)
PRESENTER: Priyanka Golia
16:40
On PB Encodings for Constraint Problems (abstract)
PRESENTER: Thibault Falque
17:00
A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (abstract)
PRESENTER: Ramiz Gindullin
17:20
Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (abstract)
PRESENTER: Alexander Ek
17:23
Extended Abstract: Constraint Acquisition Based on Solution Counting (abstract)
17:26
Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (abstract)
16:45-17:05 Session 38 (VardiFest)
Location: Taub 1
16:45
Verifying Accuracy Claims of Differential Privacy Algorithms (abstract)
16:55
Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst (abstract)
17:00-18:00 Session 39A (LFMTP)

Frank Pfenning special session: contributed talks

Location: Taub 3
17:00
A (Logical) Framework for Collaboration (abstract)
17:15
Type refinement as a unifying principle (abstract)
17:30
Language Minimalism and Logical Frameworks (abstract)
PRESENTER: Chris Martens
17:45
Logics for Robotics
17:00-18:00 Session 39B: Joint Session with Vardi-Fest (LogTeach)
Location: Taub 1
17:00
How to be an ethical computer scientist (Joint with Vardi Fest) (abstract)
17:10-18:00 Session 40 (VardiFest)
Location: Taub 1
17:10
How to be an ethical computer scientist (abstract)
18:30-20:00Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event
Tuesday, August 2nd

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 44A: ML (CP)
Location: Taub 7
09:00
Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation (abstract)
PRESENTER: Senne Berden
09:30
Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (abstract)
10:00
Improved Sample Complexity Bounds for Branch-and-Cut (abstract)
PRESENTER: Siddharth Prasad
09:00-10:30 Session 44B: Theory (CP)
Location: Taub 4
09:00
CSP Beyond Tractable Constraint Languages (abstract)
PRESENTER: Stefan Szeider
09:30
On Redundancy in Constraint Satisfaction Problems (abstract)
10:00
Fixed-Template Promise Model Checking Problems (abstract)
PRESENTER: Kristina Asimi
09:00-10:30 Session 44F: Temporal and Data Logic, Linear Recurrences and Equation Systems (LICS)

"Temporal and Data Logic, Linear Recurrences and Equation Systems": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
09:00
Temporal Team Semantics Revisited (abstract)
09:15
Deciding Hyperproperties Combined with Functional Specifications (abstract)
PRESENTER: Jana Hofmann
09:30
Reasoning on Data Words over Numeric Domains (abstract)
09:45
Solvability of orbit-finite systems of linear equations (abstract)
PRESENTER: Sławomir Lasota
10:00
Computing the Density of the Positivity Set for Linear Recurrence Sequences (abstract)
10:15
On the Skolem Problem and the Skolem Conjecture (abstract)
PRESENTER: James Worrell
09:00-10:30 Session 44G: QBF-1 (SAT)
09:00
Classes of Hard Formulas for QBF Resolution (abstract)
PRESENTER: Olaf Beyersdorff
09:30
Should decisions in QCDCL follow prefix order? (abstract)
PRESENTER: Benjamin Böhm
10:00
Changing Partitions in Rectangle Decision Lists (abstract)
09:15-10:15 Session 45A: FSCD Invited Speaker (FSCD)
09:15
Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting
09:15-10:30 Session 45B: Semantics (ICLP)
Location: Taub 9
09:15
Treewidth-aware Reductions of Normal ASP to SAT– Is Normal ASP Harder than SAT after All? (abstract)
09:30
Inference and Learning with Model Uncertainty in Probabilistic Logic Programs (abstract)
PRESENTER: Victor Verreet
09:45
Tractable Reasoning using Logic Programs with Intensional Concepts (abstract)
10:00
Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (abstract)
PRESENTER: Joaquin Arias
10:15
ApproxASP – A Scalable Approximate Answer Set Counter (abstract)
PRESENTER: Mohimenul Kabir
09:30-10:30 Session 46: Invited Talk (KR)
Location: Taub 2
09:30
Neuro-Symbolic Adventures on Commonsense Knowledge and Reasoning (abstract)
10:30-11:00Coffee Break
11:10-12:10 Session 48: Keynote (FLoC)
11:10
Information Structures for Privacy and Fairness (abstract)
12:10-12:40 Session 49B: Knowledge Graphs (KR)
Location: Taub 3
12:10
Open Relation Extraction With Non-existent and Multi-span Relationships (abstract)
PRESENTER: Huifan Yang
12:30-14:00Lunch Break

Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).

14:00-15:30 Session 50A: Tutorial (CP)
Chair:
Location: Taub 7
14:00
Solving with Provably Correct Results: Beyond Satisfiability, and Towards Constraint Programming (abstract)
PRESENTER: Ciaran McCreesh
14:00-15:30 Session 50B: Applications (CP)
Location: Taub 4
14:00
Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data (abstract)
14:30
A Constraint Programming Approach to Ship Refit Project Scheduling (abstract)
15:00
DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security (abstract)
PRESENTER: Timothy Curry
14:00-15:30 Session 50C: Semantics (FSCD)
14:00
A Fibrational Tale of Operational Logical Relations (abstract)
14:30
On Quantitative Algebraic Higher-Order Theories (abstract)
PRESENTER: Paolo Pistone
15:00
Sheaf semantics of termination-insensitive noninterference (abstract)
14:00-15:00 Session 50D: Invited talk by Theresa Swift: Two Languages, One System:Tightly Connecting XSB Prolog and Python (ICLP)

Two Languages, One System:Tightly Connecting XSB Prolog and Python

Abstract: Python, ranked first on the May 2022 Tiobe index, is a hugely popular language, heavily used in machine learning and other applications. Prolog, ranked twenty-first the May 2022 Tiobe index, while less popular has important reasoning and knowledge representation capabilities, particularly since modern Prologs support constraint-based reasoning, tabling-based deduction, and probabilistic inference. Despite their differences, Prolog and Python share important commonalities. First, both Prolog and CPython (the standard Python implementation) are written in C with well-developed interfaces to other C programs. In addition, both languages are dynamically typed with data structures that are recursively generated in just a few ways. Infact, nearly all core data structures of the two languages can be efficiently bi-translated, leading to a tight connection of the two systems. This talk presents the design, experience, and implications of such a connection using XSB Prolog version 5.0. The connection for XSB to call Python has led to XSB orchestrating commercial projects using interfaces to Elastic search, dense vector storage, nlp systems, Google maps, and to a 14.6 billion triple Wikidata graph. The connection for Python to call XSB allows XSB to be imported as any other Python module so that XSB can easily be invoked from Jupyter notebooks or other graphical interfaces. On a more speculative level, the talk mentions how this work might be leveraged for research in neuro-symbolic learning, natural language processing and cross-language type inference.

Location: Taub 9
14:00-15:30 Session 50E: Multi-Agent Systems (KR)
Location: Taub 2
14:00
Verification and Realizability in Finite-Horizon Multiagent Systems (abstract)
14:30
Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems (abstract)
15:00
Automatic Synthesis of Dynamic Norms for Multi-Agent Systems (abstract)
PRESENTER: Giuseppe Perelli
14:00-14:30 Session 50F: Doctoral Consortium (KR)
Location: Taub 3
14:00
Matthias König's Thesis: Graph Parameters for Abstract Argumentation
14:05
Impact of Logic Paradigms on Abstract Argumentation
14:10
Computational Aspects of Structured Argumentation
14:15
Do Humans Find Postulates of Belief Change Plausible?
14:20
A Conditional Perspective for Reasoning, Revision and Relevance
14:25
Deontic Logic for Epistemic Actions
14:00-15:30 Session 50G: Lambda Calculus, Quantum Programming, Games in Category Theory (LICS)

"Lambda Calculus, Quantum Programming, Games in Category Theory": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
14:00
Curry and Howard Meet Borel (abstract)
PRESENTER: Paolo Pistone
14:15
Resource approximation for the lambda-mu-calculus (abstract)
14:30
Graded Monads and Behavioural Equivalence Games (abstract)
PRESENTER: Chase Ford
14:45
The Pebble-Relation Comonad in Finite Model Theory (abstract)
PRESENTER: Yoàv Montacute
15:00
Quantum Expectation Transformers for Cost Analysis (abstract)
15:15
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (abstract)
PRESENTER: Junyi Liu
14:00-15:30 Session 50H: SAT (SAT)
14:00
SAT Preprocessors and Symmetry (abstract)
14:30
A Comprehensive Study of k-Portfolios of Recent SAT Solvers (abstract)
PRESENTER: Jakob Bach
15:00
SAT-based Leximax Optimisation Algorithms (abstract)
PRESENTER: Mikolas Janota
14:30-15:00 Session 51: Doctoral Consortium (KR)
Location: Taub 3
14:30
Relevance in Reasoning with and Revision of Conditional Beliefs
14:35
Doctoral Consortium Application
14:40
On Merging of Open-Domain Ontologies
14:45
Structure-based ontology extensions
14:50
Filippo De Bortoli - Reasoning Efficiently with Description Logics that Count
14:55
Data Quality in Ontology-Based Data Access
15:00-15:30 Session 52A: Logic Programming & Machine Learning (ICLP)
Location: Taub 9
15:00
Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks (abstract)
PRESENTER: Fabrizio Riguzzi
15:15
Graph-based Interpretation of Normal Logic Programs (abstract)
PRESENTER: Gopal Gupta
15:00-15:35 Session 52B: Doctoral Consortium (KR)
Location: Taub 3
15:00
Decidability Limits of Finite Ontology-Mediated Query Entailment
15:05
Towards a Logical Account for Human-Aware Explanation Generation in Model Reconciliation Problems
15:10
Logics for Representation and Design of Auctions
15:15
Optimisation Methods for Complex Event Recognition
15:20
On the learnability of knowledge in language domains
15:25
Investigating Novel Representations and Deep Reinforcement Learning for General Game Playing
15:30
Data Efficient Paradigms for Personalized Assessment of Taskable AI Systems
15:30-16:00Coffee Break
16:00-17:30 Session 54A: OR (CP)
Location: Taub 7
16:00
Parallel Hybrid Best-First Search (abstract)
PRESENTER: Simon de Givry
16:30
Sequence Variables for Routing Problems (abstract)
17:00
From Cliques to Colorings and Back Again (abstract)
16:00-17:30 Session 54B: Tutorial + ML (CP)

16:00-17:00: Tutorial

17:00-17:30: Machine Learning

Location: Taub 4
16:00
Building a Constraint Programming Solver Guided by Machine Learning: Opportunities and Challenges (abstract)
17:00
Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints (abstract)
PRESENTER: Daphné Lafleur
16:00-17:30 Session 54D: Applications & Automatic Reasoning (ICLP)
Location: Taub 9
16:00
Making ProB compatible with SICStus and SWI-Prolog (Best Application Paper Award) (abstract)
PRESENTER: David Geleßus
16:22
Building Information Modeling using Constraint Logic Programming (abstract)
PRESENTER: Joaquin Arias
16:44
A Gaze into the Internal Logic of Graph Neural Networks, with Logic (abstract)
17:06
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis (abstract)
16:00-17:30 Session 54E: Temporal Reasoning (KR)
Location: Taub 2
16:00
On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning (abstract)
PRESENTER: Nicola Gigante
16:30
Unique Characterisability and Learnability of Temporal Instance Queries (abstract)
PRESENTER: Yury Savateev
17:00
A Gödel calculus for Linear Temporal Logic (abstract)
16:00-17:30 Session 54F: Description Logics (KR)
Location: Taub 3
16:00
Counting queries over ELHI⊥ ontologies (abstract)
PRESENTER: Quentin Manière
16:30
Ontology-Mediated Querying on Databases of Bounded Cliquewidth (abstract)
PRESENTER: Lukas Schulze
17:00
Finite Entailment of UCRPQs over ALC Ontologies (abstract)
PRESENTER: Albert Gutowski
16:00-17:30 Session 54G: Type and Category Theory (LICS)

"Type and Category Theory": 6 papers (12 min presentation + 2-3 min Q&A)

Chair:
Location: Taub 1
16:00
Semantics for two-dimensional type theory (abstract)
PRESENTER: Benedikt Ahrens
16:15
Normalization for Multimodal Type Theory (abstract)
16:30
Zigzag normalisation for associative n-categories (abstract)
PRESENTER: Lukas Heidemann
16:45
Syllepsis in Homotopy Type Theory (abstract)
PRESENTER: G. A. Kavvos
17:00
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks (abstract)
17:15
A Type Theory for Strictly Unital Infinity-Categories (abstract)
PRESENTER: Alex Rice
16:00-17:30 Session 54H: MaxSAT (SAT)
16:00
MaxSAT-Based Bi-Objective Boolean Optimization (abstract)
PRESENTER: Christoph Jabs
16:30
Incremental Maximum Satisfiability (abstract)
PRESENTER: Andreas Niskanen
17:00
Analysis of Core-Guided MaxSAT Using Cores and Correction Sets (abstract)
PRESENTER: Nina Narodytska
Wednesday, August 3rd

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 56B: Type Theory and Formalization (FSCD)
09:00
An Analysis of Tennenbaum's Theorem in Constructive Type Theory (abstract)
PRESENTER: Marc Hermes
09:30
Constructing Unprejudiced Extensional Type Theories with Choices via Modalities (abstract)
PRESENTER: Vincent Rahli
10:00
Division by two, in homotopy type theory (abstract)
PRESENTER: Samuel Mimram
09:00-10:30 Session 56C: Semantics (ICLP)
Location: Taub 9
09:00
On Syntactic Forgetting under Uniform Equivalence (abstract)
PRESENTER: Matthias Knorr
09:15
Abduction in Probabilistic Logic Programs (abstract)
PRESENTER: Fabrizio Riguzzi
09:30
DeepStochLog: Neural Stochastic Logic Programming (abstract)
PRESENTER: Giuseppe Marra
09:45
Transforming Gringo Rules into Formulas in a Natural Way (abstract)
10:00
On Paraconsistent Belief Revision: the Case of Priest’s Logic of Paradox (abstract)
PRESENTER: Nicolas Schwind
10:15
Model Reconciliation in Logic Programs (abstract)
PRESENTER: Tran Cao Son
09:00-10:30 Session 56E: Quantitative Algebra, Probabilities and Monads (LICS)

"Quantitative Algebra, Probabilities and Monads": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
09:00
Varieties of quantitative algebras and their monads (abstract)
09:15
Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning (abstract)
PRESENTER: Matteo Mio
09:30
Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction) (abstract)
PRESENTER: Cristina Matache
09:45
Probability monads with submonads of deterministic states (abstract)
PRESENTER: Sean Moss
10:00
Monoidal Streams for Dataflow Programming (abstract)
PRESENTER: Mario Román
10:15
Partitions and Ewens Distributions in element-free Probability Theory (abstract)
09:00-10:30 Session 56F: QBF-2 + Stochastic Boolean Satisfiability (SAT)
09:00
Quantified CDCL with Universal Resolution (abstract)
09:30
Relating existing powerful proof systems for QBF (abstract)
PRESENTER: Leroy Chew
10:00
Quantifier Elimination in Stochastic Boolean Satisfiability (abstract)
PRESENTER: Hao-Ren Wang
10:30-11:00Coffee Break
11:00-12:30 Session 58A: Modelling + Robust solutions (CP)

11:00-12:00: Modelling

12:00-12:30: Robust Solutions

Location: Taub 7
11:00
Computing relaxations for the three-dimensional stable matching problem with cyclic preferences (abstract)
PRESENTER: Luis Quesada
11:30
Understanding how people approach constraint modelling and solving (abstract)
PRESENTER: Ruth Hoffmann
12:00
Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (abstract)
PRESENTER: Jheisson Lopez
11:00-12:30 Session 58B: Applications (CP)
Location: Taub 4
11:00
Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (abstract)
PRESENTER: Louis Popovic
11:30
Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (abstract)
PRESENTER: Vianney Coppé
12:00
Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry (abstract)
PRESENTER: Felix Winter
11:00-12:30 Session 58D: Semantics (ICLP)
Location: Taub 9
11:00
Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective (abstract)
11:22
Strong Equivalence of Logic Programs with Counting (abstract)
11:44
Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory (abstract)
PRESENTER: Linde Vanbesien
12:06
Solving Problems in PH with ASP(Q) (abstract)
PRESENTER: Francesco Ricca
11:00-12:30 Session 58E: KR & Machine Learning (KR)
Location: Taub 2
11:00
Neural-Probabilistic Answer Set Programming (abstract)
PRESENTER: Arseny Skryagin
11:30
Faithful Approaches to Rule Learning (abstract)
12:00
Looking Inside the Black-Box: Logic-based Explanations for Neural Networks (abstract)
PRESENTER: João Ferreira
11:00-12:30 Session 58F: Recently Published Research (KR)
Location: Taub 3
11:00
On Paraconsistent Belief Revision in LP (Extended Abstract) (abstract)
PRESENTER: Nicolas Schwind
11:10
A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract) (abstract)
PRESENTER: Laura Giordano
11:20
Influence-Driven Explanations for Bayesian Network Classifiers (abstract)
PRESENTER: Francesca Toni
11:30
Lifting Symmetry Breaking Constraints with Inductive Logic Programming (abstract)
PRESENTER: Alice Tarzariol
11:40
Abstract Argumentation with Markov Networks (Extended Abstract) (abstract)
11:50
Interpreting Neural Networks as Quantitative Argumentation Frameworks (Extended Abstract) (abstract)
12:00
An Axiomatic Approach to Revising Preferences (Extended Abstract) (abstract)
PRESENTER: Adrian Haret
12:10
Simulating Multiwinner Voting Rules in Judgment Aggregation (abstract)
PRESENTER: Julian Chingoma
11:00-12:30 Session 58G: Automata, Transducers and Games (LICS)

"Automata, Transducers and Games": 6 papers (12 min presentation + 2-3 min Q&A)

Chair:
Location: Taub 1
11:00
Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods (abstract)
PRESENTER: Igor Walukiewicz
11:15
The boundedness and zero isolation problems for weighted automata over nonnegative rationals (abstract)
PRESENTER: David Purser
11:30
Efficient Construction of Reversible Transducers from Regular Transducer Expressions (abstract)
PRESENTER: Govind R
11:45
Active learning for sound negotiations (abstract)
PRESENTER: Igor Walukiewicz
12:00
Stochastic Games with Synchronizing Objectives (abstract)
12:15
Characterizing Positionality in Games of Infinite Duration over Infinite Graphs (abstract)
12:30-14:00Lunch Break

Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).

14:00-15:30 Session 59A: Awards (CP)

14:00-15:00: Best paper awards

15:00-15:30: Dissertation award

Location: Taub 7
14:00
Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (abstract)
PRESENTER: Isaac Rudich
14:30
Exploiting Functional Constraints in Generating Dominance Breaking Nogoods for Constraint Optimization (abstract)
PRESENTER: Allen Z. Zhong
15:00
Doctoral Research Award
14:00-15:30 Session 59B: Automata and Computability (FSCD)
14:00
Restricting tree grammars with term rewriting (abstract)
PRESENTER: Felix Laarmann
14:30
On Lookaheads in Regular Expressions with Backreferences (abstract)
PRESENTER: Nariyoshi Chida
15:00
Certified Decision Procedures for Two-Counter Machines (abstract)
14:00-15:30 Session 59C: Justification & Hybrid Knowledge Bases (ICLP)
Location: Taub 9
14:00
Tree-Like Justification Systems are Consistent (abstract)
PRESENTER: Bart Bogaerts
14:22
Nested Justification Systems (abstract)
PRESENTER: Bart Bogaerts
14:44
An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols (abstract)
PRESENTER: Fabrizio Riguzzi
15:06
A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases (abstract)
PRESENTER: Spencer Killen
14:00-15:30 Session 59D: KR & Machine Learning (KR)
Location: Taub 2
14:00
Sum-Product Loop Programming: From Probabilistic Circuits to Loop Programming (abstract)
14:30
Learning generalized policies without supervision using GNNs (abstract)
PRESENTER: Blai Bonet
15:00
Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings (abstract)
PRESENTER: Yaniv Aspis
14:00-15:30 Session 59E: Recently Published Research (KR)
Location: Taub 3
14:00
Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation (abstract)
PRESENTER: Curtis Bright
14:10
Rushing and Strolling among Answer Sets -- Navigation Made Easy (Extended Abstract) (abstract)
PRESENTER: Dominik Rusovac
14:20
A General Framework for Stable Roommates Problems using Answer Set Programming (abstract)
PRESENTER: Esra Erdem
14:30
Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming (abstract)
14:40
Hybrid Conditional Planning for Robotic Applications (Extended Abstract) (abstract)
PRESENTER: Esra Erdem
14:50
LACE: A Logical Approach to Collective Entity Resolution (abstract)
PRESENTER: Meghyn Bienvenu
15:00
Rule Learning over Knowledge Graphs with Genetic Logic Programming (abstract)
14:00-15:00 Session 59F: Invited Talk by Amal Ahmed: Semantic Intermediate Representations for the Working Metatheoretician (LICS)

Semantic Intermediate Representations for the Working Metatheoretician:

Abstract: Designers of typed programming languages commonly prove meta-theoretic properties such as type soundness for at least a core of their language. But any practical language implementation must provide some way of interoperating with code written in other languages -- usually via a foreign-function interface (FFI) -- which opens the door to new, potentially unsafe, behaviors that aren't accounted for in the original type soundness proof. Despite the prevalence of interoperability in practical software, principled foundations for the end-to-end design, implementation, and verification of interoperability mechanisms have been largely neglected. In this talk, I'll advocate a proof technique for _working metatheoreticians_ seeking to ensure soundness or security properties of real languages, which implement interoperability using glue code that mediates interaction between languages after compilation to a common lower-level intermediate representation (IR). This proof technique involves building a _semantic intermediate representation_: a semantic model of source-language types as relations on terms of the lower-level IR. Semantic IRs can be used to guide the design and implementation of sound FFIs and to verify that the IR glue code used to implement conversions ensures type soundness. More interestingly, semantic IRs provide a basis for numerous avenues of future work on the principled design of language interoperability: how to support the inclusion of libraries whose behavior is foreign to the original language, how to prove soundness and security properties that are robust to behaviors (attackers) outside of the semantic IR, and how to develop a semantic-IR compiler backend that makes it easier to implement and verify sound interoperability for a wide array of source languages.

Location: Taub 1
14:00-15:30 Session 59G: Theory (SAT)
14:00
Tight Bounds for Tseitin Formulas (abstract)
PRESENTER: Petr Smirnov
14:30
A generalization of the Satisfiability Coding Lemma and its applications (abstract)
PRESENTER: Harry Sha
15:00
On the Parallel Parameterized Complexity of MaxSAT Variants (abstract)
PRESENTER: Max Bannach
15:00-15:30 Session 60: Linear Recurrences and Skolem Problem (LICS)

Linear recurrences and Skolem problem (rescheduled talks from Tuesday)

Edon Kelmendi. Computing the Density of the Positivity Set for Linear Recurrence Sequences15 min

Richard Lipton, Florian Luca, Joris Nieuwveld, Joel Ouaknine, David Purser and James Worrell. On the Skolem Problem and the Skolem Conjecture15 min

Location: Taub 1
15:30-16:00Coffee Break
16:00-17:30 Session 61A: Awards + ACP General Assembly (CP)

16:00-16:30: Early Career Award

16:30-17:30: ACP General Assembly

Location: Taub 7
16:00
Early Career Award
16:00-17:30 Session 61C: Applications (ICLP)
Location: Taub 9
16:00
A Neuro-Symbolic ASP Pipeline for Visual Question Answering (abstract)
PRESENTER: Nelson Higuera
16:22
Knowledge Authoring with Factual English (abstract)
PRESENTER: Paul Fodor
16:44
Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning (abstract)
PRESENTER: Kristian Reale
16:59
Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (abstract)
PRESENTER: Joaquin Arias
17:14
A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem (abstract)
PRESENTER: Pierre Tassel
16:00-17:00 Session 61D: Invited Talk (KR)
Location: Taub 2
16:00
Probabilities, Reasoning, and Argumentation (abstract)
16:00-17:30 Session 61E: Poster Session (LICS)

Mario Roman. Monoidal Streams for Dataflow Programming

Paolo Pistone. Curry and Howard Meet Borel

Pascal Schweitzer. Choiceless Polynomial Time with Witnessed Symmetric Choice

Yoàv Montacute. The Pebble-Related Comonad in Finite Model Theory

Felipe Ferreira Santos. Separating LREC from LFP

Nikolas Mählmann. Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

16:00-17:30 Session 61F (LICS)

LICS SC meeting (on invitation only)

Location: Taub 201
16:00-17:30 Session 61G: The Olympic Games Session (Block 1) (Olympic Games)

The FLoC Olympic Games 2022 follows the successful edition started in 2014 in conjunction with FLoC, in the spirit of the ancient Olympic Games. Every four years, as part of the Federated Logic Conference, the Games gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At this Olympic Games Session, the competition organizers of the following competitions will present their competitions to the public and give away special prizes to their successful competitors: Confluence Competition, LP/CP Programming Contest, XCSP3, MiniZinc, SAT Competition, MaxSAT Evaluation, Model counting competition, Quantified Boolean Formula.

17:00-18:00 Session 62A: Conditionals (KR)
Location: Taub 2
17:00
Compound conditionals as random quantities and Boolean algebras (abstract)
PRESENTER: Tommaso Flaminio
17:30
A General Framework for Modelling Conditional Reasoning - Preliminary Report (abstract)
PRESENTER: Giovanni Casini
17:00-18:00 Session 62B: Actions (KR)
Location: Taub 3
17:00
Act for Your Duties but Maintain Your Rights (abstract)
PRESENTER: Shufang Zhu
17:30
Epistemic Actions: Comparing Multi-agent Belief Bases with Action Models (abstract)
18:30-20:30 Walking tour (at Haifa) (FLoC)

pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)

Thursday, August 4th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 63A: Tutorial (CP)
Location: Taub 7
09:00
MDD-Based Constraint Programming in Haddock (abstract)
PRESENTER: Laurent Michel
09:00-10:30 Session 63B: SAT (CP)
Location: Taub 4
09:00
On Quantitative Testing of Samplers (abstract)
PRESENTER: Mate Soos
09:30
On the Enumeration of Frequent High Utility Itemsets: A symbolic AI Approach (abstract)
PRESENTER: Said Jabbour
10:00
From Crossing-Free Resolution to Max-SAT Resolution (abstract)
09:00-10:30 Session 63C: Proof Theory and Linear Logic (FSCD)
09:00
Decision problems for linear logic with least and greatest fixed points (abstract)
PRESENTER: Abhishek De
09:30
Linear lambda-calculus is linear (abstract)
PRESENTER: Gilles Dowek
10:00
A Graphical Proof Theory of Logical Time (abstract)
PRESENTER: Matteo Acclavio
09:00-10:00 Session 63D: Invited talk by Manuel Hermenegildo: 50th anniversary of the birth of Prolog: Some reflections on Prolog's Evolution, Status, and Future (ICLP)

50th anniversary of the birth of Prolog: Some reflections on Prolog's Evolution, Status, and Future [LINK TO SLIDES]

Abstract: This year we celebrate Prolog's 50th anniversary, and the continued relevance of Prolog and logic programming as a basis for both higher-level programming and symbolic, explainable AI.  This talk will provide an overview of Prolog's evolution, status, and future. It will start with a quick tour of the major milestones in the advancement of the language and its implementations, from the original Marseille and Edinburgh versions, to the many current ones, with more appearing continuously. This will be followed by some reflections on issues such as what still makes Prolog different and relevant as a language and tool, the best approaches for teaching Prolog, some landmark applications, relation to other logic programming languages, or the use of Prolog and Prolog-related tools for other programming languages.  The talk will also attempt to dispel along the way some common misconceptions about the language, while discussing some past weaknesses and others that may still need addressing. It will conclude with some reflections on challenges and opportunities for the future.

Part of the contents of this talk appear in the recent TPLP paper "50 years of Prolog and Beyond", by Philipp Körner, Michael Leuschel, João Barbosa, Vítor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, Jose F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu, and Giovanni Ciatto, written for Prolog's 50th anniversary and TPLP's 20th anniversary. See prologyear.logicprogramming.org for pointers to this paper and other initiatives related to the Year of Prolog. The Year of Prolog is organized by the Association for Logic Programming and the Prolog Heritage foundation.

Location: Taub 9
09:00-10:30 Session 63E: Argumentation (KR)
Location: Taub 2
09:00
Rediscovering Argumentation Principles Utilizing Collective Attacks (abstract)
PRESENTER: Matthias König
09:30
A Credal Least Undefined Stable Semantics for Probabilistic Logic Programs and Probabilistic Argumentation (abstract)
PRESENTER: Fabio Cozman
10:00
Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework (abstract)
PRESENTER: Tuomo Lehtonen
09:00-10:30 Session 63F: Belief Revision (KR)
Location: Taub 3
09:00
On Syntactic Forgetting with Strong Persistence (abstract)
09:30
Kernel Contraction and the Order of Relevance (abstract)
10:00
Who’s the Expert? On Multi-source Belief Change (abstract)
PRESENTER: Joe Singleton
09:00-10:30 Session 63G: Linear Logic and Proof Systems (LICS)

"Linear Logic and Proof Systems": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
09:00
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings (abstract)
PRESENTER: Takeshi Tsukada
09:15
Bouncing threads for circular and non-wellfounded proofs (abstract)
PRESENTER: David Baelde
09:30
On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems (abstract)
PRESENTER: Ilario Bonacina
09:45
A functorial excursion between algebraic geometry and linear logic (abstract)
10:00
Logical Foundations of Quantitative Equality (abstract)
10:15
Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic (abstract)
09:00-10:30 Session 63H: 25 years of SAT (SAT)

25-years of SAT

09:00
25 years of SAT: Conflict-Driven SAT Solving (abstract)
09:24
25 years of SAT: Maximum Satisfiability for Real-World Optimization (abstract)
09:48
25 years of SAT: Trusting SAT Solvers (abstract)
10:12
25 years of SAT: Proof complexity and SAT solving (abstract)
10:00-10:30 Session 64: Implementation & Transformations (ICLP)
Location: Taub 9
10:00
Efficient Datalog Rewriting for Query Answering in TGD Ontologies (abstract)
PRESENTER: Zhe Wang
10:15
What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration (abstract)
PRESENTER: Mohan Sridharan
10:30-11:00Coffee Break
11:00-12:30 Session 65A: MDD (CP)
Location: Taub 7
11:00
Heuristics for MDD Propagation in Haddock (abstract)
PRESENTER: Rebecca Gentzel
11:30
CNF Encodings of Binary Constraint Trees (abstract)
PRESENTER: Ruiwei Wang
12:00
Nucleus-Satellites Systems of OMDDs for Reducing the Size of Compiled Forms (abstract)
PRESENTER: Nicolas Schmidt
11:00-12:30 Session 65B: Constraint and Conjecture Acquisition (CP)
Location: Taub 4
11:00
Learning Constraint Programming Models from Data using Generate-and-Aggregate (abstract)
PRESENTER: Samuel Kolb
11:30
Constraint Acquisition Based on Solution Counting (abstract)
12:00
Acquiring Maps of Interrelated Conjectures on Sharp Bounds (abstract)
11:00-12:30 Session 65C: Type Theory and Logical Frameworks (FSCD)
Chair:
11:00
A stratified approach to Lob induction (abstract)
PRESENTER: Daniel Gratzer
11:30
Encoding type universes without using matching modulo associativity and commutativity (abstract)
12:00
Adequate and computational encodings in the logical framework Dedukti (abstract)
11:00-12:30 Session 65D: Functional Logic Programming, Datalog & Machine Learning (ICLP)
Location: Taub 9
11:00
From Logic to Functional Logic Programs (abstract)
11:22
MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award) (abstract)
11:44
Jumping Evaluation of Nested Regular Path Queries (abstract)
PRESENTER: Joachim Niehren
12:06
FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data (abstract)
PRESENTER: Gopal Gupta
11:00-12:00 Session 65E: Invited Talk (KR)
Location: Taub 2
11:00
Graph Queries: Do We Study What Matters? (abstract)
11:00-12:30 Session 65F: Graphs, Behavioural Equivalences and Learning (LICS)

"Graphs, Behavioural Equivalences and Learning": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
11:00
Treelike decompositions for transductions of sparse graphs (abstract)
PRESENTER: Sandra Kiefer
11:15
Stable graphs of bounded twin-width (abstract)
PRESENTER: Jakub Gajarský
11:30
Model Checking on Interpretations of Classes of Bounded Local Cliquewidth (abstract)
11:45
Size measures and alphabetic equivalence in the mu-calculus (abstract)
PRESENTER: Johannes Marti
12:00
Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete (abstract)
12:15
Computable PAC Learning of Continuous Features (abstract)
PRESENTER: Cameron Freer
11:00-12:30 Session 65G: Machine-Learning for SAT/SMT (SAT)
11:00
25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren (abstract)
11:30
On the performance of deep generative models of realistic SAT instances (abstract)
12:00
Towards Learning Quantifier Instantiation in SMT (abstract)
PRESENTER: Mikolas Janota
12:00-12:30 Session 66A: Automated Reasoning (KR)
Location: Taub 2
12:00
Automating Reasoning with Standpoint Logic via Nested Sequents (abstract)
12:30-14:00Lunch Break

Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).

14:00-15:30 Session 67A: Tutorial + Benchmarking (CP)

14:00-15:00: Tutorial

15:00-15:30: Benchmarking

Location: Taub 7
14:00
Formal Explainable AI (abstract)
15:00
A framework for generating informative benchmark instances (abstract)
PRESENTER: Nguyen Dang
14:00-15:30 Session 67B: Planning + DCOP (CP)

14:00-15:00: Planning

15:00-15:30: DCOP

Location: Taub 4
14:00
Isomorphisms between STRIPS problems and sub-problems (abstract)
PRESENTER: Arnaud Lequen
14:30
Plotting: A Planning Problem With Complex Transitions (abstract)
15:00
Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs (abstract)
PRESENTER: Jie Wang
14:00-15:00 Session 67C: FSCD Invited Speaker (FSCD)
14:00
A Methodology for Designing Proof Search Calculi for Non-Classical Logics
14:00-14:30 Session 67D: Best DC Paper (Alice Tarzariol): A Model-Oriented Approach for Lifting Symmetries in Answer Set Programming (ICLP)

When solving combinatorial problems, pruning symmetric solution candidates from the search space is essential. Most of the existing approaches are instance-specific and focus on the automatic computation of Symmetry Breaking Constraints (SBCs) for each given problem instance. However, the application of such approaches to large-scale instances or advanced problem encodings might be problematic since the computed SBCs are propositional and, therefore, can neither be meaningfully interpreted nor transferred to other instances. As a result, a time-consuming recomputation of SBCs must be done before every invocation of a solver.

To overcome these limitations, we introduce a new model-oriented approach for Answer Set Programming that lifts the SBCs of small problem instances into a set of interpretable first-order constraints using a form of machine learning called Inductive Logic Programming. After targeting simple combinatorial problems, we aim to extend our method to be applied also for advanced decision and optimization problems.

Location: Taub 9
14:00-15:30 Session 67E: Systems & Robotics (KR)
Location: Taub 2
14:00
Online Grounding of Symbolic Planning Domains in Unknown Environments (abstract)
PRESENTER: Leonardo Lamanna
14:30
Stream Reasoning with Cycles (abstract)
15:00
Symbolic Knowledge Extraction from Opaque Machine Learning Predictors: GridREx & PEDRO (abstract)
PRESENTER: Roberta Calegari
14:00-15:30 Session 67F: Belief Revision/RDFS (KR)
Location: Taub 3
14:00
A Minimal Deductive System for RDFS with Negative Statements (abstract)
PRESENTER: Umberto Straccia
14:30
Hyperintensional Partial Meet Contractions (abstract)
15:00
On the Representation of Darwiche and Pearl’s Epistemic States for Iterated Belief Revision (abstract)
PRESENTER: Nicolas Schwind
14:00-15:30 Session 67G: FOL, SOL and Model Theory (LICS)

"FOL, SOL and Model Theory": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
14:00
The amazing mixed polynomial closure and its applications to two-variable first-order logic (abstract)
14:15
The Regular Languages of First-Order Logic with One Alternation (abstract)
PRESENTER: Corentin Barloy
14:30
Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics (abstract)
PRESENTER: Matthias Naaf
14:45
Geometric decision procedures and the VC dimension of linear arithmetic theories (abstract)
PRESENTER: Alessio Mansutti
15:00
A direct computational interpretation of second-order arithmetic via update recursion (abstract)
15:15
When Locality Meets Preservation (abstract)
14:00-15:30 Session 67H: SAT / PBS (SAT)
Chair:
14:00
Introducing Intel(R) SAT Solver (abstract)
14:30
Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization (abstract)
PRESENTER: Matti Järvisalo
15:00
Certified CNF Translations for Pseudo-Boolean Solving (abstract)
PRESENTER: Andy Oertel
14:30-15:00 Session 68: 10-Year Test-of-Time Award (Torsten Schaub, Max Ostrowski): From "ASP modulo CSP" to "ASP modulo X", or how clingcon paved the way for clingo[X] systems (ICLP)

From "ASP modulo CSP" to "ASP modulo X", or how clingcon paved the way for clingo[X] systems

Abstract: Clingcon extends the ASP system Clingo with linear constraints over integers. As such, its series of variants served as a consecutive design study onhow to extend ASP systems with foreign inferences. Meanwhile this has culminated in the generic theory reasoning framework of the ASP system clingo.We will sketch the evolution of this technology, look at its current state, and emphasis the role of semantics in view of a successful outcome.

 

Location: Taub 9
15:00-15:30 Session 69A: Complexity Theory and Logic (FSCD)
Chair:
15:00
mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity (abstract)
PRESENTER: Thomas Seiller
15:00-15:30 Session 69B: Semantics (ICLP)
Location: Taub 9
15:00
ASP-Based Declarative Process Mining (abstract)
15:15
Implementing Stable-Unstable Semantics with ASPTOOLS and Clingo (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 70: Plenary (FLoC)
16:00
Complexity Measures for Reactive Systems (abstract)
17:00-17:30 Piano concert (KR)

Program:

  • Mozart Sonata n°3 K. 281 B-flat major
  • Liszt Rhapsody n°7
  • Gerschwin Three preludes

Bio: François Schwarzentruber is associate professor at école normale supérieure de Rennes. He took piano lessons by Suzanne Muller-Gunst. He performed Beethoven's piano concertos n° 3 and 4 with the orchestra of institut national polytechnique (INP) of Toulouse,Rhapsody in Blue of Gershwin together with the university orchestra of Rennes. He gave several concerts, in the public library Champs Libres in Rennes, in retirement houses, but also in festivals. He won the "special Mozart and "Amateurs virtuoses" awards at International Ile-de-France Piano Competition (amateurs). He also composes, mostly short pieces for piano.

 

Friday, August 5th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 73A: DEI Special Event (CP)

9:00 Introduction (Chris Beck)

9:05 "Diversity, Equity and Inclusion in CP: Presenting survey results and recent findings" (presenter: Maria Garcia de la Banda)

9:45 Panel on DEI in CP  Panelists: Noa Agmon, Luis Quesada, Hélène Verhaeghe  Panel facilitators: Chris Beck, Maria Garcia de la Banda

Location: Taub 7
09:00-10:30 Session 73B: Reasoning & Solving (ICLP)
Location: Taub 9
09:00
Stream Reasoning with Deadlines (abstract)
09:22
Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling (abstract)
09:44
Efficient Knowledge Compilation Beyond Weighted Model Counting (Best Student Paper Award) (abstract)
PRESENTER: Rafael Kiesel
10:06
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses (abstract)
PRESENTER: Fabio Fioravanti
09:00-10:30 Session 73C: Description Logics (KR)
Location: Taub 2
09:00
Interpolants and Explicit Definitions in Extensions of the Description Logic EL (abstract)
PRESENTER: Marie Fortin
09:30
Sticky Policies in OWL2: Extending PL with fixpoints and Transitive Closure (abstract)
PRESENTER: Luigi Sauro
10:00
Pushing Optimal ABox Repair from EL Towards More Expressive Horn-DLs (abstract)
09:00-10:30 Session 73D: Systems & Robotics / Existential Rules (KR)
Location: Taub 3
09:00
Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (abstract)
PRESENTER: Meghyn Bienvenu
09:30
Forecasting Argumentation Frameworks (abstract)
PRESENTER: Francesca Toni
10:00
ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser (abstract)
PRESENTER: Tobias Geibinger
10:10
On the Relationship between Shy and Warded Datalog+/- (abstract)
PRESENTER: Teodoro Baldazzi
10:20
Chasing streams with existential rules (abstract)
PRESENTER: Thomas Eiter
09:00-10:00 Session 73E: Invited talk by Mikolaj Bojanczyk (LICS)

Transducers of polynomial growth

Abstract: The polyregular functions are a class of string-to-string functions that have polynomial size outputs, and which can be defined using finite state models. There are many equivalent definitions of this class, with roots in automata theory, programming  languages and logic. The talk surveys recent results on polyregular functions. It presents five of the equivalent definitions, and gives self-contained proofs for most of the equivalences. Decision problems as well as restricted subclasses of the polyregular functions are also discussed.

Location: Taub 1
09:15-10:30 Session 74 (Mentoring Workshop)
Location: Taub 6
09:15
Welcome
PRESENTER: Marijana Lazić
09:30
Formal methods for Machine Learning
10:00-10:30 Session 75: Poster Session (LICS)

Daniel Gratzer. Normalization for multimodal type theory

Clemens Grabmayer. Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete

Soumodev Mal. On the Satisfiability of Context-free String Constraints with Subword Ordering

Matthias Naaf. Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics

Jana Hofmann. Deciding Hyperproperties combined with Functional Specifications

 

10:30-11:00Coffee Break
11:00-12:30 Session 76A: Theory + TDM (CP)

11:00-12:00: Theory

12:00-12:30: Trustworthy Decision Making

Location: Taub 7
11:00
Complexity of Minimum-Size Arc-Inconsistency Explanations (abstract)
PRESENTER: Emmanuel Hebrard
11:30
Weisfeiler-Leman Invariant Promise Valued CSPs (abstract)
PRESENTER: Silvia Butti
12:00
An Auditable Constraint Programming Solver (abstract)
PRESENTER: Ciaran McCreesh
11:00-12:30 Session 76B: Propagation + Heuristics (CP)
Location: Taub 4
11:00
A Portfolio-Based Approach to Select Efficient Variable Ordering Heuristics for Constraint Satisfaction Problems (abstract)
PRESENTER: Hongbo Li
11:30
Explaining Propagation for Gini and Spread with Variable Mean (abstract)
PRESENTER: Alexander Ek
12:00
Structured Set Variable Domains in Bayesian Network Structure Learning (abstract)
11:00-12:30 Session 76C: Rewriting (FSCD)
11:00
Polynomial Termination over N is Undecidable (abstract)
11:30
Compositional Confluence Criteria (abstract)
PRESENTER: Nao Hirokawa
12:00
Rewriting for monoidal closed categories (abstract)
PRESENTER: David Sprunger
11:00-12:00 Session 76D: Invited talk by Fabrizio Riguzzi: Probabilistic Logic Programming: Semantics, Inference and Learning (ICLP)

Probabilistic Logic Programming: Semantics, Inference and Learning [LINK TO SLIDES]

Abstract: Probabilistic Logic Programming is now more than 30 years old and has become an active field of research at the intersection of Logic Programming and Uncertainty in AI.Among the various semantics, the Distribution Semantics (DS) has emerged as one of the most intuitive and versatile. The talk will introduce the DS and its various extensions to deal with function symbols, continuous random variables and multiple stable models.Computing the probability of queries is the task of inference, which can be solved either by exact or approximate algorithms. Exact inference is usually performed by means of knowledge compilation while approximate inference by means of Monte Carlo.Inference is at the basis of learning programs from data that has recently received much attention. The talk will provide an overview of algorithms for learning the parameters and for learning the structure of programs, discussing the various Inductive Logic Programming techniques that have been adopted and the various tradeoffs between quality of the model and speed of learning.

Location: Taub 9
11:00-12:30 Session 76E: Belief Merging/Revision (KR)
Location: Taub 2
11:00
The More the Worst-Case-Merrier: A Generalized Condorcet Jury Theorem for Belief Fusion (abstract)
PRESENTER: Jonas Karge
11:30
Region-Based Merging of Open-Domain Terminological Knowledge (abstract)
PRESENTER: Thanh Ma
12:00
Projection of Belief in the Presence of Nondeterministic Actions and Fallible Sensing (abstract)
PRESENTER: Jens Classen
12:10
Inference with System W Satisfies Syntax Splitting (abstract)
PRESENTER: Jonas Haldimann
12:20
Iterated Belief Change, Computationally (abstract)
PRESENTER: Kai Sauerwald
11:00-12:30 Session 76F: Datalog & Existential Rules (KR)
Location: Taub 3
11:00
Conservative Extensions for Existential Rules (abstract)
PRESENTER: Carsten Lutz
11:30
Revisiting Semiring Provenance for Datalog (abstract)
PRESENTER: Liat Peterfreund
12:00
Normalisations of Existential Rules: Not so Innocuous! (abstract)
11:00-12:30 Session 76G: Verification (LICS)

"Verification": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
11:00
On the Satisfiability of Context-free String Constraints with Subword Ordering (abstract)
PRESENTER: Soumodev Mal
11:15
The complexity of soundness in workflow nets (abstract)
11:30
Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes (abstract)
11:45
Probabilistic Verification Beyond Context-Freeness (abstract)
PRESENTER: Andrzej Murawski
12:00
Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification (abstract)
12:15
The complexity of bidirected reachability in valence systems (abstract)
PRESENTER: Georg Zetzsche
11:00-12:30 Session 76H (Mentoring Workshop)
Location: Taub 6
11:00
How to be an Abstraction Engineer (abstract)
11:45
How to Give a Good (Research) Talk
12:00-12:30 Session 77: ASP Optimization (ICLP)
Location: Taub 9
12:00
Rushing and Strolling among Answer Sets – Navigation Made Easy (abstract)
PRESENTER: Dominik Rusovac
12:15
Large-Neighbourhood Search for ASP Optimisation (abstract)
PRESENTER: Tobias Geibinger
12:30-14:00Lunch Break

Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).

14:00-15:30 Session 78A: Categorical Semantics (FSCD)
14:00
Stateful Structural Operational Semantics (abstract)
PRESENTER: Henning Urbat
14:30
A combinatorial approach to higher-order structure for polynomial functors (abstract)
PRESENTER: Hugo Paquet
15:00
Galois connecting call-by-value and call-by-name (abstract)
PRESENTER: Dylan McDermott
14:00-15:30 Session 78B: Logic Programming, Constraints & Machine Learning (ICLP)
Location: Taub 9
14:00
A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers (abstract)
PRESENTER: Zach Hansen
14:22
On Model Reconciliation: How to Reconcile When Robot Does not Know Human’s Model? (abstract)
PRESENTER: Tran Cao Son
14:44
An ASP approach for reasoning on neural networks under a finitely many-valued semantics for weighted conditional knowledge bases (abstract)
PRESENTER: Laura Giordano
15:06
Efficient lifting of symmetry breaking constraints for complex combinatorial problems (Best Student Paper Award) (abstract)
PRESENTER: Alice Tarzariol
14:00-15:00 Session 78C: Invited Talk (KR)
Location: Taub 2
14:00
From Non-monotonic Reasoning to Argumentation and Commonsense (Great Moments in KR Talk) (abstract)
14:00-15:30 Session 78D: Complexity and Circuits (LICS)

"Complexity and Circuits": 6 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
14:00
Separating LREC from LFP (abstract)
14:15
Reasonable Space for the Lambda-Calculus, Logarithmically (abstract)
PRESENTER: Gabriele Vanoni
14:30
Cyclic Implicit Complexity (abstract)
PRESENTER: Gianluca Curzi
14:45
Identity testing for radical expressions (abstract)
PRESENTER: Klara Nosan
15:00
Complexity of Modular Circuits (abstract)
PRESENTER: Piotr Kawałek
15:15
Choiceless Polynomial Time with Witnessed Symmetric Choice (abstract)
14:00-15:30 Session 78E (Mentoring Workshop)
Location: Taub 6
14:00
On Time and Space (of Humans) (abstract)
14:45
From PhD to industry: A recent graduate’s perspective (abstract)
14:00-15:30 Session 78F: QBF + Awards / competitions (SAT)
14:00
QBF Merge Resolution is powerful but unnatural (abstract)
PRESENTER: Gaurav Sood
14:30
Awards / Competition Results - I (with Live Broadcast) (abstract)
15:00-15:30 Session 79A: Planning (KR)
Location: Taub 2
15:00
Discovering User-Interpretable Capabilities of Black-Box Planning Agents (abstract)
PRESENTER: Pulkit Verma
15:00-15:30 Session 79B: Deontic Logic (KR)
Chair:
Location: Taub 3
15:00
Dynamic Deontic Logic for Permitted Announcements (abstract)
PRESENTER: Xu Li
15:30-16:00Coffee Break
15:30-17:00 Session 80A: KR & Machine Learning (KR)
Location: Taub 2
15:30
Learning Typed Rules over Knowledge Graphs (abstract)
PRESENTER: Hong Wu
16:00
A Graph Neural Network Reasoner for Game Description Language (abstract)
PRESENTER: Alvaro Gunawan
16:30
Explaining Causal Models with Argumentation: the Case of Bi-variate Reinforcement (abstract)
PRESENTER: Francesca Toni
15:30-16:30 Session 80B: Argumentation (KR)
Location: Taub 3
15:30
On Dynamics in Structured Argumentation Formalisms (abstract)
PRESENTER: Anna Rapberger
16:00
Defining Defense and Defeat in Abstract Argumentation From Scratch -- A Generalizing Approach (abstract)
PRESENTER: Lydia Blümel
16:00-16:30 Session 81B: Scheduling & Planning (ICLP)
Location: Taub 9
16:00
Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers (abstract)
PRESENTER: Wolfgang Faber
16:15
Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP (abstract)
16:00-16:45 Session 81C: CSP, SAT and Boolean Algebra (LICS)

"CSP, SAT, Boolean algebra": 3 papers (12 min presentation + 2-3 min Q&A)

Location: Taub 1
16:00
On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing (abstract)
16:15
Smooth approximations and CSPs over finitely bounded homogeneous structures (abstract)
PRESENTER: Michael Pinsker
16:30
A first-order completeness result about characteristic Boolean algebras in classical realizability (abstract)
16:50-17:30 Session 83: Award Session: Kleene award, LICS Test-of-Time award, Church award (LICS)

Award Session: Kleene award, LICS Test-of-Time award, Church award

Location: Taub 1
Saturday, August 6th

View this program: with abstractssession overviewtalk overview

Sunday, August 7th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 85A: Formal Methods for Probabilistic Programs (CAV)
Location: Taub 1
09:00
Data-Driven Invariant Learning for Probabilistic Programs (abstract)
PRESENTER: Subhajit Roy
09:20
Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (abstract)
09:40
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (abstract)
PRESENTER: Lutz Klinkenberg
10:00
Abstraction-Refinement for Hierarchical Probabilistic Models (abstract)
PRESENTER: Sebastian Junges
09:00-10:30 Session 85B: CSF Opening and Security Protocols 1 (CSF)
Location: Taub 2
09:00
Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting (abstract)
PRESENTER: Petar Paradžik
09:30
Is Eve nearby? Analysing protocols under the distant-attacker assumption (abstract)
10:00
A small bound on the number of sessions for security protocols (abstract)
09:00-10:30 Session 85C: Opening and Query Answering (DL)
Location: Taub 9
09:00
DL Opening Remarks
PRESENTER: Martin Homola
09:15
Complexity Landscape for Counting Queries (Extended abstract) (abstract)
PRESENTER: Quentin Manière
09:40
Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (abstract)
PRESENTER: Alisa Kovtunova
10:05
Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (abstract)
PRESENTER: Yury Savateev
09:00-10:00 Session 85D: Invited Talk (ITP)
09:00
(Invited) Modelling and Verifying Properties of Biological Neural Networks (abstract)
09:30-10:30 Session 87: Argumentation 1 (NMR)
Location: Taub 4
09:30
Abductive Reasoning with Sequent-Based Argumentation (Extended Abstract) (abstract)
PRESENTER: Ofer Arieli
10:00
The Effect of Preferences in Abstract Argumentation Under a Claim-Centric View (abstract)
10:30-11:00Coffee Break
11:00-12:00 Session 89: Keynote (FLoC)
11:00
Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry (abstract)
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, ITP).

 

14:00-15:30 Session 90A: Formal Methods for Neural Networks (CAV)
Location: Taub 1
14:00
Shared Certificates for Neural Network Verification (abstract)
14:20
Example Guided Synthesis of Linear Approximations for Neural Network Verification (abstract)
PRESENTER: Brandon Paulsen
14:40
Verifying Neural Networks Against Backdoor Attacks (abstract)
PRESENTER: Long H. Pham
15:00
Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning (abstract)
PRESENTER: Jiaxu Tian
15:20
Neural Network Robustness as a Verification Property: A Principled Case Study (abstract)
PRESENTER: Marco Casadio
14:00-15:30 Session 90B: Language-based Security (CSF)
Location: Taub 2
14:00
A Formal Model of Checked C (abstract)
PRESENTER: Liyi Li
14:30
SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation (abstract)
PRESENTER: Roberto Blanco
15:00
Proving full-system security properties under multiple attacker models on capability machines (abstract)
14:00-15:30 Session 90C: Joint NMR/DL Session (1) (DL)
Location: Taub 9
14:00
Hybrid Answer Set Programming: Opportunities and Challenges (abstract)
15:00
Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (abstract)
PRESENTER: Rafael Kiesel
14:00-15:30 Session 90D (ITP)
14:00
Candle: A Verified Implementation of HOL Light (abstract)
14:30
A Verified Cyclicity Checker (abstract)
PRESENTER: Arve Gengelbach
15:00
Kalas: A Verified, End-to-End Compiler for a Choreographic Language (abstract)
14:00-15:00 Session 90E: Keynote NMR and DL (NMR)
Location: Taub 9
14:00
Hybrid Anwer Set Programming: Opportunities and Challenges (abstract)
15:00-15:30 Session 91: Joint DL/NMR Session A (NMR)
Location: Taub 9
15:00
Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
PRESENTER: Rafael Kiesel
15:30-16:00Coffee Break
16:00-17:30 Session 92A: Software Verification and Model Checking (CAV)
Location: Taub 1
16:00
The Lattice-Theoretic Essence of Property Directed Reachability Analysis (abstract)
PRESENTER: Mayuko Kori
16:20
Affine Loop Invariant Generation via Matrix Algebra (abstract)
PRESENTER: Yucheng Ji
16:40
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (abstract)
17:00
Proof-guided Underapproximation Widening for Bounded Model Checking (abstract)
PRESENTER: Subhajit Roy
17:20
SolCMC: Solidity Compiler’s Model Checker (abstract)
PRESENTER: Leonardo Alt
16:00-17:30 Session 92B: Privacy 1 (CSF)
Location: Taub 2
16:00
Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes (abstract)
PRESENTER: Peeter Laud
16:30
DPL: A Language for GDPR Enforcement (abstract)
PRESENTER: Farzane Karami
17:00
Privacy as Reachability (abstract)
16:00-17:30 Session 92C: Joint NMR/DL Session (2) (DL)
Location: Taub 9
16:00
Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (abstract)
16:25
Defeasible reasoning in RDFS (abstract)
PRESENTER: Giovanni Casini
16:50
Modelling Multiple Perspectives by Standpoint-Enhanced DLs (abstract)
16:00-17:30 Session 92D (ITP)
16:00
Formalized functional analysis with semilinear maps (abstract)
16:30
Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics (abstract)
PRESENTER: Chelsea Edmonds
17:00
Formalization of a Stochastic Approximation Theorem (abstract)
PRESENTER: Koundinya Vajjha
16:00-17:30 Session 92E: Joint DL/NMR Session B (NMR)
Location: Taub 9
16:00
Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (abstract)
16:25
Defeasible reasoning in RDFS (abstract)
PRESENTER: Giovanni Casini
16:50
Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics
Monday, August 8th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 94A: Hyperproperties and Security (CAV)
Location: Taub 1
09:00
Software Verification of Hyperproperties Beyond k-Safety (abstract)
PRESENTER: Raven Beutner
09:20
A Scalable Shannon Entropy Estimator (abstract)
PRESENTER: Kuldeep S. Meel
09:40
PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (abstract)
PRESENTER: Yuxin Fan
10:00
Explaining Hyperproperty Violations (abstract)
PRESENTER: Julian Siber
10:20
Distilling Constraints in Zero-Knowledge Protocols (abstract)
PRESENTER: Miguel Isabel
09:00-10:30 Session 94B: Voting and Distributed Systems (CSF)
Location: Taub 2
09:00
N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures (abstract)
PRESENTER: Thilo Weghorn
09:30
Applying consensus and replication securely with FLAQR (abstract)
PRESENTER: Priyanka Mondal
10:00
How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis (abstract)
PRESENTER: Johannes Müller
09:00-10:30 Session 94C: Joint NMR/DL Session (3) (DL)
Location: Taub 9
09:00
Rectifying Classifiers (abstract)
10:00
Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (abstract)
PRESENTER: Sophie Tourret
09:00-10:30 Session 94D: Invited Talk and Cooperating Reasoners (IJCAR)
09:00
From the Universality of Mathematical Truth to the Interoperability of Proof Systems (Invited Talk)
10:00
Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description) (abstract)
PRESENTER: Gereon Kremer
09:00-10:30 Session 94E (ITP)
09:00
Refinement of Parallel Algorithms down to LLVM (abstract)
09:30
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification (abstract)
PRESENTER: Hrutvik Kanabar
10:00
Dandelion: Certified Approximations of Elementary Functions (abstract)
PRESENTER: Heiko Becker
10:30-11:00Coffee Break
11:00-12:30 Session 96B: Cryptography 1 (CSF)
Location: Taub 2
11:00
Contingent payments from two-party signing and verification for abelian groups (abstract)
PRESENTER: Sergiu Bursuc
11:30
Collusion-Preserving Computation without a Mediator (abstract)
PRESENTER: Yun Lu
12:00
Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox (abstract)
PRESENTER: Sabine Oechsner
11:00-12:30 Session 96C: Joint NMR/DL Session (4) (DL)
Location: Taub 9
11:00
AGM Revision in Description Logics Under Fixed-Domain Semantics (abstract)
11:25
Repairing Ontologies via Kernel Pseudo-Contraction (abstract)
11:50
Pointwise Circumscription in Description Logics (abstract)
12:15
Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (abstract)
PRESENTER: Martin Homola
11:00-12:30 Session 96D: Effective Superposition and Orderings (IJCAR)
11:00
SCL(EQ): SCL for First-Order Logic with Equality (abstract)
11:20
Ground joinability and connectedness in the superposition calculus (abstract)
PRESENTER: André Duarte
11:40
Term Ordering for Non-Reachability of (Conditional) Rewriting (abstract)
12:00
An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (abstract)
PRESENTER: Lorenz Leutgeb
11:00-12:30 Session 96E (ITP)
11:00
Synthetic Kolmogorov Complexity in Coq (abstract)
PRESENTER: Yannick Forster
11:30
Formalizing Szemerédi's Regularity Lemma in Lean (abstract)
PRESENTER: Yaël Dillies
12:00
Formalizing the divergence theorem and the Cauchy integral formula in Lean (abstract)
11:00-12:30 Session 96F: Joint DL/NMR Session D (NMR)
Location: Taub 9
11:00
AGM Revision in Description Logics Under Fixed-Domain Semantics
11:25
Repairing Ontologies via Kernel Pseudo-Contraction (abstract)
11:50
Pointwise Circumscription in Description Logics
12:15
Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results
PRESENTER: Martin Homola
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).

14:00-15:30 Session 97A: Formal Methods for Hardware, Cyber-Physical and Hybrid Systems (CAV)
Location: Taub 1
14:00
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (abstract)
PRESENTER: Ryotaro Banno
14:20
Abstraction Modulo Stability for Reverse Engineering (abstract)
PRESENTER: Anna Becchi
14:40
Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (abstract)
PRESENTER: Ethan Lew
15:00
RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (abstract)
PRESENTER: Sylvie Putot
15:10
STLmc: Robust STL Model Checking of Hybrid Systems using SMT (abstract)
PRESENTER: Kyungmin Bae
15:20
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (abstract)
14:00-15:30 Session 97B: Invited Talk 1 (CSF)
Location: Taub 2
14:00
Membership Inference Attacks against Classifiers (abstract)
14:00-15:30 Session 97C: Query Answering & Extensions (DL)
Location: Taub 9
14:00
Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract) (abstract)
PRESENTER: Meghyn Bienvenu
14:25
Ontology-based Data Federation (Extended Abstract) (abstract)
PRESENTER: Diego Calvanese
14:50
Comonadic Semantics for Description Logics Games (abstract)
15:05
Advanced languages of terms for ontologies (abstract)
14:00-15:30 Session 97D: Knowledge Representation and Justification (IJCAR)
Chair:
14:00
Actions over Core-closed Knowledge Bases (abstract)
PRESENTER: Claudia Cauli
14:20
GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (abstract)
PRESENTER: Tanel Tammet
14:35
Local Reductions for the Modal Cube (abstract)
PRESENTER: Cláudia Nalon
14:55
Evonne: Interactive Proof Visualization for Description Logics (System Description) (abstract)
PRESENTER: Patrick Koopmann
15:10
Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications (abstract)
PRESENTER: Hui Yang
14:00-15:30 Session 97E (ITP)
14:00
Deeper Shallow Embeddings (abstract)
PRESENTER: Jacob Prinz
14:30
Compositional Verification of Interacting Systems using Event Monads (abstract)
PRESENTER: Bohua Zhan
15:00
Reflexive tactics for algebra, revisited (abstract)
14:00-15:30 Session 97F: Belief Revision (NMR)
Location: Taub 4
14:00
Trust Graphs for Belief Revision: Framework and Implementation (abstract)
PRESENTER: Aaron Hunter
14:30
Truth-Tracking with Non-Expert Information Sources (abstract)
PRESENTER: Joseph Singleton
15:00
Asking human reasoners to judge postulates of belief change for plausibility (abstract)
PRESENTER: Clayton Baker
15:30-16:00Coffee Break
16:00-17:30 Session 98A: Probabilistic Techniques (CAV)
Location: Taub 1
16:00
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (abstract)
16:20
Sampling-Based Verification of CTMCs with Uncertain Rates (abstract)
PRESENTER: Thom Badings
16:40
Playing Against Fair Adversaries in Stochastic Games with Total Rewards (abstract)
PRESENTER: Pablo Castro
17:00
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (abstract)
PRESENTER: Lorenz Leutgeb
17:20
Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (abstract)
PRESENTER: Aina Niemetz
16:00-17:30 Session 98C: Tractable DL (DL)
Location: Taub 9
16:00
Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (abstract)
PRESENTER: Patrick Koopmann
16:25
Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies (abstract)
16:50
A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (abstract)
17:15
Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract) (abstract)
PRESENTER: Laura Giordano
16:00-17:30 Session 98D: Preprocessing and Simplification (IJCAR)
16:00
SAT-based Proof Search in Intermediate Propositional Logics (abstract)
16:20
Preprocessing of Propagation Redundant Clauses (abstract)
PRESENTER: Joseph Reeves
16:40
Clause Redundancy and Preprocessing in Maximum Satisfiability (abstract)
PRESENTER: Jeremias Berg
17:00
Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE) (abstract)
PRESENTER: Tomohiro Fujita
16:00-17:30 Session 98F: Preferences and Conditionals (NMR)
Location: Taub 4
16:00
Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect (abstract)
PRESENTER: Jesse Heyninck
16:30
Situated Conditionals - A Brief Introduction (abstract)
PRESENTER: Giovanni Casini
17:00
On some weakenings of transitivity in the logic of norms (extended abstract) (abstract)
18:30-20:30 Walking tour (at Haifa) (FLoC)

pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)

Tuesday, August 9th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 100B: Information Flow (CSF)
Location: Taub 2
09:00
IFCIL: An Information Flow Configuration Language for SELinux (abstract)
09:30
Towards a General-Purpose Dynamic Information Flow Policy (abstract)
PRESENTER: Peixuan Li
10:00
Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games (abstract)
09:00-10:30 Session 100C: Modularity and Forgetting (1) (DL)
Location: Taub 9
09:00
More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (abstract)
PRESENTER: Andrea Mazzullo
09:25
Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (abstract)
09:50
Fine-Grained Forgetting for the Description Logic ALC (abstract)
10:15
Uniform and Modular Sequent Systems for Description Logics (abstract)
PRESENTER: Jonas Karge
09:00-10:30 Session 100D: Choices, Substitutions and Formalizations (IJCAR)
09:00
Sequent Calculi for Choice Logics (abstract)
09:20
Lash 1.0 (System Description) (abstract)
PRESENTER: Cezary Kaliszyk
09:35
Goéland : A Concurrent Tableau-Based Theorem Prover (System Description) (abstract)
PRESENTER: Julie Cailler
09:50
Synthetic tableaux: minimal tableau search heuristics (abstract)
10:10
Binary codes that do not preserve primitivity (abstract)
PRESENTER: Štěpán Holub
09:00-10:30 Session 100E (ITP)
09:00
Formalization of Randomized Approximation Algorithms for Frequency Moments (abstract)
09:30
Mechanizing Soundness of Off-Policy Evaluation (abstract)
PRESENTER: Jared Yeager
10:00
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt (abstract)
PRESENTER: Alley Stoughton
09:00-10:00 Session 100F: Keynote (NMR)
Location: Taub 4
09:00
Fallacious arguments: the place where Knowledge Representation and Argument Mining meet each other (abstract)
10:00-10:30 Session 101: NMR and Learning (NMR)
Location: Taub 4
10:00
There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot (abstract)
PRESENTER: Mohan Sridharan
10:30-11:00Coffee Break
11:00-12:30 Session 102A: Automata and Logic (CAV)
Location: Taub 1
11:00
FORQ-based Language Inclusion Formal Testing (abstract)
PRESENTER: Kyveli Doveri
11:20
Sound Automation of Magic Wands (abstract)
11:40
Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (abstract)
PRESENTER: Yong Li
12:00
From Spot 2.0 to Spot 2.10: What's New? (abstract)
12:10
Complementing Büchi Automata with Ranker (abstract)
11:00-12:30 Session 102B: Security Protocols 2 (CSF)
Location: Taub 2
11:00
Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant (abstract)
PRESENTER: Adrien Koutsos
11:30
Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol (abstract)
PRESENTER: Felipe Boeira
12:00
Symbolic protocol verification with dice: process equivalences in the presence of probabilities (abstract)
PRESENTER: Steve Kremer
11:00-12:30 Session 102C: Expressivity & Decidability (DL)
Location: Taub 9
11:00
Charting the Borderland – Decidability in Description Logics and Beyond (abstract)
12:00
Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (abstract)
PRESENTER: Alisa Kovtunova
11:00-12:30 Session 102D: Proof Systems and Recursion (IJCAR)
11:00
Finite two-dimensional proof systems for non-finitely axiomatizable logics (abstract)
11:20
Le\'sniewski's Ontology -- Proof-Theoretic Characterization (abstract)
11:40
Cyclic Proofs, Hypersequents, and Transitive Closure Logic (abstract)
12:00
Rensets and Renaming-Based Recursion for Syntax and Bindings (abstract)
11:00-12:30 Session 102E (ITP)
11:00
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (abstract)
11:30
Undecidability of Dyadic First-Order Logic in Coq (abstract)
PRESENTER: Johannes Hostert
12:00
Computational Back-and-Forth Arguments in Constructive Type Theory (abstract)
11:00-12:30 Session 102F: Argumentation 2 (NMR)

Argumentation

Location: Taub 4
11:00
Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity (abstract)
PRESENTER: Markus Ulbricht
11:30
Bipolar Argumentation Frameworks with Explicit Conclusions: Connecting Argumentation and Logic Programming (abstract)
PRESENTER: Fabio Cozman
12:00
From Weighted Conditionals to a Gradual Argumentation Semantics and back (abstract)
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).

13:00-14:00 Session 103: Tool Demonstrations (CAV)

Tool demonstrations for:

  1. STLmc: Robust STL Model Checking of Hybrid Systems using SMT (13:00-13:30)
  2. UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (13:30-14:00)
14:00-16:00 Session 104A: Deductive Verification and Decision Procedures (CAV)
Location: Taub 1
14:00
Even Faster Conflicts and Lazier Reductions for String Solvers (abstract)
PRESENTER: Andres Noetzli
14:20
Local Search For SMT on Linear Integer Arithmetic (abstract)
PRESENTER: Shaowei Cai
14:40
Reasoning about Data Trees using CHCs (abstract)
PRESENTER: Gennaro Parlato
15:00
Verified Erasure Correction in Coq with MathComp and VST (abstract)
PRESENTER: Joshua M. Cohen
15:20
End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (abstract)
PRESENTER: Shenghao Yuan
15:40
Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (abstract)
PRESENTER: Joonwon Choi
14:00-15:30 Session 104B: Invited Talk 2 (CSF)
Location: Taub 2
14:00
So near and yet so far: formal verification of distance bounding protocols (abstract)
14:00-16:00 Session 104C: Abduction and Explanations (DL)
Location: Taub 9
14:00
Concept Abduction for Description Logics (abstract)
PRESENTER: Yevgeny Kazakov
14:25
On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (abstract)
PRESENTER: Patrick Koopmann
14:50
SAT-Based Axiom Pinpointing Revisited (abstract)
PRESENTER: Yevgeny Kazakov
15:15
An API for DL Abduction Solvers (abstract)
PRESENTER: Martin Homola
15:30
Evaluating the Interpretability of Threshold Operators (abstract)
15:45
A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (abstract)
PRESENTER: Bernardo Alkmim
14:00-15:30 Session 104D: Proof Search and Generalizations (IJCAR)
14:00
Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (abstract)
PRESENTER: Chaitanya Mangla
14:20
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (abstract)
14:35
Semantic Relevance (abstract)
14:55
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (abstract)
PRESENTER: Santiago Escobar
15:10
A framework for approximate generalization in quantitative theories (ONLINE) (abstract)
PRESENTER: Temur Kutsia
14:00-15:30 Session 104E (ITP)
14:00
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r) (abstract)
14:30
Formalizing the ring of adèles of a global field (abstract)
15:00
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant (abstract)
14:00-15:30 Session 104F: Agents, actions and planning (NMR)
Location: Taub 4
14:00
Modelling Agents Roles in the Epistemic Logic L-DINF (abstract)
14:30
A situation-calculus model of Knowledge and Belief based on Thinking about Justifications (abstract)
15:00
Towards Legally and Ethically Correct Online HTN Planning for Data Transfer (abstract)
PRESENTER: Hisashi Hayashi
15:00-16:00 Session 105: The Olympic Games Session (Block 2) (Olympic Games)

The FLoC Olympic Games 2022 follows the successful edition started in 2014 in conjunction with FLoC, in the spirit of the ancient Olympic Games. Every four years, as part of the Federated Logic Conference, the Games gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At this Olympic Games Session, the competition organizers of the following competitions will present their competitions to the public and give away special prizes to their successful competitors: SYNTComp, CASC-J11, termCOMP, SMT Competition, SL Competition.

Location: Taub 8
16:00-16:30Coffee Break
16:30-17:30 Session 108: Plenary (FLoC)
Chair:
16:30
SMT-based Verification of Distributed Network Control Planes (abstract)
17:30-18:30 Session 109: Business Meeting (CAV)

17:30-17:45 - As part of the buisneess meeting we will have a 15 minutes presentation by Pavithra Prabhakar.

Title: Formal Methods and Verification Programs and International Partnerships at NSF.

The talk will provide a brief overview of the funding opportunities at the US National Science Foundation related to the area of formal methods and computer aided verification. International partnerships and opportunities for participation of the broader scientific community will be highlighted.

Location: Taub 1
Wednesday, August 10th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 110B: Privacy 2 (CSF)
Location: Taub 2
09:00
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co (abstract)
PRESENTER: Peter B. Rønne
09:30
Universal Optimality and Robust Utility Bounds for Metric Differential Privacy (abstract)
10:00
Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments (abstract)
PRESENTER: Semyon Yurkov
09:00-10:30 Session 110C: Modularity and Forgetting (2) (DL)
Location: Taub 9
09:00
Knowledge Extraction Based on Forgetting and Subontology Generation (abstract)
10:00
Next Steps for ReAD: Modules for Classification Optimisation (abstract)
PRESENTER: Haoruo Zhao
09:00-10:30 Session 110D: System Evolution and Termination (IJCAR)
09:00
CTL* model checking for data-aware dynamic systems with arithmetic (abstract)
PRESENTER: Sarah Winkler
09:20
Implicit Definitions with Differential Equations for KeYmaera X (System Description) (abstract)
PRESENTER: Yong Kiam Tan
09:35
On eventual non-negativity and positivity for the weighted sum of powers of matrices (abstract)
09:55
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (abstract)
PRESENTER: Florian Frohn
10:10
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (abstract)
PRESENTER: Nils Lommen
09:00-10:30 Session 110E (ITP)
09:00
(Invited) User Interface Design in the HolPy Theorem Prover (abstract)
10:00
Accelerating Verified-Compiler Development with a Verified Rewriting Engine (abstract)
PRESENTER: Jason Gross
10:30-11:00Coffee Break
11:00-12:30 Session 112B: Verification and Synthesis (CSF)
Location: Taub 2
11:00
Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems (abstract)
PRESENTER: Lisa Oakley
11:30
The Complexity of Verifying Boolean Programs as Differentially Private (abstract)
PRESENTER: Ludmila Glinskih
12:00
Adversary Safety by Construction in a Language of Cryptographic Protocols (abstract)
PRESENTER: Alice Lee
11:00-12:30 Session 112C: Referring Expressions & Information Extraction (DL)
Location: Taub 9
11:00
Computing Concept Referring Expressions with Standard OWL Reasoners (abstract)
PRESENTER: Birte Glimm
11:25
Accessing Document Data Sources using Referring Expression Types (abstract)
PRESENTER: David Toman
11:50
Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs (abstract)
PRESENTER: Diego Calvanese
12:15
Category-based Semantics for the Description Logic ALC and Reasoning (abstract)
PRESENTER: Ludovic Brieulle
11:00-12:30 Session 112D: Decidable Logics and Models (IJCAR)
11:00
Connection-minimal Abduction in EL via translation to FOL (abstract)
PRESENTER: Sophie Tourret
11:20
Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (abstract)
PRESENTER: Lucas Bueri
11:40
Reasoning About Vectors using an SMT Theory of Sequences (abstract)
PRESENTER: Clark Barrett
12:00
Flexible Proof Production in an Industrial-Strength SMT Solver (abstract)
PRESENTER: Haniel Barbosa
12:30-14:00Lunch Break

Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, IJCAR, ITP).

13:00-14:00 Session 114: Tool Demonstrations (CAV)

Tool demonstrations for:

  1. From Spot 2.0 to Spot 2.10: What's New? (13:00-13:30)
  2. Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (13:30-14:00)
14:00-15:30 Session 115A: Machine Learning (CAV)
Location: Taub 1
14:00
Specification-Guided Learning of Nash Equilibria with High Social Welfare (abstract)
14:20
Synthesizing Fair Decision Trees via Iterative Constraint Solving (abstract)
PRESENTER: Jingbo Wang
14:40
SMT-based Translation Validation for Machine Learning Compiler (abstract)
PRESENTER: Juneyoung Lee
15:00
Verifying Fairness in Quantum Machine Learning (abstract)
PRESENTER: Ji Guan
15:20
MoGym: Using Formal Models for Training and Verifying Decision-making Agents (abstract)
14:00-15:30 Session 115B: Cryptography 2 (CSF)
Location: Taub 2
14:00
Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing (abstract)
PRESENTER: Floyd Zweydinger
14:30
A Complete Characterization of Security for Linicrypt Block Cipher Modes (abstract)
PRESENTER: Lawrence Roy
15:00
Locked Circuit Indistinguishability: A Notion of Security for Logic Locking (abstract)
PRESENTER: Mohamed Elmassad
14:00-15:30 Session 115C: Invited Talk and Optimized Reasoning (IJCAR)
14:00
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
PRESENTER: Elvira Albert
15:00
Guiding an Automated Theorem Prover with Neural Rewriting (abstract)
14:00-15:30 Session 115D (ITP)
14:00
Use and abuse of instance parameters in the Lean mathematical library (abstract)
14:30
The Zoo of Lambda-Calculus Reduction Strategies, and Coq (abstract)
PRESENTER: Tomasz Drab
15:00
Formalizing the set of primes as an alternative to the DPRM theorem (short paper) (abstract)
PRESENTER: Cezary Kaliszyk
15:30-16:00Coffee Break
16:00-17:30 Session 116A: Synthesis and Concurrency (CAV)
Location: Taub 1
16:00
Synthesis and Analysis of Petri Nets from Causal Specifications (abstract)
16:20
Verifying generalised and structural soundness of workflow nets via relaxations (abstract)
16:40
Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (abstract)
PRESENTER: Andreas Katis
16:50
Information Flow Guided Synthesis (abstract)
PRESENTER: Niklas Metzger
17:10
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (abstract)
PRESENTER: Andreas Gittis
16:00-17:00 Session 116B: Hyperproperties (CSF)
Location: Taub 2
16:00
Prophecy Variables for Hyperproperty Verification (abstract)
PRESENTER: Raven Beutner
16:30
Mapping Synthesis for Hyperproperties (abstract)
PRESENTER: Tzu-Han Hsu
16:00-17:00 Session 116C: Modalities and Decidability (IJCAR)
16:00
Non-associative, non-commutative multi-modal linear logic (abstract)
PRESENTER: Stepan Kuznetsov
16:20
Paraconsistent Gödel modal logic (abstract)
16:40
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (abstract)
PRESENTER: Yoni Zohar
Thursday, August 11th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 120A: SAT/SMT Solving (DSV)
Location: Ullmann 300
09:00
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (abstract)
09:45
Democratizing SAT Solving (abstract)
09:00-10:30 Session 120B (FRIDA)
Location: Ullmann 102
09:00
Preserving Hyperproperties when Using Concurrent Objects (abstract)
09:45
On Direct and Indirect Information in Distributed Protocols (abstract)
09:00-10:30 Session 120C (GuttmanFest)
Location: Ullmann 200
09:00
Security Protocols as Choreographies
PRESENTER: Alessandro Bruni
09:30
How to Explain Security Protocols to Your Children
09:50
Secure Key Management Policies in Strand Spaces
PRESENTER: Riccardo Focardi
10:10
Verifying a Blockchain-Based Remote Debugging Protocol for Bug Bounty
PRESENTER: Pierpaolo Degano
09:00-10:30 Session 120D: Model Counting: Applications (MC)
Location: Ullmann 302
09:00
Quantifying Software Reliability via Model-Counting (abstract)
PRESENTER: Samuel Teuber
09:30
Stochastic Constraint Optimisation with Applications in Network Analysis (abstract)
PRESENTER: Anna Latour
10:00
Rushing and Strolling among Answer Sets - Navigation Made Easy (abstract)
09:00-10:30 Session 120E (NSV)
Location: Ullmann 308
09:00
Recent advances for hybrid systems verification with HyPro (abstract)
10:00
MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types (abstract)
09:00-10:30 Session 120F (PAAR)
Location: Ullmann 205
09:00
Training ENIGMAs, CoPs, and other thinking creatures (abstract)
10:00
QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers (abstract)
09:00-10:30 Session 120G: Parallel algorithms (PDAR)
Location: Ullmann 303
09:00
Isabelle LLVM Parallel (abstract)
09:45
A Linear Parallel Algorithm to Compute Strong and Branching Bisimilarity (abstract)
09:00-10:30 Session 120H: Invited talk #1 (SMT)
Location: Ullmann 311
09:00
Local Search for Bit-Precise Reasoning and Beyond (abstract)
10:00
Trail saving in SMT (abstract)
PRESENTER: Milan Banković
09:00-10:30 Session 120I (SYNT)
Location: Ullmann 201
09:00
Inductive and Parameter Synthesis to Find POMDP Controllers
10:00
Towards Synthesis in Superposition (abstract)
PRESENTER: Petra Hozzová
10:15
LTL Synthesis with Transformer Neural Networks (abstract)
PRESENTER: Frederik Schmitt
09:00-10:30 Session 120J: SMT & Automated Deduction (University Level) (ThEdu)
Location: Ullmann 306
09:00
On Exams with the Isabelle Proof Assistant (abstract)
09:30
Invited Talk: Satisfiability Modulo Theories in an Undergraduate Class (abstract)
09:00-10:00 Session 120K (WOLVERINE)

Keynote presentation

Location: Ullmann 202
09:00
Artificial Intelligence (abstract)
09:00-10:30 Session 120L (WST)
Location: Ullmann 309
09:00
Tuple Interpretations and Applications to Higher-Order Runtime Complexity (abstract)
PRESENTER: Deivid Vale
09:30
A transitive HORPO for curried systems (abstract)
PRESENTER: Liye Guo
10:00
Approximating Relative Match-Bounds (abstract)
PRESENTER: Dieter Hofbauer
09:05-10:25 Session 121 (iPRA)
Location: Ullmann 203
09:05
Uniform Interpolants and Model Completions in Formal Verification of Infinite-State Systems (abstract)
10:05
Interpolation via Finitely Subdirectly Irreducible Algebras (abstract)
PRESENTER: Wesley Fussner
09:10-10:30 Session 122: Isabelle 1 (Isabelle)
Location: Ullmann 101
09:10
Welcome
09:20
Auxiliary tools for Combinatorics on Words (abstract)
PRESENTER: Stepan Holub
09:35
Transfer and reversal of lists (abstract)
PRESENTER: Martin Raška
10:00
Oracle Integration of Floating-Point Solvers with Isabelle (abstract)
PRESENTER: Olle Torstensson
09:15-10:30 Session 123A (ARQNL)
Chair:
Location: Ullmann 104
09:15
Advances and Challenges in the Development and Application of Forgetting Tools (abstract)
09:15-10:30 Session 123B: Keynote Presentation (FCS)
Location: Ullmann 310
09:15
Computer-aided Verification and Automated Synthesis of Cryptographic Protocols (abstract)
09:30-10:30 Session 124B: Keynote Talk (PERR)

Title: Regression verification of unbalanced recursive functions with multiple calls

Speaker:  Chaked R.J.Sayedoff  and Ofer Strichman ,  Technion, Israel

Abstract: Given two programs p1 and p2, typically two versions of the sameprogram, the goal of \emph{regression verification} is to mark pairs offunctions from p1 and p2 that are equivalent, given a definitionof equivalence. The most common definition is that of \emph{partialequivalence}, namely that the two functions emit the same output if theyare fed with the same input and they both terminate. The strategy usedby the Regression Verification Tool (RVT) is to progress bottom up onthe call graphs of P1,P2, abstract those functions that were alreadyproven to be equivalent with uninterpreted functions, turn loops intorecursion, and abstract the recursive calls also with uninterpretedfunctions. This enables it to create verification conditions in the formof small programs that are loop- and recursion-free. This method workswell for recursive functions as long as they are in sync, and typicallyfails otherwise. In this work we study the problem of provingequivalence when the two recursive functions are not in sync.Effectively we extend  previous work that studied this problem forfunctions with a single recursive call site, to the general case. Wealso introduce a method for detecting automatically the unrolling thatis necessary for making two recursive functions synchronize, whenpossible. We show examples of pairs of functions with multiple recursivecalls that can now be proven equivalent with our method, but cannot beproven equivalent with any other automated verification system.

Location: Ullmann 305
09:30
Regression verification of unbalanced recursive functions with multiple calls (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 125A (ARQNL)
Chair:
Location: Ullmann 104
11:00
Towards a Coq formalization of a quantified modal logic (abstract)
11:30
Reasoning in Non-normal Modal Description Logics (abstract)
PRESENTER: Andrea Mazzullo
12:00
Intuitionistic derivability in Anderson's variant of the ontological argument (abstract)
11:00-12:30 Session 125B: Model Checking (I) (DSV)
Location: Ullmann 300
11:00
Eldarica and TriCera: towards an open verification framework (abstract)
11:45
C2C-trans as a design methodology for software verification tools (abstract)
11:00-11:45 Session 125C: Blockchain and Real-world Security (FCS)
Location: Ullmann 310
11:00
A Preview to HoRStify: Sound Security Analysis of Smart Contracts (abstract)
PRESENTER: Sebastian Holler
11:15
Automatic Fair Exchanges (abstract)
11:30
Towards Unlinkable Smartcard-based Payments: an extended abstract (abstract)
PRESENTER: Semen Yurkov
11:00-12:30 Session 125D: Formal Methods for Smart Contracts (FMBC)
Location: Ullmann 307
11:00
Finding smart contract vulnerabilities with ConCert's property-based testing framework (abstract)
PRESENTER: Eske Hoy Nielsen
11:30
Automatic generation of attacker contracts in Solidity (abstract)
12:00
Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (abstract)
12:15
FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (abstract)
PRESENTER: Aurélien Saue
11:00-12:30 Session 125E (FRIDA)
Location: Ullmann 102
11:00
Quorum Tree Abstractions of Consensus Protocols (abstract)
11:45
What's Decidable about Causally Consistent Shared Memory? (abstract)
11:00-12:40 Session 125F (GuttmanFest)
Location: Ullmann 200
11:00
On the Complexity of Verification of Time-Sensitive Distributed Systems
11:30
Protocol Analysis with Time and Space
PRESENTER: Santiago Escobar
12:00
Probabilistic annotations for protocol models
12:20
Securing Node-RED Applications
11:00-12:30 Session 125G: Isabelle 2 (Isabelle)
Location: Ullmann 101
11:00
A Verified Implementation of B-trees in Isabelle/HOL (abstract)
PRESENTER: Niels Mündler
11:30
On Axiomatic Systems for Classical Propositional Logic (abstract)
11:50
On Termination for Hybrid Tableaux (abstract)
12:10
Lessons of Teaching Formal Methods with Isabelle (abstract)
11:00-12:30 Session 125H: Model Counting: Applications & Experiments (MC)
Location: Ullmann 302
11:00
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (abstract)
PRESENTER: Andreas Gittis
11:20
Generating Random Weighted Model Counting Instances: An Empirical Analysis with Varying Primal Treewidth (abstract)
11:50
Extending Partially Directed Graphs and Determine the Size of their Markov Equivalence Class (abstract)
11:00-12:30 Session 125I (NSV)
Location: Ullmann 308
11:00
Combining learning-based methods and temporal logic specifications for designing controllers for unknown environments (abstract)
12:00
Verified Numerical Methods for Ordinary Differential Equations (abstract)
PRESENTER: Ariel Kellison
11:00-12:30 Session 125J (PAAR)
Location: Ullmann 205
11:00
A Two-Watched Literal Scheme for First-Order Logic (abstract)
PRESENTER: Lorenz Leutgeb
11:30
Lazy Paramodulation in Practice (abstract)
PRESENTER: Cezary Kaliszyk
12:00
Empirical Properties of Term Orderings for Superposition (abstract)
11:00-12:30 Session 125K: Parallel SAT solving (PDAR)
Location: Ullmann 303
11:00
Leveraging GPUs for Parallel SAT Solving (abstract)
11:45
Dealing With Uncertainty Between Peers and Having the Best of Times With Distributed Systems (abstract)
11:00-12:30 Session 125L: Research Papers (PERR)
Location: Ullmann 305
11:00
Compositional Approaches to Games in Model Checking (abstract)
11:30
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract) (abstract)
PRESENTER: Yu-Yang Lin
12:00
Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems (abstract)
PRESENTER: Kasper Hagens
11:00-12:30 Session 125M: Arithmetics and higher-order reasoning (SMT)
Location: Ullmann 311
11:00
Bit-Precise Reasoning via Int-Blasting (abstract)
PRESENTER: Yoni Zohar
11:20
An SMT Approach for Solving Polynomials over Finite Fields (abstract)
PRESENTER: Thomas Hader
11:40
On Satisfiability of Polynomial Equations over Large Prime Fields (abstract)
PRESENTER: Lucas Vella
12:00
Goose: A Meta Solver for Deep Neural Network Verification (abstract)
PRESENTER: Joseph Scott
11:00-12:30 Session 125N (SYNT)
Location: Ullmann 201
11:00
Beyond Counterexamples: Satisfiability and Synthesis Modulo Oracles (abstract)
12:00
Complexity of Relational Query Synthesis (abstract)
PRESENTER: Aalok Thakkar
12:15
Interactive Debugging of Concurrent Programs under Relaxed Memory Models (abstract)
PRESENTER: Subhajit Roy
11:00-12:30 Session 125P: Proof Tree Builder & Rule Based ATP (ThEdu)
Location: Ullmann 306
11:00
A Proof Tree Builder for Sequent Calculus and Hoare Logic (abstract)
11:30
Rule Based Geometry Automated Theorem Provers (abstract)
PRESENTER: Pedro Quaresma
11:00-12:00 Session 125Q (WOLVERINE)

Table hosts presenting an overview of the topic that will be discussed in their table. 

Location: Ullmann 202
11:00
Safe Reinforcement Learning (abstract)
11:20
Explainable Artificial Intelligence (abstract)
11:40
Robustness of Neural Networks (abstract)
11:00-12:30 Session 125R (WST)
Location: Ullmann 309
11:00
CeTA — Efficient Certification of Termination Proofs (abstract)
12:00
Hydra Battles and AC Termination (abstract)
PRESENTER: Aart Middeldorp
11:00-12:20 Session 125S (iPRA)
Location: Ullmann 203
11:00
Interpolation and Completeness in the Modal Mu-Calculus (abstract)
12:00
When iota Meets lambda (abstract)
PRESENTER: Michal Zawidzki
12:00-12:30 Session 126A: Secure Hardware (FCS)
Location: Ullmann 310
12:00
Unveiling Security through Obscurity Approach of Intel TDX Remote Attestation (abstract)
12:15
pi_RA: A pi-calculus for verifying protocols that use remote attestation (abstract)
PRESENTER: Emiel Lanckriet
12:00-12:30 Session 126B (WOLVERINE)

Round-table discussions -- part I

Location: Ullmann 202
12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:30 Session 127A (ARQNL)
Chair:
Location: Ullmann 104
14:00
Do Lawyers Use Automated Reasoning? (abstract)
15:00
(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems (abstract)
14:00-15:30 Session 127B: Model Checking (II) and Synthesis (DSV)
Location: Ullmann 300
14:00
Solving Constrained Horn Clauses Lazily and Incrementally (abstract)
14:45
Interaction Models vs. Formal Models: Synthesis Co-Design (abstract)
14:00-14:45 Session 127C: Analysis for Security and Privacy (FCS)
Location: Ullmann 310
14:00
VeNuS: Neural Network Robustness Specifications via Verifier-guided Optimization (abstract)
PRESENTER: Anan Kabaha
14:15
Compositional Higher-order Declassification Using Logical Relations (abstract)
PRESENTER: Jan Menz
14:30
Robust Indistinguishability (abstract)
PRESENTER: Adam O'Neill
14:00-15:15 Session 127D: Formal Methods for Blockchain Protocols (FMBC)
Location: Ullmann 307
14:00
Proofgold: Blockchain for Formal Methods (abstract)
PRESENTER: Cezary Kaliszyk
14:30
A Domain Specific Language for Testing Consensus Implementations (abstract)
14:45
Determinism of ledger updates (abstract)
15:00
Human and machine-readable models of state machines for the Cardano ledger (abstract)
PRESENTER: Andre Knispel
14:00-15:30 Session 127E (FRIDA)
Location: Ullmann 102
14:00
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 (abstract)
14:45
Eliminating Message Counters in Threshold Automata (abstract)
14:00-15:30 Session 127F (GuttmanFest)
Chair:
Location: Ullmann 200
14:00
Joshua Guttman: Pioneering Strand Spaces
14:20
Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran
14:40
Principles of Remote Sattestation
15:00
Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer
PRESENTER: Prajna Bhandary
14:00-15:30 Session 127G: Isabelle 3 (Isabelle)
Location: Ullmann 101
14:00
Isabelle/VSCode and Electron/Node.js as emerging Isabelle technologies (abstract)
14:30
Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode (abstract)
PRESENTER: Bernhard Stöger
15:00
A Linter for Isabelle: Implementation and Evaluation (abstract)
PRESENTER: Fabian Huch
14:00-15:30 Session 127H: Algorithms & Complexity (MC)
Location: Ullmann 302
14:00
Heuristic computation of exact treewidth - some improvements and more experimental evaluations (abstract)
14:30
Counting Complexity for Projected Reasoning in Abstract Argumentation (abstract)
15:00
A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth (abstract)
14:00-15:30 Session 127I (NSV)
Location: Ullmann 308
14:00
Motion planning with temporal logic constraints and preferences (abstract)
15:00
Neural Network Precision Tuning Using Stochastic Arithmetic (abstract)
PRESENTER: Quentin Ferro
14:00-15:30 Session 127J (PAAR)
Location: Ullmann 205
14:00
Exploring Partial Models with SCL (abstract)
PRESENTER: Simon Schwarz
14:30
On SGGS and Horn Clauses (abstract)
15:00
Exploring Representation of Horn clauses using GNNs (abstract)
PRESENTER: Chencheng Liang
14:00-15:30 Session 127K: Parallel Theorem Proving & SAT solving (PDAR)
Chair:
Location: Ullmann 303
14:00
Goéland : A Concurrent Tableau-Based Theorem Prover (abstract)
14:45
Structural Parameter Based Parallel Algorithms for Partially Weighted MaxSAT (abstract)
14:00-15:00 Session 127L: Research Papers (PERR)
Location: Ullmann 305
14:00
Implementing a Path Based Equivalence Checker for Petri net based Models of Programs (abstract)
14:30
Generating Mutation Tests Using an Equivalence Prover (abstract)
14:00-15:30 Session 127N (SYNT)
Location: Ullmann 201
14:00
Reactive Synthesis of LTL specifications with Rich Theories (abstract)
PRESENTER: Andoni Rodriguez
14:20
Regex+: Synthesizing Regular Expressions from Positive Examples (abstract)
14:40
Inferring Environment Assumptions in Model Refinement (abstract)
15:00
A Framework for Transforming Specifications in Reinforcement Learning (abstract)
15:20
SYNTCOMP Results
14:00-15:30 Session 127P: Proofs in Education (High-School Level) (ThEdu)
Location: Ullmann 306
14:00
Invited Talk: Computer-assisted proofs and automated methods in Mathematics Education (abstract)
15:00
A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year (abstract)
PRESENTER: Pedro Quaresma
14:00-14:30 Session 127Q (WOLVERINE)

Round-table discussions -- part II

Location: Ullmann 202
14:00-15:30 Session 127R (WST)
Location: Ullmann 309
14:00
A Calculus for Modular Non-Termination Proofs by Loop Acceleration (abstract)
PRESENTER: Carsten Fuhs
14:30
Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (abstract)
PRESENTER: Jürgen Giesl
15:00
Improved Automatic Complexity Analysis of Integer Programs (abstract)
PRESENTER: Nils Lommen
14:00-15:20 Session 127S (iPRA)
Location: Ullmann 203
14:00
Interpolants and Transformational Proof Systems (abstract)
15:00
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification (abstract)
PRESENTER: Philipp Wendler
15:30-16:00Coffee Break
16:00-17:30 Session 131A (ARQNL)
Chair:
Location: Ullmann 104
16:00
Advancing Automated Theorem Proving for the Modal Logics D and S5 (abstract)
16:30
Automated verification of deontic correspondences in Isabelle/HOL - First results (abstract)
PRESENTER: Xavier Parent
17:00
Solving QMLTP Problems by Translation to Higher-order Logic (abstract)
PRESENTER: Geoff Sutcliffe
16:00-17:30 Session 131B: Industrial Use of Formal Methods (DSV)
Location: Ullmann 300
16:00
Formal Verification of Ethereum Smart Contracts: SMT-Based Approaches and Challenges (abstract)
16:45
Achieving Verified Cloud Authorization (abstract)
16:00-16:45 Session 131C: Formal Methods for 2nd Layers/off-chain Protocols (FMBC)
Location: Ullmann 307
16:00
Multi: a Formal Playground for Smart Multi-contract interaction (abstract)
PRESENTER: Martin Ceresa
16:30
Automating Security Analysis of Off-Chain Protocols (abstract)
PRESENTER: Sophie Rain
16:00-17:30 Session 131E: Isabelle 4 (Isabelle)
Location: Ullmann 101
16:00
Gale-Shapley Verified (abstract)
16:30
From P != NP to monotone circuits of super-polynomial size (abstract)
17:00
Automating Kantian Ethics in Isabelle: A Case Study (abstract)
16:00-17:30 Session 131F: Sampling and First Order (MC)
Location: Ullmann 302
16:00
Recursive Solutions to First-Order Model Counting (abstract)
PRESENTER: Paulius Dilkas
16:30
Scalable Uniform Sampling via Efficient Knowledge Compilation (abstract)
PRESENTER: Yong Lai
17:00
Designing Samplers is Easy: The Boon of Testers (abstract)
PRESENTER: Priyanka Golia
16:00-17:00 Session 131G (NSV)
Location: Ullmann 308
16:00
Adversarial Testing and Repair for Neural Network based Control Systems using Optimization (abstract)
16:00-17:30 Session 131H (PAAR)
Location: Ullmann 205
16:00
Optimal Strategy Schedules for Everyone (abstract)
16:30
The Vampire Approach to Induction (abstract)
PRESENTER: Marton Hajdu
17:00
Reuse of Introduced Symbols in Automatic Theorem Provers (abstract)
PRESENTER: Michael Rawson
16:00-17:00 Session 131J: Invited Talk (PERR)

Title: Compositional relational reasoning via operational game semantics

Andrzej Murawski (University of Oxford)

Abstract: We use operational game models as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages,with either general or ground-type references and with either call/cc or no control operator. In game semantics, the differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.

The proposed technique, which we call Kripke Normal-Form Bisimulations, combines insights from normal-form bisimulation and Kripke-style logical relations with game semantics. In particular, the role of the heap is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, where applicable.

The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, the framework developed in the paper sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.

 

This is joint work with Guilhem Jaber (Universite de Nantes).

 

Location: Ullmann 305
16:00
Compositional relational reasoning via operational game semantics (abstract)
16:00-17:00 Session 131L (SYNT)
Location: Ullmann 201
16:00
SyGuS-IF + SemGuS Results
16:10
Future Work and Open Challenges Panel – Authors+Chairs
16:00-17:00 Session 131N (WST)

Business Meeting (WST 2022)

Location: Ullmann 309
16:00-17:20 Session 131P (iPRA)
Location: Ullmann 203
16:00
Application of Interpolation in Networks (abstract)
17:00
Interpolants and Interference (abstract)
18:00-19:30Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event
Friday, August 12th

View this program: with abstractssession overviewtalk overview

08:30-09:00Coffee & Refreshments
09:00-10:30 Session 134A (GuttmanFest)
Location: Taub 6
09:00
Model Finding for Exploration
09:30
On Orderings in Security Models
10:00
Benign Interaction of Security Domains
PRESENTER: Flemming Nielson
09:00-10:30 Session 134B (PAAR)
Location: Taub 7
09:00
The Logic Languages of the TPTP World and Proofs and Models in the TPTP World (abstract)
10:00
Automated Reasoning in Non-classical Logics in the TPTP World (abstract)
PRESENTER: Alexander Steen
09:00-10:30 Session 134C: 1st invited talk and paper presentation (SC^2)
Location: Taub 3
09:00
Non-Linear Real Arithmetic with Transcendental Function Symbols: Undecidable but Easy? (abstract)
10:00
Cylindrical Algebraic Coverings for Quantifiers (abstract)
PRESENTER: Gereon Kremer
09:00-10:30 Session 134D: Celebrating 20 years of the SMT workshop (SMT)
Location: Taub 2
09:00
Panel discussion "SMT: Past, Present and Future"
PRESENTER: Cesare Tinelli
10:00
CDSAT for nondisjoint theories with shared predicates: arrays with abstract length (abstract)
09:00-10:30 Session 134E (VeriProp)
Location: Taub 9
09:00
Probabilistic Hyperproperties (abstract)
09:50
Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games (abstract)
PRESENTER: Ichiro Hasuo
10:10
Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics (abstract)
PRESENTER: Thom Badings
09:30-10:30 Session 135B: Invited talk (UNIF)
Location: Taub 8
09:30
Unification types in modal logics (abstract)
10:00-10:30 Session 136 (WST)
Location: Taub 4
10:00
The Termination Competition (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 137A: Automation and Tooling (Coq)
Location: Taub 5
11:00
Trakt: a generic pre-processing tactic for theory-based proof automation (abstract)
PRESENTER: Enzo Crance
11:30
10 Years of Superlinear Slowness in Coq (abstract)
PRESENTER: Jason Gross
12:00
Autogenerating Natural Language Proofs (abstract)
PRESENTER: Seth Poulsen
11:00-12:30 Session 137B (GuttmanFest)
Location: Taub 6
11:00
A Declaration of Software Independence
PRESENTER: Peter Y A Ryan
11:30
A Tutorial-Style Introduction to DY*
PRESENTER: Guido Schmitz
11:50
Establishing the Price of Privacy in Federated Data Trading
PRESENTER: Kangsoo Jung
12:10
Prototyping Formal Methods Tools: a Protocol Analysis Case Study
PRESENTER: Abigail Siegel
11:00-12:30 Session 137C (PAAR)
Location: Taub 7
11:00
Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving (abstract)
11:30
An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning (abstract)
12:00
The Isabelle Community Benchmark (abstract)
PRESENTER: Fabian Huch
11:00-12:30 Session 137D: Paper presentations (SC^2)
Location: Taub 3
11:00
NP: SMT-Solving Combinatorial Inequalities (abstract)
PRESENTER: Ali Kemal Uncu
11:30
Decidability of difference logics with unary predicates (abstract)
PRESENTER: Baptiste Vergain
12:00
Automatic Deployment of Component-based Applications in the Cloud (abstract)
11:00-12:30 Session 137E: Theories and Proofs (SMT)
Chair:
Location: Taub 2
11:00
User-Propagators for Custom Theories in SMT Solving (abstract)
11:20
An SMT-LIB Theory of Heaps (abstract)
PRESENTER: Zafer Esen
11:40
Challenges and Solutions for Higher-Order SMT Proofs (abstract)
PRESENTER: Mikolas Janota
12:00
A simple proof format for SMT (abstract)
PRESENTER: Jochen Hoenicke
11:00-12:30 Session 137F (UNIF)
Location: Taub 8
11:00
Higher-Order Unification with Definition by Cases (abstract)
PRESENTER: David Cerna
11:30
Higher-order unification from E-unification with second-order equations and parametrised metavariables (abstract)
12:00
Nominal Anti-Unification of Letrec-Expressions (abstract)
11:00-12:30 Session 137G (VeriProp)
Location: Taub 9
11:00
Distribution Testing and Probabilistic Programming: A Match made in Heaven (abstract)
11:50
A Quantitative Verification Infrastructure (abstract)
12:10
Inferring Expected Runtimes and Sizes (abstract)
PRESENTER: Eleanore Meyer
11:00-12:30 Session 137H (WST)
Location: Taub 4
11:00
Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (abstract)
PRESENTER: Eleanore Meyer
11:20
LoAT: The Loop Acceleration Tool (abstract)
PRESENTER: Florian Frohn
11:40
AProVE 2022 (abstract)
PRESENTER: Jürgen Giesl
12:00
The System SOL version 2022 (Tool Description) (abstract)
PRESENTER: Makoto Hamana
12:20
Things WANDA cannot do (abstract)
12:30-14:00Lunch Break

Lunches will be held in Taub hall.

14:00-15:30 Session 138A: Presenting and Working with Coq Code (Coq)
Location: Taub 5
14:00
jsCoq: Literate Proof Documents Dressed for the Web
15:00
HenBlocks: Structured Editing for Coq (abstract)
PRESENTER: Bernard Boey
14:00-15:30 Session 138B (GuttmanFest)
Chair:
Location: Taub 6
14:00
Three Branches of Accountability
14:30
Adapting constraint solving to automatically analyze UPI Protocols
14:50
Quantum Machine Learning and Fraud Detection
15:10
Formal Methods and Mathematical Intuition
14:00-15:35 Session 138C (PAAR)
Location: Taub 7
14:00
short COST action EuroProofNet introduction
14:05
EuroProofNet presentation on proofs in Dedukti
14:50
EuroProofNet presentation on SMT and proofs
14:00-15:30 Session 138D: 2nd invited talk and paper presentation (SC^2)
Location: Taub 3
14:00
Computer algebra and automation in Lean's mathematical library (abstract)
15:00
Enumerating Projective Planes of Order Nine with Proof Verification (abstract)
PRESENTER: Daniel Dallaire
14:00-15:30 Session 138F: Invited talk (UNIF)
Location: Taub 8
14:00
Unification Decision Procedures using Basic Narrowing modulo an Equational Theory
15:00
Fuzzy Order-Sorted Feature Term Unification (abstract)
14:00-15:30 Session 138G (VeriProp)
Location: Taub 9
14:00
Quantifying Leakage in Privacy Risk Analysis using Probabilistic Programming
14:50
Deterministic stream-sampling for probabilistic programming: semantics and verification (abstract)
PRESENTER: William Smith
15:10
Probabilistic Guarded Kleene Algebra with Tests (abstract)
14:00-15:30 Session 138H (WST)
Location: Taub 4
14:00
CeTA – A certifier for termCOMP 2022 (abstract)
PRESENTER: René Thiemann
14:20
Certified Matchbox (abstract)
14:35
MultumNonMulta at termCOMP 2022 (abstract)
14:55
Runtime complexity of parallel-innermost term rewriting at TermComp 2022 (abstract)
15:15
DEPP (abstract)
PRESENTER: Aart Middeldorp
15:30-16:00Coffee Break
16:00-16:30 Session 139B: Paper presentation (SC^2)
Location: Taub 3
16:00
An SC-Square Approach to the Minimum Kochen–Specker Problem (abstract)
PRESENTER: Zhengyu Li
16:00-17:00 Session 139D (UNIF)
Location: Taub 8
16:00
Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report) (abstract)
16:30
Restricted Unification in the Description Logic FLbot (abstract)
16:00-17:15 Session 139E (VeriProp)
Location: Taub 9
16:00
Uncertainty propagation in discrete-time systems using probabilistic forms (abstract)
16:50
Verifying Probabilistic Programs using Generating Functions (abstract)