POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Thu 23 Jan 2025 13:20 - 13:40 at Marco Polo - Decision Procedures

The classical `decision problem’ asks whether a given formula of first-order logic is satisfiable. In this work we consider an extension of this problem to regular first-order \emph{theories}, i.e. (infinite) regular sets of formulae. Building on the beautiful classification of syntactic classes as decidable or undecidable for the classical decision problem, we show that some classes (the EPR and Gurevich classes) which are decidable in the classical setting are undecidable for regular theories; on the other hand for each we show a subclass which remains decidable in our setting, leaving a complete classification as a challenge for future work. Finally, we observe that our problem generalises prior work on verification of uninterpreted programs, and give a semantic class of existential formulae for which the problem is decidable.

This program is tentative and subject to change.

Thu 23 Jan

Displayed time zone: Mountain Time (US & Canada) change

13:20 - 14:20
Decision ProceduresPOPL at Marco Polo
13:20
20m
Talk
The Decision Problem for Regular First Order Theories
POPL
Umang Mathur National University of Singapore, David Mestel Maastricht University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
13:40
20m
Talk
A Primal-Dual Perspective on Program Verification Algorithms
POPL
Takeshi Tsukada Chiba University, Hiroshi Unno Tohoku University, Oded Padon Weizmann Institute of Science, Sharon Shoham Tel Aviv University
14:00
20m
Talk
Dis/Equality Graphs
POPL
George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Jahrim Gabriele Cesario University of St. Gallen, Guido Salvaneschi University of St. Gallen