Usually it isn't about execution of programs, but analysis of their properties. To do so you can use eg model checking, and you require a semantic definition f

Usually it isn't about execution of programs, but analysis of their properties. To do so you can use eg model checking, and you require a semantic definition for doing so. I don't recall floating point stuff being hard to encode. See eg the flocq project.