FSE 2025
Mon 23 - Fri 27 June 2025 Trondheim, Norway
co-located with ISSTA 2025
Tue 24 Jun 2025 11:30 - 11:50 at Cosmos 3A - Verification and Validation Chair(s): Alex Orso

Floating-point constraint solving is challenging due to the complex representation and non-linear computations. Search-based constraint solving provides an effective method for solving floating-point constraints. In this paper, we propose QSF to improve the efficiency of search-based solving for floating-point constraints. The key idea of QSF is to model the floating-point constraint solving problem as a multi-objective optimization problem. Specifically, QSF considers both the number of unsatisfied constraints and the sum of the violation degrees of unsatisfied constraints as the objectives for search-based optimization. Besides, we propose a new evolutionary algorithm in which the mutation operators are specially designed for floating-point numbers, aiming to solve the multi-objective problem more efficiently. We have implemented QSF and conducted extensive experiments on both the SMT-COMP benchmark and the benchmark from real-world floating-point programs. The results demonstrate that compared to SOTA floating-point solvers, QSF achieved an average speedup of 15.72X under a 60-second timeout and an impressive 87.48X under a 600-second timeout on the first benchmark. Similarly, on the second benchmark, QSF delivered an average speedup of 25.74X and 106.76X, respectively, under the two timeout configurations. Furthermore, QSF has also enhanced the performance of symbolic execution for floating-point programs.

Tue 24 Jun

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

10:30 - 12:30
Verification and ValidationDemonstrations / Ideas, Visions and Reflections / Research Papers / Journal First at Cosmos 3A
Chair(s): Alex Orso Georgia Institute of Technology
10:30
10m
Talk
TraceMOP: An Explicit-Trace Runtime Verification Tool for Java
Demonstrations
Kevin Guan Cornell University, Owolabi Legunsen Cornell University
10:40
10m
Talk
VO-GCSE: Verification Optimization through Global Common Subexpression Elimination
Demonstrations
Rafael Menezes University of Manchester, Norbert Tihanyi Technology Innovation Institute, Ridhi Jain Technology Innovation Institute (TII), Abu Dhabi, UAE, Alexander Levin Nvidia, Rosiane de Freitas Federal University of Amazonas, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil
10:50
10m
Talk
GIVUP: Automated Generation and Verification of Textual Process Descriptions
Demonstrations
Quentin Nivon University Grenoble Alpes, Gwen Salaün University of Grenoble Alpes, Frederic Lang Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Grenoble, France
11:00
10m
Talk
NeuroStrata: Harnessing Neuro-Symbolic Paradigms for Improved Testability and Verifiability of Autonomous CPS
Ideas, Visions and Reflections
Xi Zheng Macquarie University, Ziyang Li University of Pennsylvania, Ivan Ruchkin University of Florida, Ruzica Piskac Yale University, Miroslav Pajic Duke University
11:10
20m
Talk
Scene Flow Specifications: Encoding and Monitoring Rich Temporal Safety Properties of Autonomous Systems
Research Papers
Trey Woodlief University of Virginia, United States, Felipe Toledo , Matthew B Dwyer University of Virginia, Sebastian Elbaum University of Virginia
DOI
11:30
20m
Talk
QSF: Multi-Objective Optimization based Efficient Solving for Floating-Point Constraints
Research Papers
Xu Yang College of Computer Science and Technology, National University of Defense Technology, Zhenbang Chen College of Computer, National University of Defense Technology, Wei Dong National University of Defense Technology, Ji Wang National University of Defense Technology
DOI
11:50
20m
Talk
Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications
Journal First
Mirko Köhler TU Darmstadt, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen
12:10
20m
Talk
ChangeGuard: Validating Code Changes via Pairwise Learning-Guided Execution
Research Papers
Lars Gröninger University of Stuttgart, Beatriz Souza Universität Stuttgart, Michael Pradel University of Stuttgart
DOI

Information for Participants
Tue 24 Jun 2025 10:30 - 12:30 at Cosmos 3A - Verification and Validation Chair(s): Alex Orso
Info for room Cosmos 3A:

Cosmos 3A is the first room in the Cosmos 3 wing.

When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.

:
:
:
: