DSpace Collection:
http://hdl.handle.net/11381/2782974
Thu, 27 Feb 2020 11:18:16 GMT2020-02-27T11:18:16ZCorrect Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification
http://hdl.handle.net/11381/2870718
Title: Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification
Abstract: Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes.... One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form z = x op y and use constraint propagation techniques to infer new information on the variables' possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables x, y or z, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called filtering algorithms are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics.Tue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/11381/28707182019-01-01T00:00:00ZThat's C, baby. C!
http://hdl.handle.net/11381/2870712
Title: That's C, baby. C!
Abstract: Hardly a week goes by at BUGSENG without having to explain to someone that almost any piece of C text, considered in isolation, means absolutely nothing. The belief that C text has meaning in itself is so common, also among seasoned C practitioners, that I thought writing a short paper on the subject was a good time investment. The problem is due to the fact that the semantics of the C programming language is not fully defined: non-definite behavior, predefined macros, different library implementations, peculiarities of the translation process, . . . : all these contribute to the fact that no meaning can be assigned to source code unless full details about the build are available. The paper starts with an exercise that admits a solution. The existence of this solution will hopefully convince anyone that, in general, unless the toolchain and the build procedure are fully known, no meaning can be assigned to any nontrivial piece of C code.Tue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/11381/28707122019-01-01T00:00:00ZLa difesa della competitività economica
http://hdl.handle.net/11381/2870631
Title: La difesa della competitività economicaMon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11381/28706312018-01-01T00:00:00ZEIKASMOS (XXX). Quaderni bolognesi di Filologia
http://hdl.handle.net/11381/2868976
Title: EIKASMOS (XXX). Quaderni bolognesi di FilologiaTue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/11381/28689762019-01-01T00:00:00Z