LICS 2023 Invited Talks

Tonian Pitassi (Columbia University, USA)

(TBA)

Dan Suciu (University of Washington, USA)

Applications of Information Inequalities to Database Theory Problems

The talk describes several applications of information inequalities to problems in database theory. The problems discussed include: upper bounds of a query's output, worst-case optimal join algorithms, the query domination problem, and the implication problem for approximate integrity constraints. No prior knowledge of query processing or information theory is needed: all required concepts and results from information inequalities are introduced here, gradually, and motivated by database problems.

[Preprint]

Dale Miller (Inria Saclay & LIX, Institut Polytechnique de Paris, Palaiseau France)

A system of inference based on proof search: an extended abstract

Gentzen designed his natural deduction proof system to ``come as close as possible to actual reasoning.'' Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. The PSF framework attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated.

LICS 2023 Invited Tutorials

Adnan Darwiche (University of California, Los Angeles, USA)

Logic for Explainable AI

A central quest in explainable AI relates to understanding the decisions made by (learned) classifiers. There are three dimensions of this understanding that have been receiving significant attention in recent years. The first dimension relates to characterizing necessary and sufficient conditions for decisions, therefore providing abstractions of instances that can be viewed as the ``reasons behind decisions.’' The next dimension relates to identifying minimal aspects of an instance that are sufficient for a decision, therefore characterizing maximal aspects of the instance that are irrelevant to the decision. The last dimension relates to identifying minimal aspects of an instance that are necessary for a decision and, hence, characterize minimal perturbations to the instance that yield alternate decisions. We will discuss in this tutorial some recent developments in symbolic logic which provide a comprehensive semantical and computational theory of explainability along these dimensions. The tutorial will also discuss how this theory is particularly applicable to non-symbolic classifiers such as those based on Bayesian networks, decision trees, random forests and some types of neural networks.

Azadeh Farzan (University of Toronto, Canada)

Commutativity in Automated Program Verification

Trace theory (formulated by Mazurkiewicz in 1987) is a framework for formalizing equivalence relations for concurrent program runs based on a commutativity relation over the set of atomic steps taken by individual program threads. It has been implicitly or explicitly used in a broad set of program analysis techniques, such as predictive testing for atomicity or data race violations, static and dynamic partial order reduction in model checking (particularly stateless model checking), and reasoning about distributed programs. In this talk, I will present a different line of work that uses traces for the purpose of proof simplification for a broad set of automated verification goals. The long term thesis of this line of work has been that by taking advantage of commutativity, one can potentially attempt a substantially simpler verification task in place of the original goal, and succeed at it despite the inevitability of the failure of the original verification task. The idea is to verify a different program, in place of the original one, and use commutativity as a way of soundly carrying over the verification results to the original one.

I will talk about hypersafety verification of sequential and concurrent programs, and safety and liveness verification of concurrent and distributed programs. I will show how commutativity can be incorporated into a new verification algorithm which enumerates infinitely many possibilities for alternative programs to be verified instead of the original one. Towards the end of the talk, I will give an overview of some open research questions in this area.