FormaliSE

International Conference on Formal Methods in Software Engineering

Conference Program

GMT - Greenwich Mean Time -

(GMT hours)

Meeting Room: Eugénio de Andrade

Meeting Room: Eugénio de Andrade

SpeakerCristian Cadar

TITLE: FormalISE: Reflections on Formal and Informal Methods in Software Engineering

ABSTRACT: In this talk, I reflect on formal and informal methods that are, or are becoming available to software engineers, ranging from manual testing to static analysis, fuzzing, symbolic execution and formal verification. These reflections are shaped by my experiences designing and applying different forms of program analysis techniques (with a focus on the middle ground between formal and informal methods) to a wide range of software systems and software engineering problems.

Session chair Antónia Lopes

10:30 AM - 11:00 AM

Meeting Room: Eugénio de Andrade

11:00 AM

Contract Automata: A Specification Language for Mode-Based Systems

Authors: Alexander Weigl, Joshua Bachmeier, Bernhard Beckert, Mattias Ulbrich

11:30 AM

Finite Automata synthesis from Interactions

Authors: Erwan Mahe, Boutheina Bannour, Christophe Gaston, Arnault Lapitre, Pascale Le Gall

12:00 AM

Preprocessing is What You Need: Understanding and Predicting the Complexity of SAT-based Uniform Random Sampling

Authors: Olivier Zeyen, Maxime Cordy, Gilles Perrouin, Mathieu ACHER

Session chairDomenico Bianculli

12:30 AM - 02:00 PM

Meeting Room: Eugénio de Andrade

02:00 PM

Diagnosing Violations of Time-based Properties Captured in iCFTL

Authors: Cristina Stratan, Joshua Heneage Dawes, Domenico Bianculli

3:00 PM

Time for Networks: Mutation Testing for Timed Automata Networks

Authors: David Cortés, James Ortiz, Davide Basile, Jesus Aranda, Gilles Perrouin, Pierre Yves Schobbens

02:30 PM

Verifying Opacity of Discrete-Timed Automata

Authors: Julian Klein, Paul Kogel, Sabine Glesner

Session chairJoão Ferreira

03:30 PM - 04:00 PM

Meeting Room: Eugénio de Andrade

04:00 PM

Automated Repair of Violated Eventually Properties in Concurrent Programs

Authors: Irman Faqrizal, Quentin Nivon, Gwen Salaün

04:30 PM

Compositional Analysis of Parametric Cooperative Cyber-Physical Systems

Authors: Raniah Alghamdi, Richard Trefler

05:00 PM

Formal Methods in Requirements Engineering: Survey and Future Directions

Authors: Robert Lorch, Baoluo Meng, Kit Siu, Abha Moitra, Michael Durling, Saswata Paul, Sarat Chandra Varanasi, Craig McMillan

Session chairCristian Cadar

Meeting Room: Eugénio de Andrade

SpeakerClaire Dross

TITLE: Two-way collaboration between flow and proof in SPARK

ABSTRACT: There are various kinds of static (and dynamic) verification frameworks and tools, all with weaknesses and strengths. Combining them manually or automatically is common by making different tools interoperate or integrating various analyses in the same tool. In SPARK, two analyses work on different paths: deductive verification and data and information flow analysis. This talk presents how these analyses collaborate to improve the efficiency and precision of the SPARK tool while retaining soundness.

Session chairCarlo A. Furia

10:30 AM - 11:00 AM

Meeting Room: Eugénio de Andrade

11:00 AM

A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification

Authors: Louis Gauthier, Virgile Prevosto, Julien Signoles

11:30 AM

Formally Verified Interval Arithmetic and Its Application to Program Verification

Authors: Achim D. Brucker, Teddy Cameron-Burke, Amy Stell

12:00 AM

Towards Verifiable Multi-Agent Interaction Pattern Specification

Authors: Alberto Tagliaferro, Livia Lestingi, Matteo Rossi

Session chairClaire Dross

12:30 AM - 02:00 PM

Meeting Room: Eugénio de Andrade

02:00 PM

Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets

Authors: Preston K. Robinette, Diego Manzanas Lopez, Serena Serbinowska, Kevin Leach, Taylor T Johnson

02:30 PM

Leveraging Large Language Models to Boost Dafny's Developers Productivity

Authors: Álvaro F. Silva, Alexandra Mendes, João F. Ferreira

Session chairStefania Gnesi

Meeting Room: Eugénio de Andrade

SESSION CHAIR

03:30 PM - 04:00 PM