Mathematical programming based debugging

8 years 7 months ago
Mathematical programming based debugging
Verifying that a piece of software has no bugs means proving that it has certain desired properties, such as an array index not taking values outside certain Abstract interpretation is used in the static analysis of code to establish the inclusion-wise smallest set of values (numerical invariant) that the program variables can attain during program execution. Such sets can be used to detect run-time errors without actually running the program. We present a mathematical program that determines guaranteed smallest interval invariants of computer programs with integer affine arithmetics and compare our results to existing techniques.
Leo Liberti, Stéphane Le Roux, Jeremy Lecon
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2010
Where ENDM
Authors Leo Liberti, Stéphane Le Roux, Jeremy Leconte, Fabrizio Marinelli
Comments (0)