Program Round-off Error Certifier via Static Analysis


PRECiSA (Program Round-off Error Certifier via Static Analysis) is a fully automatic analyzer for the estimation of round-off errors of floating-point valued functional expressions.

The input to PRECiSA is a program composed of floating-point valued functions. In its currrent version, PRECiSA accepts a subset of the language of the Prototype Verification System (PVS), including LET expressions, IF-THEN-ELSE constructions, non-recursive function calls, and floating point values and operations such as: addition, multiplication, division, subtraction, floor, and square root.

How to use the web interface

Choose a predefined program from the drop-down list or write your own following the syntax defined here. It is assumed by PRECiSA that the input program is type correct. The use of PVS to type check the program and to prove any TCC elicited in that process in highly recommended.

Ranges for the input variables of each function of your program must be given in the "Input ranges" box as:

<fun>(<var1>,...,<varn>): <var1> in [<l1>,< u1>],...,<varn> in [< ln>,<un>]

where <fun> is a function with formal parameters <var1>,...,<varn>; and for every index i in [1,n], <li> and <ui> are numerical values such that <vari> is assumed to range in the interval [<li>,<ui>]. Note that, when you load a predefined program, a possible set of ranges for the input variables is displayed in the aforementioned text area. These values can be later modified.

In the same way, the user can select subprogram (or decision paths) of interest in the "Decision paths of interest" box. The user can specify these paths by listing the paths/sub-programs of interests as a list of True and False (for example [True,False,True]). The analysis is done for all the execution paths in the program, or better for all combination of real/FP execution path in the program). Since the number of these paths is exploding for nested if-then-else, this selection allows the user to select zero or more sub-programs or expressions of interest. For these sub-programs, a dedicated error expression representing the round-off error estimation is computed. For the other sub-programs, the tool will generate a unique error which is the maximum of all the round-off error estimations corresponding to these paths. If the user does not select any sub-program of interest (None), the tool will just produce the overall round-off error for the stable case and for the unstable one. If the user is interested in a precise analysis of the entire program (All), the analysis will generate a semantic element for each combination of real/FP execution path in the program. Therefore, there is a tradeoff between the number of sub-programs of interest and the efficiency of the analysis. Note that, when you load a predefined program, a possible set of decision paths of interest is displayed in the aforementioned text area. These values can be later modified.

By pressing the button "Analyze with PRECiSA", the analysis will produce the error estimation and display it in the "Output " box. (notice that in this version of the web interface the parameters used for the branch-and-bound search are max-depth=9 and precision=10-16)

By default, PRECiSA correctly handles conditionals (see this paper for details.). However, by checking the corresponding option the stable test assumption can be applied.


Input ranges

Decision paths of interest

 Stable tests assumption



Mariano Moscato, Laura Titolo, Aaron Dutle, and Cesar Muñoz
"Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis" (SAFECOMP 2017)

Laura Titolo, Marco A. Feliu, Mariano Moscato, and Cesar Muñoz
"An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs" (VMCAI 2018)

The open-source code of PRECiSA and more examples are available at the github page PRECiSA .

Contact Information

Laura Titolo:
Mariano Moscato:
Marco Feliu:
Cesar Muñoz:

NIA logo