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)
Chair:
Location: Ullmann 308
| 09:00 | Tutorial: Belief Change, Ontology Repair and Evolution (Part 1) (abstract) |
09:00-10:00 Session 1B (DECFOML)
Chair:
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.
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Ullmann 310
| 09:00 | Constraint modelling and solving: Learning from observing people (abstract) |
09:00-09:50 Session 1I (VardiFest)
Chair:
Location: Taub 1
| 09:00 | On the unusual effectiveness of automata in logic (abstract) |
09:00-10:30 Session 1J (WiL)
Chair:
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.
Chair:
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
Chair:
Location: (virtual only)
| 09:30 | Exact Separation Logic (abstract) |
09:30-10:30 Session 3B: Invited Talk (WPTE)
Chair:
Location: Ullmann 305
| 09:30 | Transforming Text to (and from) XML (abstract) |
09:40-10:30 Session 4: Paper presentations (ModRef)
Chair:
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)
Chair:
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)
Chair:
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
Chair:
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)
Chair:
Location: Ullmann 308
| 11:00 | Tutorial: Belief Change, Ontology Repair and Evolution (Part 2) (abstract) |
11:00-12:00 Session 10B (DECFOML)
Chair:
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.
Chair:
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.
Chair:
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)
Chair:
Location: Ullmann 303
| 11:00 | TBA |
| 12:00 | Elementary Simplicial Collapses in Cubical Agda |
11:00-12:30 Session 10G (IFIP-WG1.6)
Chair:
Location: Ullmann 306
| 11:00 | Quantitative Weak Linearisation (abstract) |
| 12:00 | The International School on Rewriting (abstract) PRESENTER: Johannes Waldmann |
11:00-12:30 Session 10H: learning interpretable ML models (LMML)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Júlia Pukancová |
| 12:00 | Modular Provenance in Multi-Context Systems (abstract) PRESENTER: Matthias Knorr |
11:35-12:05 Session 11 (VardiFest)
Chair:
Location: Taub 1
| 11:35 | On the Extraordinary Effectiveness of Logic in Strategic Reasoning (abstract) |
| 11:45 | Automated Synthesis of Mechanisms (abstract) PRESENTER: Munyque Mittelmann |
| 11:55 | Synthesis of plans for teams of manufacturing robots (abstract) |
12:10-12:40 Session 12A (DECFOML)
Chair:
Location: Ullmann 104
| 12:10 | The Quantified Reflection Calculus as a Modal Logic (abstract) PRESENTER: Ana de Almeida Borges |
12:10-12:40 Session 12B (VardiFest)
Chair:
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)
Chair:
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
Chair:
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
Chair:
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) PRESENTER: Athénaïs Vaginay |
| 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/
Chair:
Location: Ullmann 200
| 14:00 | Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (abstract) |
14:00-14:30 Session 14D (DECFOML)
Chair:
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.
Chair:
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) PRESENTER: Jørgen Villadsen |
| 14:45 | SIVA: Simulation and visualization of the DL tableau algorithm (abstract) PRESENTER: Júlia Pukancová |
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Ullmann 310
| 14:00 | A Constraint-Based Tool for Generating Benchmark Instances (abstract) |
14:00-15:30 Session 14K (PC)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Ilina Stoilkovska |
14:00-15:30 Session 14R (XLoKR)
XLoKR Session 3
Chair:
Location: Ullmann 202
| 14:00 | On interactive explanations as reasoning (abstract) PRESENTER: Guilherme Paulino-Passos |
| 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)
Chair:
Location: Ullmann 104
| 14:30 | From Modal Logic to Fluted logic (abstract) |
14:30-15:30 Session 15B (TLLA-LINEARITY)
Chair:
Location: Ullmann 302
| 14:30 | Recursive Session Logical Relations (abstract) |
14:50-15:30 Session 17 (VardiFest)
Chair:
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
Chair:
Location: (virtual only)
| 15:00 | Proving Logical Atomicity using Lock Invariants (abstract) PRESENTER: Shengyi Wang |
| 15:30 | Deciding Separation Logic with Heap Lists (abstract) PRESENTER: Mihaela Sighireanu |
| 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
Chair:
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
Chair:
Location: Ullmann 200
| 16:00 | Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (abstract) |
16:00-16:30 Session 19C (DECFOML)
Chair:
Location: Ullmann 104
| 16:00 | Decidable Fragments of Term Modal Logic (abstract) |
16:00-17:00 Session 19D (FoMLAS)
FoMLAS Session 4
Chair:
Location: Ullmann 201
| 16:00 | Counter-Example Guided Neural Network Compression Refinement (CEG4N) (abstract) PRESENTER: João Batista Pereira Matos Júnior |
| 16:30 | Goal-Aware RSS for Complex Scenarios via Program Logic (abstract) |
16:00-17:30 Session 19E (HoTT/UF)
Chair:
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 19G: verification of black-box ML models (LMML)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Ullmann 203
| 16:00 | The Tournament Fixing Problem (abstract) |
16:00-17:30 Session 19K (TLLA-LINEARITY)
Chair:
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)
Chair:
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) PRESENTER: Stefania Costantini |
16:00-17:30 Session 19M: Talks (3) (WPTE)
Chair:
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) PRESENTER: Christopher Brown |
| 16:45 | Refactoring Steps for P4 (work in progress) (abstract) PRESENTER: Máté Tejfel |
16:00-17:00 Session 19N (WiL)
Chair:
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)
Chair:
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
Chair:
Location: Taub 1
| 17:10 | On how the past illuminates the future (abstract) |
17:15-18:15 Session 23: Discussion and Open Problems (PCCR)
Open problem session and discussions.
Chair:
Location: Ullmann 203
17:30-18:30 Session 24A: CAUSAL and EELP (ASPOCP)
CAUSAL and EELP
Chair:
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 PRESENTER: Stefania Costantini |
17:30-19:00 Session 24C (LogTeach)
Chair:
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
Chair:
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.
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Ullmann 311
| 09:00 | Towards an Efficient CNF Encoding of Block Ciphers (abstract) PRESENTER: Daniel Waszkiewicz |
| 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)
Chair:
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
Chair:
Location: Ullmann 101
| 09:00 | A Computational Interpretation of Girard’s Intuitionistic Proof-Nets (abstract) |
09:00-09:50 Session 26K (VardiFest)
Chair:
Location: Taub 1
| 09:00 | On the Effectiveness of Logic in Robotics (abstract) |
09:00-10:30 Session 26L: Doctoral Program (CP)
Chair:
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) PRESENTER: Augustin Delecluse |
| 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
Chair:
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
Chair:
Location: Ullmann 305
| 09:30 | Online Reasoning under Uncertainty with the Event Calculus (abstract) PRESENTER: Alexander Artikis |
09:30-10:30 Session 28C (TLLA-LINEARITY)
Chair:
Location: Ullmann 302
| 09:30 | A coherent differential PCF (abstract) |
09:50-10:30 Session 29 (VardiFest)
Chair:
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.
Chair:
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)
Chair:
Location: Ullmann 303
| 11:00 | Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability PRESENTER: Jonathan Weinberger |
| 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)
Chair:
Location: Ullmann 306
| 11:00 | Seven Confluence Criteria for Solving COPS #20 (abstract) |
| 12:00 | Formalized Signature Extension Results for Equivalence (abstract) PRESENTER: Fabian Mitterwallner |
11:00-12:30 Session 31E (LFMTP)
Workshop papers
Chair:
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) PRESENTER: Thomas Traversié |
11:00-12:30 Session 31F (LogTeach)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Kilian Rueckschloss |
11:00-12:30 Session 31K: SAT and Parallel Solving (POS)
Chair:
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) PRESENTER: Hidetomo Nabeshima |
| 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)
Chair:
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
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Felix Ulrich-Oltean |
| 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)
Chair:
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)
Chair:
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
Chair:
Location: Ullmann 104
Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 1) (abstract) |
14:00-15:30 Session 34B (FoMLAS)
FoMLAS Session 7
Chair:
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.
Chair:
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) PRESENTER: Sarat Chandra Varanasi |
| 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) PRESENTER: Sarat Chandra Varanasi |
14:00-15:30 Session 34D (HoTT/UF)
Chair:
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)
Chair:
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
Chair:
Location: Taub 3
| 14:00 | A modal analysis of dependently typed metaprogramming (abstract) |
14:00-15:30 Session 34G (LogTeach)
Chair:
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) PRESENTER: Frederik Krogsdal Jacobsen |
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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
Chair:
Location: Ullmann 101
| 14:00 | PBPO+ Graph Rewriting in Context (abstract) |
14:00-15:30 Session 34P (TLLA-LINEARITY)
Chair:
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)
Chair:
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)
Chair:
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
Chair:
Location: Taub 3
| 15:00 | Associativity or Non-Associativity, Local or Global! (abstract) PRESENTER: Eben Blaisdell |
15:00-15:40 Session 35B (VardiFest)
Chair:
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
Chair:
Location: Ullmann 104
Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 2) (abstract) |
16:00-17:00 Session 37B (FoMLAS)
FoMLAS Session 8
Chair:
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).
Chair:
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)
Chair:
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
Chair:
Location: Taub 3
| 16:00 | Reasoning about Specifications in LF (abstract) |
16:00-17:30 Session 37H: Panel (Nikolaj Bjørner, Christoph Haase, Liat Peterfreund) (Mentoring Workshop)
Location: Taub 7
16:00-17:30 Session 37I (PC)
Chair:
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)
Chair:
Location: Ullmann 305
| 16:00 | Explainability, causality and computational and-or graphs (abstract) |
16:00-17:00 Session 37K: Proofs II (POS)
Chair:
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
Chair:
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)
Chair:
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)
Chair:
Location: Taub 4
| 16:00 | Optimized Code Generation against Power Side Channels (abstract) PRESENTER: Rodothea Myrsini Tsoupidi |
| 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) PRESENTER: Christopher Coulombe |
| 17:26 | Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (abstract) PRESENTER: Jovial Cheukam Ngouonou |
16:45-17:05 Session 38 (VardiFest)
Chair:
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
Chair:
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)
Chair:
Location: Taub 1
| 17:00 | How to be an ethical computer scientist (Joint with Vardi Fest) (abstract) |
17:10-18:00 Session 40 (VardiFest)
Chair:
Location: Taub 1
| 17:10 | How to be an ethical computer scientist (abstract) |
18:00-19:00 Session 42: A session to honor 100 years since the birth of the late Boris (Boaz) Trakhtenbrot (FLoC)
Chair:
Location: Taub 1
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)
Chair:
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) PRESENTER: Felix Ulrich-Oltean |
| 10:00 | Improved Sample Complexity Bounds for Branch-and-Cut (abstract) PRESENTER: Siddharth Prasad |
09:00-10:30 Session 44B: Theory (CP)
Chair:
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)
Chair:
Location: Taub 1
| 09:00 | Temporal Team Semantics Revisited (abstract) PRESENTER: Jens Oliver Gutsfeld |
| 09:15 | Deciding Hyperproperties Combined with Functional Specifications (abstract) PRESENTER: Jana Hofmann |
| 09:30 | Reasoning on Data Words over Numeric Domains (abstract) PRESENTER: Anthony Widjaja Lin |
| 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)
Chair:
| 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)
Chair:
| 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)
Chair:
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) PRESENTER: Ricardo Gonçalves |
| 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)
Chair:
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)
Chair:
Location: Churchill Auditorium
| 11:10 | Information Structures for Privacy and Fairness (abstract) |
12:10-12:40 Session 49A: Epistemic Logic (KR)
Chair:
Location: Taub 2
| 12:10 | The Topology of Surprise (abstract) PRESENTER: David Fernández-Duque |
12:10-12:40 Session 49B: Knowledge Graphs (KR)
Chair:
Location: Taub 3
| 12:10 | Open Relation Extraction With Non-existent and Multi-span Relationships (abstract) PRESENTER: Huifan Yang |
12:10-12:40 Session 49C: Application of SAT to Quantum circuits (SAT)
Chair:
| 12:10 | Towards a SAT Encoding for Quantum Circuits (abstract) PRESENTER: Robert Wille |
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)
Chair:
Location: Taub 4
| 14:00 | Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data (abstract) PRESENTER: Chaithanya Basrur |
| 14:30 | A Constraint Programming Approach to Ship Refit Project Scheduling (abstract) PRESENTER: Raphaël Boudreault |
| 15:00 | DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security (abstract) PRESENTER: Timothy Curry |
14:00-15:30 Session 50C: Semantics (FSCD)
Chair:
| 14:00 | A Fibrational Tale of Operational Logical Relations (abstract) PRESENTER: Francesco Dagnino |
| 14:30 | On Quantitative Algebraic Higher-Order Theories (abstract) PRESENTER: Paolo Pistone |
| 15:00 | Sheaf semantics of termination-insensitive noninterference (abstract) PRESENTER: Jonathan Sterling |
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.
Chair:
Location: Taub 9
14:00-15:30 Session 50E: Multi-Agent Systems (KR)
Chair:
Location: Taub 2
| 14:00 | Verification and Realizability in Finite-Horizon Multiagent Systems (abstract) PRESENTER: Senthil Rajasekaran |
| 14:30 | Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems (abstract) PRESENTER: Alison R. Panisson |
| 15:00 | Automatic Synthesis of Dynamic Norms for Multi-Agent Systems (abstract) PRESENTER: Giuseppe Perelli |
14:00-14:30 Session 50F: Doctoral Consortium (KR)
Chair:
Location: Taub 3
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)
Chair:
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) PRESENTER: Vladimir Zamdzhiev |
| 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)
Chair:
| 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)
Chair:
Location: Taub 3
15:00-15:30 Session 52A: Logic Programming & Machine Learning (ICLP)
Chair:
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)
Chair:
Location: Taub 3
15:30-16:00Coffee Break
16:00-17:30 Session 54A: OR (CP)
Chair:
Location: Taub 7
| 16:00 | Parallel Hybrid Best-First Search (abstract) PRESENTER: Simon de Givry |
| 16:30 | Sequence Variables for Routing Problems (abstract) PRESENTER: Augustin Delecluse |
| 17:00 | From Cliques to Colorings and Back Again (abstract) PRESENTER: Anthony Karahalios |
16:00-17:30 Session 54B: Tutorial + ML (CP)
16:00-17:00: Tutorial
17:00-17:30: Machine Learning
Chair:
Location: Taub 4
| 16:00 | Building a Constraint Programming Solver Guided by Machine Learning: Opportunities and Challenges (abstract) PRESENTER: Louis-Martin Rousseau |
| 17:00 | Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints (abstract) PRESENTER: Daphné Lafleur |
16:00-17:30 Session 54C: Unification and Matching (FSCD)
Chair:
| 16:00 | Combined Hierarchical Matching: The Regular Case (abstract) PRESENTER: Christophe Ringeissen |
| 16:30 | Nominal Anti-Unification with Atom-Variables (abstract) PRESENTER: Manfred Schmidt-Schauss |
| 17:00 | A Certified Algorithm for AC-Unification (abstract) PRESENTER: Daniele Nantes-Sobrinho |
16:00-17:30 Session 54D: Applications & Automatic Reasoning (ICLP)
Chair:
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)
Chair:
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) PRESENTER: David Fernández-Duque |
16:00-17:30 Session 54F: Description Logics (KR)
Chair:
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) PRESENTER: Rasmus Ejlers Møgelberg |
| 17:15 | A Type Theory for Strictly Unital Infinity-Categories (abstract) PRESENTER: Alex Rice |
16:00-17:30 Session 54H: MaxSAT (SAT)
Chair:
| 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 |
17:30-18:30 Session 55: Logic Lounge (FLoC)
Chair:
Location: Churchill Auditorium
| 17:30 | Thinking Fast and Slow in AI (abstract) |
Wednesday, August 3rd
View this program: with abstractssession overviewtalk overview
08:30-09:00Coffee & Refreshments
09:00-10:00 Session 56A: Invited Talk (zoom link: https://technion.zoom.us/j/97111314813) (CP)
Chairs:
Location: Churchill Auditorium
| 09:00 | All Questions Answered (abstract) |
09:00-10:30 Session 56B: Type Theory and Formalization (FSCD)
Chair:
| 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)
Chair:
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-09:30 Session 56D: Report Back on Dagstuhl Perspectives Workshop: Current and Future Challenges in Knowledge Representation and Reasoning (KR)
Chair:
Location: Taub 2
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)
Chair:
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)
Chair:
| 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
Chair:
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)
Chair:
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 58C: Applications: Concurrency, Quantum Computation (FSCD)
Chair:
| 11:00 | Type-Based Termination for Futures (abstract) PRESENTER: Siva Somayyajula |
| 11:30 | Addition and differentiation of ZX-diagrams (abstract) PRESENTER: Margarita Veshchezerova |
11:00-12:30 Session 58D: Semantics (ICLP)
Chair:
Location: Taub 9
| 11:00 | Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective (abstract) PRESENTER: Panos Rondogiannis |
| 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)
Chair:
Location: Taub 2
| 11:00 | Neural-Probabilistic Answer Set Programming (abstract) PRESENTER: Arseny Skryagin |
| 11:30 | Faithful Approaches to Rule Learning (abstract) PRESENTER: David Tena Cucala |
| 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)
Chair:
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) |
11:00-12:30 Session 58H: Applications + pragmatics (SAT)
Chair:
| 11:00 | A SAT Attack on Rota's Basis Conjecture (abstract) PRESENTER: Markus Kirchweger |
| 11:30 | The packing chromatic number of the infinite square grid is at least 14 (abstract) PRESENTER: Bernardo Subercaseaux |
| 12:00 | Migrating Solver State (abstract) PRESENTER: Benjamin Kiesl |
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
Chair:
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)
Chair:
| 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)
Chair:
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)
Chair:
Location: Taub 2
| 14:00 | Sum-Product Loop Programming: From Probabilistic Circuits to Loop Programming (abstract) PRESENTER: Viktor Pfanschilling |
| 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)
Chair:
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) PRESENTER: Yusuf Izmirlioglu |
| 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) PRESENTER: Emanuel Sallinger |
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.
Chair:
Location: Taub 1
14:00-15:30 Session 59G: Theory (SAT)
Chair:
| 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
Chair:
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
Chairs:
Location: Taub 7
| 16:00 | Early Career Award |
16:00-17:30 Session 61B: Lambda Calculus and Normalization/Reduction (FSCD)
Chair:
| 16:00 | Strategies for Asymptotic Normalization (abstract) PRESENTER: Giulio Guerrieri |
| 16:30 | Solvability for Generalized Applications (abstract) PRESENTER: Loïc Peyrot |
| 17:00 | Normalization without syntax (abstract) PRESENTER: Willem Heijltjes |
16:00-17:30 Session 61C: Applications (ICLP)
Chair:
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)
Chair:
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
Location: Taub floor 1 lobby
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.
Chair:
Location: Churchill Auditorium
16:00-17:30 Session 61H: Model Counting (SAT)
Chair:
| 16:00 | Proofs for Propositional Model Counting (abstract) PRESENTER: Markus Hecher |
| 16:30 | A New Exact Solver for (Weighted) Max#SAT (abstract) PRESENTER: Marie Miceli |
| 17:00 | Weighted Model Counting with Twin-Width (abstract) PRESENTER: Stefan Szeider |
17:00-18:00 Session 62A: Conditionals (KR)
Chair:
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)
Chair:
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) PRESENTER: Francois Schwarzentruber |
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)
Chair:
Location: Taub 7
| 09:00 | MDD-Based Constraint Programming in Haddock (abstract) PRESENTER: Laurent Michel |
09:00-10:30 Session 63B: SAT (CP)
Chair:
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) PRESENTER: Mohamed Sami Cherif |
09:00-10:30 Session 63C: Proof Theory and Linear Logic (FSCD)
Chair:
| 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.
Chair:
Location: Taub 9
09:00-10:30 Session 63E: Argumentation (KR)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Francesco Dagnino |
| 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
Chair:
| 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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Christopher Coulombe |
| 12:00 | Acquiring Maps of Interrelated Conjectures on Sharp Bounds (abstract) PRESENTER: Jovial Cheukam-Ngouonou |
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)
Chair:
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) PRESENTER: Stefano Sferrazza |
| 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)
Chair:
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)
Chair:
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) PRESENTER: Nikolas Mählmann |
| 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)
Chair:
| 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) PRESENTER: Jesús Giráldez-Cru |
| 12:00 | Towards Learning Quantifier Instantiation in SMT (abstract) PRESENTER: Mikolas Janota |
12:00-12:30 Session 66A: Automated Reasoning (KR)
Chair:
Location: Taub 2
| 12:00 | Automating Reasoning with Standpoint Logic via Nested Sequents (abstract) PRESENTER: Lucía Gómez Álvarez |
12:00-12:30 Session 66B: Strategic Reasoning (KR)
Chair:
Location: Taub 3
| 12:00 | Private and public affairs in strategic reasoning (abstract) PRESENTER: Aniello Murano |
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
Chair:
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
Chair:
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) PRESENTER: Joan Espasa Arxer |
| 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)
Chair:
| 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.
Chair:
Location: Taub 9
14:00-15:30 Session 67E: Systems & Robotics (KR)
Chair:
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) PRESENTER: Periklis Mantenoglou |
| 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)
Chair:
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) PRESENTER: Renata Wassermann |
| 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)
Chair:
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.
Chair:
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)
Chair:
Location: Taub 9
| 15:00 | ASP-Based Declarative Process Mining (abstract) PRESENTER: Francesco Chiariello |
| 15:15 | Implementing Stable-Unstable Semantics with ASPTOOLS and Clingo (abstract) |
15:30-16:00Coffee Break
16:00-17:00 Session 70: Plenary (FLoC)
Chair:
Location: Churchill Auditorium
| 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.
Chair:
Location: Churchill Auditorium
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
Chairs:
Location: Taub 7
09:00-10:30 Session 73B: Reasoning & Solving (ICLP)
Chair:
Location: Taub 9
| 09:00 | Stream Reasoning with Deadlines (abstract) PRESENTER: Periklis Mantenoglou |
| 09:22 | Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling (abstract) PRESENTER: Mohammed El-Kholany |
| 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)
Chair:
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) PRESENTER: Francesco Kriegel |
09:00-10:30 Session 73D: Systems & Robotics / Existential Rules (KR)
Chair:
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.
Chair:
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
Chair:
Location: Taub floor 1 lobby
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
Chair:
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)
Chair:
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) PRESENTER: George Katsirelos |
11:00-12:30 Session 76C: Rewriting (FSCD)
Chair:
| 11:00 | Polynomial Termination over N is Undecidable (abstract) PRESENTER: Fabian Mitterwallner |
| 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.
Chair:
Location: Taub 9
11:00-12:30 Session 76E: Belief Merging/Revision (KR)
Chair:
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)
Chair:
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) PRESENTER: Marie-Laure Mugnier |
11:00-12:30 Session 76G: Verification (LICS)
"Verification": 6 papers (12 min presentation + 2-3 min Q&A)
Chair:
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) PRESENTER: Philip Offtermatt |
| 11:30 | Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes (abstract) PRESENTER: Wojciech Czerwiński |
| 11:45 | Probabilistic Verification Beyond Context-Freeness (abstract) PRESENTER: Andrzej Murawski |
| 12:00 | Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification (abstract) PRESENTER: Pascal Bergsträßer |
| 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 |
11:00-12:30 Session 76I: Bryant Discoveries Day (BDD) event + Tool papers (SAT)
Chair:
| 11:00 | (BDD event) |
| 11:30 | Pedant: A Certifying DQBF Solver (abstract) PRESENTER: Franz-Xaver Reichl |
| 11:50 | QBF Programming with the Modeling Language Bule (abstract) PRESENTER: Abdallah Saffidine |
| 12:10 | OptiLog v2: Model, Solve, Tune And Run (abstract) PRESENTER: Josep Alos |
12:00-12:30 Session 77: ASP Optimization (ICLP)
Chair:
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)
Chair:
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Taub 1
| 14:00 | Separating LREC from LFP (abstract) PRESENTER: Felipe Ferreira Santos |
| 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) PRESENTER: Pascal Schweitzer |
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)
Chair:
| 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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Konstantin Schekotihin |
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)
Chair:
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:00-17:30 Session 81D: Panel (Clark Barrett, Orna Grumberg, Kristin Yvonne Rozier, Natarajan Shankar) (Mentoring Workshop)
Location: Taub 6
16:00-17:00 Session 81E: Awards / Competitions (SAT)
Awards / Competitions
Chair:
| 16:00 | Awards and Competition - II (with Live Broadcast) (abstract) |
16:30-17:30 Session 82: Panel: Past, Present and Future of Prolog (ICLP)
Panel: Past, Present and Future of Prolog
Chair:
Location: Taub 9
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
Chair:
Location: Taub 1
17:00-17:30 Session 84B: Closing (KR)
Chair:
Location: Taub 2
| 17:00 | KR 2022 Closing (abstract) PRESENTER: Gabriele Kern-Isberner |
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)
Chair:
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) PRESENTER: Đorđe Žikelić |
| 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)
Chair:
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) PRESENTER: Reynaldo Gil-Pons |
| 10:00 | A small bound on the number of sessions for security protocols (abstract) PRESENTER: Stephanie Delaune |
09:00-10:30 Session 85C: Opening and Query Answering (DL)
Chair:
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)
Chair:
| 09:00 | (Invited) Modelling and Verifying Properties of Biological Neural Networks (abstract) |
09:30-10:30 Session 87: Argumentation 1 (NMR)
Chair:
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) PRESENTER: Michael Bernreiter |
10:30-11:00Coffee Break
11:00-12:00 Session 89: Keynote (FLoC)
Chair:
Location: Churchill Auditorium
| 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)
Chair:
Location: Taub 1
| 14:00 | Shared Certificates for Neural Network Verification (abstract) PRESENTER: Dimitar I. Dimitrov |
| 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)
Chair:
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) PRESENTER: Thomas Van Strydonck |
14:00-15:30 Session 90C: Joint NMR/DL Session (1) (DL)
Chair:
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)
Chair:
| 14:00 | Candle: A Verified Implementation of HOL Light (abstract) PRESENTER: Oskar Abrahamsson |
| 14:30 | A Verified Cyclicity Checker (abstract) PRESENTER: Arve Gengelbach |
| 15:00 | Kalas: A Verified, End-to-End Compiler for a Choreographic Language (abstract) PRESENTER: Alejandro Gómez-Londoño |
14:00-15:00 Session 90E: Keynote NMR and DL (NMR)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Wael-Amine Boutglay |
| 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)
Chair:
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) PRESENTER: Sébastien Gondron |
16:00-17:30 Session 92C: Joint NMR/DL Session (2) (DL)
Chair:
Location: Taub 9
| 16:00 | Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (abstract) PRESENTER: Igor de Camargo E Souza Câmara |
| 16:25 | Defeasible reasoning in RDFS (abstract) PRESENTER: Giovanni Casini |
| 16:50 | Modelling Multiple Perspectives by Standpoint-Enhanced DLs (abstract) PRESENTER: Lucía Gómez Álvarez |
16:00-17:30 Session 92D (ITP)
Chair:
| 16:00 | Formalized functional analysis with semilinear maps (abstract) PRESENTER: Frédéric Dupuis |
| 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)
Chair:
Location: Taub 9
| 16:00 | Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (abstract) PRESENTER: Igor de Camargo E Souza Câmara |
| 16:25 | Defeasible reasoning in RDFS (abstract) PRESENTER: Giovanni Casini |
| 16:50 | Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics PRESENTER: Lucia Gómez Álvarez |
17:30-18:45 Session 93: Logic Lounge: Future of Autonomous Driving; Keynote by Shai Shalev-Shwartz (Mobileye and The Hebrew University of Jerusalem); Panel: Gila Kamhi (Intel, Haifa), Sanjit Seshia (UC Berkeley) (FLoC)
Chair:
Location: Churchill Auditorium
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
| 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)
Chair:
| 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:00-10:30 Session 95: Joint DL/NMR Session C (NMR)
Chair:
Location: Taub 9
| 10:00 | Connection-Minimal Abduction in EL via Translation to FOL PRESENTER: Fajar Haifani |
10:30-11:00Coffee Break
11:00-12:30 Session 96A: Invited Talk: A Billion SMT Queries a Day (Neha Rungta) (CAV)
Chair:
Location: Taub 1
11:00-12:30 Session 96B: Cryptography 1 (CSF)
Chair:
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)
Chair:
Location: Taub 9
| 11:00 | AGM Revision in Description Logics Under Fixed-Domain Semantics (abstract) PRESENTER: Faiq Miftakhul Falakh |
| 11:25 | Repairing Ontologies via Kernel Pseudo-Contraction (abstract) PRESENTER: Vinícius Bitencourt Matos |
| 11:50 | Pointwise Circumscription in Description Logics (abstract) PRESENTER: Federica Di Stefano |
| 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)
Chair:
| 11:00 | SCL(EQ): SCL for First-Order Logic with Equality (abstract) PRESENTER: Christoph Weidenbach |
| 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)
Chair:
| 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)
Chair:
Location: Taub 9
| 11:00 | AGM Revision in Description Logics Under Fixed-Domain Semantics PRESENTER: Faiq Miftakhul Falakh |
| 11:25 | Repairing Ontologies via Kernel Pseudo-Contraction (abstract) PRESENTER: Renata Wassermann |
| 11:50 | Pointwise Circumscription in Description Logics PRESENTER: Federica Di Stefano |
| 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)
Chair:
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) PRESENTER: Elizabeth Polgreen |
14:00-15:30 Session 97B: Invited Talk 1 (CSF)
Chair:
Location: Taub 2
| 14:00 | Membership Inference Attacks against Classifiers (abstract) |
14:00-15:30 Session 97C: Query Answering & Extensions (DL)
Chair:
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) PRESENTER: Mateusz Urbańczyk |
| 15:05 | Advanced languages of terms for ontologies (abstract) PRESENTER: Philippe Balbiani |
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)
Chair:
| 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)
Chair:
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)
Chair:
Location: Taub 1
| 16:00 | PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (abstract) PRESENTER: Chaitanya Agarwal |
| 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)
Chair:
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) PRESENTER: Jean Christoph Jung |
| 16:50 | A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (abstract) PRESENTER: Satyadharma Tirtarasa |
| 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)
Chair:
| 16:00 | SAT-based Proof Search in Intermediate Propositional Logics (abstract) PRESENTER: Camillo Fiorentini |
| 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)
Chair:
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) |
17:30-18:30 Session 99: Herbrand Award Ceremony (IJCAR)
Chair:
| 17:30 | The Pleasures of Proof (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)
Chair:
Location: Taub 2
| 09:00 | IFCIL: An Information Flow Configuration Language for SELinux (abstract) PRESENTER: Lorenzo Ceragioli |
| 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)
Chair:
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) PRESENTER: Francesco Kriegel |
| 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)
Chair:
| 09:00 | Sequent Calculi for Choice Logics (abstract) PRESENTER: Michael Bernreiter |
| 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) PRESENTER: Dorota Leszczyńska-Jasion |
| 10:10 | Binary codes that do not preserve primitivity (abstract) PRESENTER: Štěpán Holub |
09:00-10:30 Session 100E (ITP)
Chair:
| 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)
Chair:
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)
Chair:
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)
Chair:
Location: Taub 1
| 11:00 | FORQ-based Language Inclusion Formal Testing (abstract) PRESENTER: Kyveli Doveri |
| 11:20 | Sound Automation of Magic Wands (abstract) PRESENTER: Thibault Dardinier |
| 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) PRESENTER: Alexandre Duret-Lutz |
| 12:10 | Complementing Büchi Automata with Ranker (abstract) PRESENTER: Barbora Šmahlíková |
11:00-12:30 Session 102B: Security Protocols 2 (CSF)
Chair:
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)
Chair:
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)
Chair:
| 11:00 | Finite two-dimensional proof systems for non-finitely axiomatizable logics (abstract) PRESENTER: Vitor Rodrigues Greati |
| 11:20 | Le\'sniewski's Ontology -- Proof-Theoretic Characterization (abstract) |
| 11:40 | Cyclic Proofs, Hypersequents, and Transitive Closure Logic (abstract) PRESENTER: Marianna Girlando |
| 12:00 | Rensets and Renaming-Based Recursion for Syntax and Bindings (abstract) |
11:00-12:30 Session 102E (ITP)
Chair:
| 11:00 | Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (abstract) PRESENTER: Asta Halkjær From |
| 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
Chair:
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:
- STLmc: Robust STL Model Checking of Hybrid Systems using SMT (13:00-13:30)
- UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (13:30-14:00)
Location: Taub entrance floor lobby
14:00-16:00 Session 104A: Deductive Verification and Decision Procedures (CAV)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Guendalina Righetti |
| 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)
Chair:
| 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) PRESENTER: Christoph Weidenbach |
| 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)
Chair:
| 14:00 | A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r) (abstract) PRESENTER: Jagadish Bapanapally |
| 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)
Chair:
Location: Taub 4
| 14:00 | Modelling Agents Roles in the Epistemic Logic L-DINF (abstract) PRESENTER: Stefania Costantini |
| 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.
Chair:
Location: Taub 8
16:00-16:30Coffee Break
16:30-17:30 Session 108: Plenary (FLoC)
Chair:
Location: Churchill Auditorium
| 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.
Chairs:
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)
Chair:
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) PRESENTER: Catuscia Palamidessi |
| 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)
Chair:
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)
Chair:
| 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) PRESENTER: Supratik Chakraborty |
| 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)
Chair:
| 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 112A: Invited Talk: Program Verification with Constrained Horn Clauses (Arie Gurfinkel) (CAV)
Chair:
Location: Taub 1
11:00-12:30 Session 112B: Verification and Synthesis (CSF)
Chair:
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)
Chair:
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)
Chair:
| 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 |
11:00-12:30 Session 112E (ITP)
Chair:
| 11:00 | Seventeen Provers under the Hammer (abstract) PRESENTER: Martin Desharnais |
| 11:30 | The Isabelle ENIGMA (abstract) PRESENTER: Zarathustra Goertzel |
| 12:00 | Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq (abstract) PRESENTER: Jason Gross |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, IJCAR, ITP).
12:30-13:15 Session 113: Business Meeting (DL)
Chair:
Location: Taub 9
| 12:30 | Business Meeting PRESENTER: Jean Christoph Jung |
13:00-14:00 Session 114: Tool Demonstrations (CAV)
Tool demonstrations for:
- From Spot 2.0 to Spot 2.10: What's New? (13:00-13:30)
- Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (13:30-14:00)
Location: Taub entrance floor lobby
14:00-15:30 Session 115A: Machine Learning (CAV)
Chair:
Location: Taub 1
| 14:00 | Specification-Guided Learning of Nash Equilibria with High Social Welfare (abstract) PRESENTER: Kishor Jothimurugan |
| 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) PRESENTER: Maximilian Alexander Köhl |
14:00-15:30 Session 115B: Cryptography 2 (CSF)
Chair:
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)
Chair:
| 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) PRESENTER: Jelle Piepenbrock |
14:00-15:30 Session 115D (ITP)
Chair:
| 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)
Chair:
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) PRESENTER: Philip Offtermatt |
| 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)
Chair:
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)
Chair:
| 16:00 | Non-associative, non-commutative multi-modal linear logic (abstract) PRESENTER: Stepan Kuznetsov |
| 16:20 | Paraconsistent Gödel modal logic (abstract) PRESENTER: Daniil Kozhemiachenko |
| 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)
Chair:
Location: Ullmann 300
| 09:00 | UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (abstract) PRESENTER: Elizabeth Polgreen |
| 09:45 | Democratizing SAT Solving (abstract) |
09:00-10:30 Session 120B (FRIDA)
Chairs:
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)
Chair:
Location: Ullmann 200
| 09:00 | Security Protocols as Choreographies PRESENTER: Alessandro Bruni |
| 09:30 | How to Explain Security Protocols to Your Children PRESENTER: Véronique Cortier |
| 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)
Chair:
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)
Chair:
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) PRESENTER: Kristin Y. Rozier |
09:00-10:30 Session 120F (PAAR)
Chair:
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) PRESENTER: Maximilian Heisinger |
09:00-10:30 Session 120G: Parallel algorithms (PDAR)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
Location: Ullmann 306
| 09:00 | On Exams with the Isabelle Proof Assistant (abstract) PRESENTER: Frederik Krogsdal Jacobsen |
| 09:30 | Invited Talk: Satisfiability Modulo Theories in an Undergraduate Class (abstract) |
09:00-10:00 Session 120K (WOLVERINE)
Keynote presentation
Chair:
Location: Ullmann 202
| 09:00 | Artificial Intelligence (abstract) |
09:00-10:30 Session 120L (WST)
Chair:
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)
Chair:
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)
Chair:
Location: Ullmann 310
| 09:15 | Computer-aided Verification and Automated Synthesis of Cryptographic Protocols (abstract) |
09:30-10:30 Session 124A: Keynote (FMBC)
Location: Ullmann 307
| 09:30 | MEV-freedom, in DeFi and beyond (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) PRESENTER: Chaked R.J. Sayedoff |
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)
Chair:
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)
Chair:
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) PRESENTER: Lorenzo Ceragioli |
| 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)
Chair:
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) PRESENTER: Ignacio Ballesteros |
| 12:00 | Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (abstract) PRESENTER: Polina Vinogradova |
| 12:15 | FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (abstract) PRESENTER: Aurélien Saue |
11:00-12:30 Session 125E (FRIDA)
Chairs:
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)
Chair:
Location: Ullmann 200
| 11:00 | On the Complexity of Verification of Time-Sensitive Distributed Systems PRESENTER: Tajana Ban Kirigin |
| 11:30 | Protocol Analysis with Time and Space PRESENTER: Santiago Escobar |
| 12:00 | Probabilistic annotations for protocol models |
| 12:20 | Securing Node-RED Applications PRESENTER: Mohammad M. Ahmadpanah |
11:00-12:30 Session 125G: Isabelle 2 (Isabelle)
Chair:
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) PRESENTER: Jørgen Villadsen |
| 11:50 | On Termination for Hybrid Tableaux (abstract) |
| 12:10 | Lessons of Teaching Formal Methods with Isabelle (abstract) PRESENTER: Frederik Krogsdal Jacobsen |
11:00-12:30 Session 125H: Model Counting: Applications & Experiments (MC)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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.
Chair:
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)
Chair:
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)
Chair:
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: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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Srinidhi Nagendra |
| 14:45 | Determinism of ledger updates (abstract) PRESENTER: Polina Vinogradova |
| 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)
Chairs:
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)
Chair:
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)
Chair:
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) PRESENTER: Friedrich Slivovsky |
14:00-15:30 Session 127I (NSV)
Chair:
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)
Chair:
Location: Ullmann 205
| 14:00 | Exploring Partial Models with SCL (abstract) PRESENTER: Simon Schwarz |
| 14:30 | On SGGS and Horn Clauses (abstract) PRESENTER: Maria Paola Bonacina |
| 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 127M: Tools (SMT)
Location: Ullmann 311
| 14:00 | NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems (abstract) PRESENTER: Anna Becchi |
| 14:20 | cvc5: A Versatile and Industrial-Strength SMT Solver (abstract) PRESENTER: Andres Noetzli |
| 14:40 | The VMT-LIB Language and Tools (abstract) PRESENTER: Alessandro Cimatti |
| 15:00 | Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (abstract) PRESENTER: Mathias Preiner |
14:00-15:30 Session 127N (SYNT)
Chair:
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) PRESENTER: Elizaveta Pertseva |
| 14:40 | Inferring Environment Assumptions in Model Refinement (abstract) PRESENTER: Srinivas Nedunuri |
| 15:00 | A Framework for Transforming Specifications in Reinforcement Learning (abstract) PRESENTER: Kishor Jothimurugan |
| 15:20 | SYNTCOMP Results |
14:00-15:30 Session 127P: Proofs in Education (High-School Level) (ThEdu)
Chair:
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-15:30 Session 127R (WST)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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:30 Session 131I: Solver diversification & Discussion (PDAR)
Chair:
Location: Ullmann 303
| 16:00 | Beyond Portfolios of Stable Solvers (abstract) |
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:30 Session 131K: SMT-COMP Report and Tool Presentation (SMT)
Chair:
Location: Ullmann 311
| 16:00 | SMT-COMP Report and Tool Presentations |
16:00-17:00 Session 131L (SYNT)
Chair:
Location: Ullmann 201
| 16:00 | SyGuS-IF + SemGuS Results |
| 16:10 | Future Work and Open Challenges Panel – Authors+Chairs |
16:00-17:20 Session 131P (iPRA)
Location: Ullmann 203
| 16:00 | Application of Interpolation in Networks (abstract) PRESENTER: H. Jerome Keisler |
| 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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Maria Paola Bonacina |
09:00-10:30 Session 134E (VeriProp)
Chair:
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 135A: Libraries (Coq)
Chair:
Location: Taub 5
| 09:30 | A Coq Library for Mechanised First-Order Logic (abstract) PRESENTER: Dominik Kirst |
| 10:00 | QuantumLib: A Library for Quantum Computing in Coq (abstract) PRESENTER: Jacob Zweifler |
09:30-10:30 Session 135B: Invited talk (UNIF)
Chair:
Location: Taub 8
| 09:30 | Unification types in modal logics (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 137A: Automation and Tooling (Coq)
Chair:
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)
Chair:
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)
Chair:
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)
Chair:
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) PRESENTER: Mădălina Erașcu |
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) PRESENTER: Clemens Eisenhofer |
| 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)
Chair:
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) PRESENTER: Daniele Nantes-Sobrinho |
11:00-12:30 Session 137G (VeriProp)
Chair:
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)
Chair:
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)
Chair:
Location: Taub 5
| 14:00 | jsCoq: Literate Proof Documents Dressed for the Web PRESENTER: Emilio Jesús Gallego Arias |
| 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 PRESENTER: Sebastian Mödersheim |
| 14:30 | Adapting constraint solving to automatically analyze UPI Protocols PRESENTER: Sreekanth Malladi |
| 14:50 | Quantum Machine Learning and Fraud Detection PRESENTER: Alessandra Di Pierro |
| 15:10 | Formal Methods and Mathematical Intuition |
14:00-15:35 Session 138C (PAAR)
Chair:
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)
Chair:
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 138E: Standards and benchmarks - Business meeting (SMT)
Chair:
Location: Taub 2
| 14:00 | SMT-Lib Update Report PRESENTER: Cesare Tinelli |
| 14:30 | Business Meeting PRESENTER: Antti Hyvärinen |
14:00-15:30 Session 138F: Invited talk (UNIF)
Chair:
Location: Taub 8
| 14:00 | Unification Decision Procedures using Basic Narrowing modulo an Equational Theory |
| 15:00 | Fuzzy Order-Sorted Feature Term Unification (abstract) PRESENTER: Gian Carlo Milanese |
14:00-15:30 Session 138G (VeriProp)
Chair:
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) PRESENTER: Wojciech Rozowski |
14:00-15:30 Session 138H (WST)
Chair:
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-17:00 Session 139A: Coq and its Ecosystem (Coq)
Chair:
Location: Taub 5
| 16:00 | Coq Community Survey 2022: Summary of Results (abstract) PRESENTER: Ana de Almeida Borges |
| 16:30 | Discussion with Coq Core Development Team PRESENTER: Emilio Jesús Gallego Arias |
16:00-16:30 Session 139B: Paper presentation (SC^2)
Chair:
Location: Taub 3
| 16:00 | An SC-Square Approach to the Minimum Kochen–Specker Problem (abstract) PRESENTER: Zhengyu Li |
16:00-16:45 Session 139C: Update on Proof Standardization (Joint Session with PAAR) (PAAR and SMT)
Chair:
Location: Taub 7
| 16:00 | SMT Proof Standardization Update |
16:00-17:00 Session 139D (UNIF)
Chair:
Location: Taub 8
| 16:00 | Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report) (abstract) PRESENTER: Andrew M. Marshall |
| 16:30 | Restricted Unification in the Description Logic FLbot (abstract) PRESENTER: Oliver Fernandez Gil |
16:00-17:15 Session 139E (VeriProp)
Chair:
Location: Taub 9
| 16:00 | Uncertainty propagation in discrete-time systems using probabilistic forms (abstract) |
| 16:50 | Verifying Probabilistic Programs using Generating Functions (abstract) |