|
6th Summer
School on Foundations of Programming and Software Systems 13-17th July 2026 Emerging
Approaches for Reasoning about Programs and Proofs The 2026 Foundations of Programming and Software
Systems (FoPSS) Summer School brings together students and researchers to
explore "Emerging Approaches for Reasoning about Programs and
Proofs." This week-long school provides a broad and immersive
introduction to the latest developments on reasoning about programming. This
year’s edition is dedicated to recent methodologies, spanning advanced type
systems, proof assistants and logic, and neurosymbolic approaches, that are
actively shaping the frontier of software verification and program semantics. Our program features a distinguished series of
lectures designed to equip participants with both a solid grounding in
established foundations and a forward-looking perspective on the field's
future. By diving into highly active research areas, attendees will gain the
theoretical tools necessary to reason rigorously about complex, modern
programs. Through engaging instruction and collaborative discussions, the
school aims to inspire the next generation of researchers to push the
boundaries of what is possible in formal reasoning and program verification. |
The
series of Summer Schools on Foundations
of Programming and Software Systems (FoPSS) was jointly created by
EATCS, ETAPS, ACM SIGLOG and ACM SIGPLAN. The first FoPPS was organized in
2017. The goal
is to introduce the participants to various aspects of computation theory and
programming languages. The
school, spread over a single week, is aimed at students and researchers in
Theoretical Computer Science, broadly construed. Each year
the school is focused on a particular, actively researched topic. |
|
Institute
for Computing and Information Radboud University Nijmegen |
Program Verification Using Concurrent Separation
Logic Concurrent
programs are challenging to get right, especially if threads share access to
memory. The formalism of "Concurrent Separation Logic" (which was
pioneered by O'Hearn and Brookes in 2007) provides a powerful framework to
verify concurrent programs. Over the
last 20 years, concurrent separation Logic has emerged into an active
research field, has been extended with many features (e.g., fine-grained
concurrency, weak memory consistency, higher-order programs), been applied to
many programming languages (e.g., Rust), and has been implemented in numerous
verification tools (e.g., F*, Iris, Verifast, Viper, VST). We will discuss
the foundations of separation logic and show how they scale to the
verification of challenging concurrent programs. Exercises and demos using
the Iris framework in the Rocq proof assistant will be provided. |
Attending
The 6
th FoPPS will be co-located with FLOC
2026 the 9th Federated Logic Conference, in the week prior to the
main conferences, and will take place in Lisbon, Portugal. Informations about
registration will be announced soon.
Planned Schedule
|
Mon |
Organizing Committee
Luís Caires, INESC ID and Técnico, University of Lisbon
José Fragoso, INESC ID and Técnico, University of Lisbon
Andreia Mordido, LASIGE and Ciências, University of
Lisbon
Bernardo Toninho, INESC ID and Técnico, University of
Lisbon