Automatic Generation of Loop Invariants in Dafny with Large Language Models (FSEN 2025 - Research Papers)

Mon 7 - Tue 8 April 2025 Västerås, Sweden

Who

João Pascoal Faria, Emanuel Trigo, Rui Abreu

Track

FSEN 2025 Research Papers

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Mon 7 Apr 2025 17:00 - 17:30 - Conference session 4 Chair(s): Mieke Massink

João Pascoal Faria

Faculty of Engineering, University of Porto and INESC TEC

Portugal

Emanuel Trigo

Faculty of Engineering, University of Porto, Portugal

Portugal

Rui Abreu

Faculty of Engineering of the University of Porto, Portugal

Portugal

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Mon 7 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30	Conference session 4 Research Papers Chair(s): Mieke Massink CNR-ISTI Pisa, Italy

16:00 30m Research paper		Shielded Online Reinforcement Learning for Stormwater Detention PondsBest Paper Award Research Papers Esther Hahyeon Kim Aalborg University, Martijn Goorden , Kim Larsen Aalborg University, Thomas Dyhre Nielsen Aalborg University
16:30 30m Research paper		Extracting Formal Models for User’s Behaviors in Social Networks using Automata and Machine Learning Research Papers Negar Kashef University of Tehran, Fatemeh Ghassemi University of Tehran
17:00 30m Research paper		Automatic Generation of Loop Invariants in Dafny with Large Language Models Research Papers João Pascoal Faria Faculty of Engineering, University of Porto and INESC TEC, Emanuel Trigo Faculty of Engineering, University of Porto, Portugal, Rui Abreu Faculty of Engineering of the University of Porto, Portugal