FRIDA 2027 (Workshop on Formal Reasoning in Distributed Algorithms)

Concurrent and distributed algorithms are central to shared-memory multiprocessing, Internet services, cloud platforms, blockchains, control systems, etc. However, verifying their correctness properties, from fault tolerance, linearizability, and liveness to more general hyperproperties, requires intricate arguments, and hand-written proofs often contain subtle errors. These challenges are growing as systems increase in complexity and adopt technologies such as CXL, RDMA, non-volatile memory, and heterogeneous architectures. AI-generated designs and code further heighten the need for formal validation. At the same time, AI agents can automate labor-intensive parts of modeling and verification, and this is rapidly changing the formal methods landscape.

Despite substantial progress, rigorous tool-supported verification of distributed algorithms and systems is not yet routine. Recent techniques can analyze high-level algorithmic descriptions and, in some cases, executable code. Making these methods practical requires closer collaboration among researchers in distributed algorithms, distributed systems, formal verification, and programming languages. FRIDA fosters this collaboration through a full-day program of invited and contributed talks and discussions, with the goal of advancing rigorous, practical techniques for the design and analysis of concurrent and distributed systems.

The FRIDA workshop has taken place almost every year since 2014:

• FRIDA 2025 - Berlin, Germany (DISC 2025)
• FRIDA 2024 - Montreal, Canada (CAV 2024)
• FRIDA 2023 - L’Aquila, Italy (DISC 2023)
• FRIDA 2022 - Haifa, Israel (FLoC 2022)
• FRIDA 2021 - Online (DISC 2021)
• FRIDA 2020 - Online (QONFEST 2020)
• FRIDA 2019 - Budapest, Hungary (DISC 2019)
• FRIDA 2018 - Oxford, UK (FLoC 2018)
• FRIDA 2017 - Vienna, Austria (DISC 2017)
• FRIDA 2016 - Marrakech, Morocco (NETYS 2016)
• FRIDA 2015 - Grenoble, France (FORTE 2015)
• FRIDA 2014 - Vienna, Austria (Vienna Summer of Logic 2014)

Call for Talks

We invite proposals for talks at FRIDA 2027, the 13th Workshop on Formal Reasoning in Distributed Algorithms, a one-day workshop co-located with POPL 2027 in Mexico City, Mexico, in January 2027.

FRIDA brings together researchers in distributed algorithms and systems, formal methods, and programming languages to share recent advances, practical experience, and open problems in the rigorous design and analysis of distributed algorithms and systems. Relevant topics include models for concurrent and distributed systems; consistency and correctness conditions such as linearizability, liveness, and hyperproperties; formal modeling and specification; model checking; interactive and automated theorem proving; AI-assisted formal modeling and verification; parameterized verification; invariant inference; synthesis; runtime verification; testing; integration of verification techniques; and benchmarking.

The program will combine invited and contributed talks, with ample time for discussion. We welcome proposals describing new or ongoing work, recently published results, tools, experience reports, position statements, and open problems. FRIDA is non-archival and will have no proceedings; proposals may present work that has been submitted or published elsewhere.