Program for Tuesday, August 9th: Talk View

PROGRAM FOR TUESDAY, AUGUST 9TH: TALK VIEW

Days:

previous day

next day

all days

View: with abstracts session overview

8:30

9:00

9:30

10:00

10:30

11:00

11:30

12:00

12:30

13:00

13:30

14:00

14:30

15:00

15:30

16:00

16:30

17:00

17:30

18:00

18:30

19:00

19:30

20:00

20:30

21:00

21:30

22:00

09:00-10:30 CAV Award 2022

09:00-10:30

IFCIL: An Information Flow Configuration Language for SELinux

Lorenzo Ceragioli, Letterio Galletta, Pierpaolo Degano, David Basin

09:00-10:30

Towards a General-Purpose Dynamic Information Flow Policy

Peixuan Li, Danfeng Zhang

09:00-10:30

Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games

David Mestel

09:00-10:30

More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role

Jean Christoph Jung, Andrea Mazzullo, Frank Wolter

09:00-10:30

Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended

Franz Baader, Patrick Koopmann, Francesco Kriegel, Adrian Nuradiansyah

09:00-10:30

Fine-Grained Forgetting for the Description Logic ALC

Mostafa Sakr, Renate A. Schmidt

09:00-10:30

Uniform and Modular Sequent Systems for Description Logics

Jonas Karge, Tim Lyon

09:00-10:30

Sequent Calculi for Choice Logics

Michael Bernreiter, Anela Lolic, Jan Maly, Stefan Woltran

09:00-10:30

Lash 1.0 (System Description)

Chad Brown, Cezary Kaliszyk

09:00-10:30

Goéland : A Concurrent Tableau-Based Theorem Prover (System Description)

Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, Hinde Bouziane

09:00-10:30

Synthetic tableaux: minimal tableau search heuristics

M. Sochański, D. Leszczyńska-Jasion, S. Chlebowski, A. Tomczyk, M. Jukiewicz

09:00-10:30

Binary codes that do not preserve primitivity

Štěpán Holub, Štěpán Starosta, Martin Raška

09:00-10:30

Formalization of Randomized Approximation Algorithms for Frequency Moments

Emin Karayel

09:00-10:30

Mechanizing Soundness of Off-Policy Evaluation

Jared Yeager, Eliot Moss, Michael Norrish, Philip Thomas

09:00-10:30

Formalizing Algorithmic Bounds in the Query Model in EasyCrypt

Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu

09:00-10:00

Fallacious arguments: the place where Knowledge Representation and Argument Mining meet each other

Serena Villata

10:00-10:30

There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive

Mohan Sridharan, Chloe Benz, Arthur Findelair, Kevin Gloaguen

11:00-12:30

FORQ-based Language Inclusion Formal Testing

Kyveli Doveri, Pierre Ganty, Nicolas Mazzocchi

11:00-12:30

Sound Automation of Magic Wands

T. Dardinier, G. Parthasarathy, N. Weeks, P. Müller, A.J. Summers

11:00-12:30

Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition

Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi, Lijun Zhang

11:00-12:30

From Spot 2.0 to Spot 2.10: What's New?

Duret-Lutz et.al

11:00-12:30

Complementing Büchi Automata with Ranker

Vojtěch Havlena, Ondrej Lengal, Barbora Šmahlíková

11:00-12:30

Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof

David Baelde, Stephanie Delaune, Adrien Koutsos, Solène Moreau

11:00-12:30

Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol

Felipe Boeira, Mikael Asplund

11:00-12:30

Symbolic protocol verification with dice: process equivalences in the presence of probabilities

Vincent Cheval, Raphaëlle Crubillé, Steve Kremer

11:00-12:30

Charting the Borderland – Decidability in Description Logics and Beyond

Sebastian Rudolph

11:00-12:30

Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)

S. Borgwardt, J. Hoffmann, A. Kovtunova, M. Krötzsch, B. Nebel, M. Steinmetz

11:00-12:30

Finite two-dimensional proof systems for non-finitely axiomatizable logics

Vitor Rodrigues Greati, Joao Marcos

11:00-12:30

Le\'sniewski's Ontology -- Proof-Theoretic Characterization

Andrzej Indrzejczak

11:00-12:30

Cyclic Proofs, Hypersequents, and Transitive Closure Logic

Anupam Das, Marianna Girlando

11:00-12:30

Rensets and Renaming-Based Recursion for Syntax and Bindings

Andrei Popescu

11:00-12:30

Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL

Asta Halkjær From, Frederik Krogsdal Jacobsen

11:00-12:30

Undecidability of Dyadic First-Order Logic in Coq

Johannes Hostert, Andrej Dudenhefner, Dominik Kirst

11:00-12:30

Computational Back-and-Forth Arguments in Constructive Type Theory

Dominik Kirst

11:00-12:30

Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity

Anna Rapberger, Markus Ulbricht, Johannes P. Wallner

11:00-12:30

Bipolar Argumentation Frameworks with Explicit Conclusions: Connecting Argumentation and Logic

Victor Hugo Rocha, Fabio Cozman

11:00-12:30

From Weighted Conditionals to a Gradual Argumentation Semantics and back

Laura Giordano

13:00-14:00 Tool Demonstrations

14:00-16:00

Even Faster Conflicts and Lazier Reductions for String Solvers

Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett, Cesare Tinelli

14:00-16:00

Local Search For SMT on Linear Integer Arithmetic

Shaowei Cai, Bohan Li, Xindi Zhang

14:00-16:00

Reasoning about Data Trees using CHCs

Marco Faella, Gennaro Parlato

14:00-16:00

Verified Erasure Correction in Coq with MathComp and VST

Joshua M. Cohen, Qinshi Wang, Andrew W. Appel

14:00-16:00

End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers

S. Yuan, F. Besson, J.-P. Talpin, S. Hym, K. Zandberg, E. Baccelli

14:00-16:00

Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence

Joonwon Choi, Adam Chlipala, Arvind

14:00-15:30

So near and yet so far: formal verification of distance bounding protocols

Stéphanie Delaune

14:00-16:00

Concept Abduction for Description Logics

Birte Glimm, Yevgeny Kazakov, Michael Welt

14:00-16:00

On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne

C. Alrabbaa, S. Borgwardt, T. Friese, P. Koopmann, J. Méndez, A. Popovič

14:00-16:00

SAT-Based Axiom Pinpointing Revisited

Birte Glimm, Yevgeny Kazakov

14:00-16:00

An API for DL Abduction Solvers

Zuzana Hlávková, Martin Homola, Patrick Koopmann, Júlia Pukancová

14:00-16:00

Evaluating the Interpretability of Threshold Operators

Guendalina Righetti, Daniele Porello, Roberto Confalonieri

14:00-16:00

A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals

Bernardo Alkmim, Edward Haeusler, Cláudia Nalon

14:00-15:30

Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers

Chaitanya Mangla, Sean Holden, Paulson Larry

14:00-15:30

Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)

Martin Suda

14:00-15:30

Semantic Relevance

Fajar Haifani, Christoph Weidenbach

14:00-15:30

Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System

Durán, Eker, Escobar, Marti-Oliet, Meseguer, Rubio, Talcott

14:00-15:30

A framework for approximate generalization in quantitative theories (ONLINE)

Temur Kutsia, Cleo Pau

14:00-15:30

A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)

Jagadish Bapanapally, Ruben Gamboa

14:00-15:30

Formalizing the ring of adèles of a global field

María Inés de Frutos-Fernández

14:00-15:30

Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof

Nicolas Magaud

14:00-15:30

Modelling Agents Roles in the Epistemic Logic L-DINF

Stefania Costantini, Valentina Pitoni, Andrea Formisano

14:00-15:30

A situation-calculus model of Knowledge and Belief based on Thinking about Justifications

Richard Scherl

14:00-15:30

Towards Legally and Ethically Correct Online HTN Planning for Data Transfer

Hisashi Hayashi, Ken Satoh

15:00-16:00 The Olympic Games Session (Block 2)

15:30-15:40 Best Student Paper Prize

15:30-16:00 Closing

16:00-16:30 Poster Session (1)

17:30-18:30 Business Meeting

08:30-09:00 Coffee & Refreshments

10:30-11:00 Coffee Break

12:30-14:00 Lunch Break

16:00-16:30 Coffee Break

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

16:30-17:30

SMT-based Verification of Distributed Network Control Planes

Aarti Gupta

19:30-22:00 FLoC Banquet (at Bikta Bayar - Beit Oren) - Paid event