August 27 – 30 , 2017, Dagstuhl Seminar 17352

Analysis and Synthesis of Floating-point Programs


Eva Darulova (MPI-SWS – Saarbrücken, DE)
Alastair F. Donaldson (Imperial College London, GB)
Zvonimir Rakamaric (University of Utah – Salt Lake City, US)
Cindy Rubio-Gonzalez (University of California – Davis, US)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 7, Issue 8 Dagstuhl Report
Aims & Scope
List of Participants
Dagstuhl's Impact: Documents available
Dagstuhl Seminar Schedule [pdf]

Press Room


This report documents the program and the outcomes of Dagstuhl Seminar 17352 “Analysis and Synthesis of Floating-point Programs”.

Floating-point numbers provide a finite approximation of real numbers that attempts to strike a fine balance between range, precision, and efficiency of performing computations. Nowadays, performing floating-point computations is supported on a wide range of computing platforms, and are employed in many widely-used and important software systems, such as high-performance computing simulations, banking, stock exchange, self-driving cars, and machine learning.

However, writing correct, and yet high-performance and energy-efficient, floating-point code is challenging. For example, floating-point operations are often non-associative (contrary to their real mathematical equivalents), which creates problems when an ordering of operations is modified by either a compiler or due to nondeterministic interleavings of concurrent executions. Furthermore, the underlying floating-point hardware is often heterogeneous, hence different results may be computed across different platforms or even across components of the same heterogeneous platform. Given the underlying complexity associated with writing floating-point code, it is not surprising that there have been numerous software bugs attributed to incorrectly implemented floating-point computations.

Research related to floating-point computation spans a multitude of areas of computer science, ranging from hardware design and architecture, all the way to high-performance computing, machine learning, and software analysis and verification. The objective of this seminar was thus to bring together researchers from several of these areas, which have either traditionally been considered as non-overlapping, or which have arguably enjoyed insufficient interaction despite a clear overlap of interests. The goal in mind here was to provide opportunities to brainstorm new theoretical advances and practical techniques and tools for making floating-point computations performant and correct, and to help foster long term collaborations.

The seminar involved brief presentations from most participants, interspersed with a lot of informal technical discussion, in addition to four breakout sessions based on common themes that arose during informal discussion. In addition, a joint panel session was held between this seminar and the concurrently running “Machine Learning and Formal Methods” seminar. This report presents the collection of abstracts associated with the participant presentations, notes summarising each discussion session, and a transcript of the panel session. We hope that the report will provide a useful resource for researchers today who are interested in understanding the state-of-the-art and open problems related to analysing and synthesising floating-point programs, and as a historical resource helping to clarify the status of this field in 2017.

Summary text license
  Creative Commons BY 3.0 Unported license
  Eva Darulova, Alastair F. Donaldson, Zvonimir Rakamaric, and Cindy Rubio-Gonzalez


  • Programming Languages / Compiler
  • Semantics / Formal Methods
  • Verification / Logic


  • Floating-point arithmetic
  • Program optimization
  • Rigorous compilation
  • Precision allocation
  • Energy-efficient Computing


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.