Program for Monday, August 8th: Talk View

PROGRAM FOR MONDAY, AUGUST 8TH: 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

09:00-10:30

Software Verification of Hyperproperties Beyond k-Safety

Raven Beutner, Bernd Finkbeiner

09:00-10:30

A Scalable Shannon Entropy Estimator

Priyanka Golia, Brendan Juba, Kuldeep S. Meel

09:00-10:30

PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation

Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang, Wanwei Liu

09:00-10:30

Explaining Hyperproperty Violations

Coenen, Dachselt, Finkbeiner, Frenkel, Hahn, Horak, Metzger, Siber

09:00-10:30

Distilling Constraints in Zero-Knowledge Protocols

E. Albert, M. Bellés-Muñoz, M. Isabel, C. Rodríguez-Núñez, A. Rubio

09:00-10:30

N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures

Thilo Weghorn, Si Liu, Christoph Sprenger, Adrian Perrig, David Basin

09:00-10:30

Applying consensus and replication securely with FLAQR

Priyanka Mondal, Maximilian Algehed, Owen Arden

09:00-10:30

How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis

David Mestel, Johannes Müller, Pascal Reisert

09:00-10:30

Rectifying Classifiers

Pierre Marquis

09:00-10:30

Connection-minimal Abduction in EL via translation to FOL (Extended Abstract)

Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach

09:00-10:30

From the Universality of Mathematical Truth to the Interoperability of Proof Systems (Invited Talk)

Gilles Dowek

09:00-10:30

Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description)

Gereon Kremer, Andrew Reynolds, Clark Barrett, Cesare Tinelli

09:00-10:30

Refinement of Parallel Algorithms down to LLVM

Peter Lammich

09:00-10:30

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification

Hrutvik Kanabar, Anthony Fox, Magnus Myreen

09:00-10:30

Dandelion: Certified Approximations of Elementary Functions

H. Becker, M. Tekriwal, E. Darulova, A. Volkova, J.-B. Jeannin

09:00-10:00

Rectifying Classifiers

Pierre Marquis

10:00-10:30

Connection-Minimal Abduction in EL via Translation to FOL

Fajar Haifani, Patrick Koopmann, Sophie Tourret, Christoph Weidenbach

11:00-12:30 Invited Talk: A Billion SMT Queries a Day (Neha Rungta)

11:00-12:30

Contingent payments from two-party signing and verification for abelian groups

Sergiu Bursuc, Sjouke Mauw

11:00-12:30

Collusion-Preserving Computation without a Mediator

Yun Lu, Michele Ciampi, Vassilis Zikas

11:00-12:30

Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox

François Dupressoir, Konrad Kohbrok, Sabine Oechsner

11:00-12:30

AGM Revision in Description Logics Under Fixed-Domain Semantics

Faiq Miftakhul Falakh, Sebastian Rudolph

11:00-12:30

Repairing Ontologies via Kernel Pseudo-Contraction

Vinícius Bitencourt Matos, Renata Wassermann

11:00-12:30

Pointwise Circumscription in Description Logics

Federica Di Stefano, Magdalena Ortiz, Mantas Simkus

11:00-12:30

Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results

Martin Homola, Júlia Pukancová, Iveta Balintová, Janka Boborová

11:00-12:30

SCL(EQ): SCL for First-Order Logic with Equality

Hendrik Leidinger, Christoph Weidenbach

11:00-12:30

Ground joinability and connectedness in the superposition calculus

André Duarte, Konstantin Korovin

11:00-12:30

Term Ordering for Non-Reachability of (Conditional) Rewriting

Akihisa Yamada

11:00-12:30

An Efficient Subsumption Test Pipeline for BS(LRA) Clauses

Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach

11:00-12:30

Synthetic Kolmogorov Complexity in Coq

Yannick Forster, Fabian Kunze, Nils Lauermann

11:00-12:30

Formalizing Szemerédi's Regularity Lemma in Lean

Bhavik Mehta, Yaël Dillies

11:00-12:30

Formalizing the divergence theorem and the Cauchy integral formula in Lean

Yury Kudryashov

11:00-12:30

AGM Revision in Description Logics Under Fixed-Domain Semantics

Faiq Miftakhul Falakh, Sebastian Rudolph

11:00-12:30

Repairing Ontologies via Kernel Pseudo-Contraction

Vinícius Bitencourt Matos, Renata Wassermann

11:00-12:30

Pointwise Circumscription in Description Logics

Federica Di Stefano, Magdalena Ortiz, Mantas Šimkus

11:00-12:30

Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results

Martin Homola, Júlia Pukancová, Iveta Balintová, Janka Boborová

14:00-15:30

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

R. Banno, K. Matsuoka, N. Matsumoto, S. Bian, M. Waga, K. Suenaga

14:00-15:30

Abstraction Modulo Stability for Reverse Engineering

Anna Becchi, Alessandro Cimatti

14:00-15:30

Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope

Stanley Bak, Sergiy Bogomolov, Niklas Kochdumper, Ethan Lew, Kostiantyn Potomkin

14:00-15:30

RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems

Eric Goubault, Sylvie Putot

14:00-15:30

STLmc: Robust STL Model Checking of Hybrid Systems using SMT

Geunyeol Yu, Jia Lee, Kyungmin Bae

14:00-15:30

UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis

Polgreen, Cheang, Gaddamadugu, Godbole, Laeufer, Lin, Manerkar, Mora, Seshia

14:00-15:30

Membership Inference Attacks against Classifiers

Ninghui Li

14:00-15:30

Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended

Meghyn Bienvenu, Camille Bourgaux

14:00-15:30

Ontology-based Data Federation (Extended Abstract)

Z. Gu, D. Lanti, A. Mosca, G. Xiao, J. Xiong, D. Calvanese

14:00-15:30

Comonadic Semantics for Description Logics Games

Bartosz Bednarczyk, Mateusz Urbańczyk

14:00-15:30

Advanced languages of terms for ontologies

Philippe Balbiani, Cigdem Gencer, Martin Diéguez

14:00-15:30

Actions over Core-closed Knowledge Bases

Claudia Cauli, Magdalena Ortiz, Nir Piterman

14:00-15:30

GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)

Tanel Tammet, Dirk Draheim, Priit Järv

14:00-15:30

Local Reductions for the Modal Cube

Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, Clare Dixon

14:00-15:30

Evonne: Interactive Proof Visualization for Description Logics (System Description)

C. Alrabbaa, F. Baader, S. Borgwardt, R. Dachselt, P. Koopmann, J. Méndez

14:00-15:30

Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications

Hui Yang, Yue Ma, Nicole Bidoit

14:00-15:30

Deeper Shallow Embeddings

Jacob Prinz, Alex Kavvos, Leonidas Lampropoulos

14:00-15:30

Compositional Verification of Interacting Systems using Event Monads

Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Ye Hong, Bican Xia

14:00-15:30

Reflexive tactics for algebra, revisited

Kazuhiko Sakaguchi

14:00-15:30

Trust Graphs for Belief Revision: Framework and Implementation

Aaron Hunter, Sam Tadey

14:00-15:30

Truth-Tracking with Non-Expert Information Sources

Joseph Singleton, Richard Booth

14:00-15:30

Asking human reasoners to judge postulates of belief change for plausibility

Clayton Baker, Thomas Meyer

16:00-17:30

PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP

Chaitanya Agarwal, Shibashis Guha, Jan Křetínský, Pazhamalai Muruganandham

16:00-17:30

Sampling-Based Verification of CTMCs with Uncertain Rates

Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga, Matthias Volk

16:00-17:30

Playing Against Fair Adversaries in Stochastic Games with Total Rewards

Pablo Castro, Pedro R. D'Argenio, Luciano Putruele, Ramiro Demasi

16:00-17:30

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures

Lorenz Leutgeb, Georg Moser, Florian Zuleger

16:00-17:30

Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers

Aina Niemetz, Mathias Preiner, Clark Barrett

16:00-17:30 Mentoring Session and 5-minute Talks

16:00-17:30

Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract)

F. Baader, P. Koopmann, F. Michel, A.-Y. Turhan, B. Zarriess

16:00-17:30

Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies

Maurice Funk, Jean Christoph Jung, Carsten Lutz

16:00-17:30

A new dimension to generalization: computing temporal EL concepts from positive examples (Extended

Satyadharma Tirtarasa, Anni-Yasmin Turhan

16:00-17:30

Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract)

Laura Giordano, Alberto Martelli, Daniele Theseider Dupre

16:00-17:30

SAT-based Proof Search in Intermediate Propositional Logics

Mauro Ferrari, Camillo Fiorentini

16:00-17:30

Preprocessing of Propagation Redundant Clauses

Joseph Reeves, Marijn Heule, Randal Bryant

16:00-17:30

Clause Redundancy and Preprocessing in Maximum Satisfiability

Hannes Ihalainen, Jeremias Berg, Matti Järvisalo

16:00-17:30

Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)

Takuya Matsuzaki, Tomohiro Fujita

16:00-17:30 ITP Business Meeting

16:00-17:30

Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect

Jesse Heyninck, Gabriele Kern-Isberner, Tommie Meyer

16:00-17:30

Situated Conditionals - A Brief Introduction

Giovanni Casini, Thomas Meyer, Ivan Varzinczak

16:00-17:30

On some weakenings of transitivity in the logic of norms (extended abstract)

Xavier Parent

17:30-18:30

The Pleasures of Proof

Natarajan Shankar

08:30-09:00 Coffee & Refreshments

10:30-11:00 Coffee Break

12:30-14:00 Lunch Break

15:30-16:00 Coffee Break

18:30-20:30 Walking tour (at Haifa)