FormaliSE 2025
Sun 27 - Mon 28 April 2025 Ottawa, Ontario, Canada
co-located with ICSE 2025
Events (5 results)

Verifying Multiple TLA+ Configurations with Blast

Research Track When: Mon 28 Apr 2025 14:30 - 15:00 People: Paul Somson, Alcino Cunha

… confidence that the system indeed works correctly for all of them. However …, by enabling the user to easily verify a TLA+ specification for all

Modeling Language for Scenario Development of Autonomous Driving Systems

Research Track When: Sun 27 Apr 2025 11:30 - 12:00 People: Toshiaki Aoki, Takashi Tomita, Tatsuji Kawai, Daisuke Kawakami, Nobuo Chida

… and enumerating all scenarios using a SAT solver. A tool for scenario enumeration …

Detecting Redundant Preconditions

Research Track When: Sun 27 Apr 2025 17:00 - 17:30 People: Nicola Thoben, Heike Wehrheim

… for detecting redundant preconditions. All three techniques are implemented within …

LLM-based Generation of Weakest Preconditions and Precise Array Invariants

Research Track When: Mon 28 Apr 2025 11:00 - 11:30 People: Daragh King, Vasileios Koutavas, Laura Kovács

… The weakest precondition of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of these weakest preconditions is an important task …

Refining Alloy-Based Mutation Operators to Reflect Common Mistakes

Research Track When: Mon 28 Apr 2025 14:00 - 14:30 People: Ana Jovanovic, Mohammad Nurullah Patwary, Allison Sullivan

… , which allows users to explore all valid scenarios that adhere to the model’s …