DisCoTec 2026 has invited speakers to give keynote talks and tutorials.
DisCoTec 2026 will host a keynote talk at each conference as well as a DisCoTec-wide keynote. The invited speakers are Mehdi Dastani (COORDINATION), Paolo Romano (DAIS), Nathalie Bertrand (FORTE), and Roberto Bruni (DisCoTec-wide).
Title: A logic for all reasons
Abstract: Program verification draws on a rich spectrum of program logics, each offering a distinct perspective on program behaviour. Hoare Logic deals with proving the absence of bugs (i.e., partial correctness) through over-approximations of reachable states. Incorrectness Logic, in contrast, identifies reachable error states without false alarms and Lisbon triples pinpoint concrete sources of errors with the same guarantee. Necessary condition logic and predicate transformers further enrich this landscape.
Despite their individual strengths, these frameworks are typically developed and applied in isolation, limiting their potential to improve precision and strengthen static analysis guarantees. In verification, as elsewhere, union is strength: integrating orthogonal reasoning principles enables analyses that are strictly more expressive and informative than before.
In this talk, we propose a unifying framework that systematically combines multiple analysis dimensions: direction (forward and backward) and approximation (under-, exact, and over-approximation), all within a simple lattice of program triples. By elevating approximation modes to first-class objects, we lay a principled foundation for modular, compositional, and expressive reasoning. Our approach reconciles correctness and incorrectness within a single logical framework, enabling the derivation of code summaries that can inhabit any point in the program logic landscape.
Bio: Roberto Bruni is Full Professor at the Computer Science Department of the University of Pisa. His research focuses on the modeling, analysis, and verification of concurrent, distributed, adaptive, and open systems, as well as on natural computing and bio-inspired models of computation. He has contributed to a wide range of areas including Petri nets, rewriting logic, category theory, process algebras, service-oriented computing, multiparty interactions, Reaction Systems, abstract interpretation and program logics. He has co-authored over 170 publications, including textbooks and monographs, and has been actively involved in numerous international research projects and the organization of international conferences. He received his PhD in Computer Science from the University of Pisa.