This paper by Banterle and Giacobazzi at Università degli Studi di Verona presents an efficient implementation of the Octagon Abstract Domain (OAD) on graphics hardware. OAD is a relational numerical abstract domain which approximates invariants as conjunctions of constraints of the form +/- x +/- y <= c, where x and y are program variables and c is a constant which can be an integer, rational or real. OAD has been used with success in the aerospace industry for analyzing C programs such as the flight control software for the Airbus A340 fly-by-wire system. ( A Fast Implementation of the Octagon Abstract Domain on Graphics Hardware. Francesco Banterle and Roberto Giacobazzi. Proceeding of The 14th International Static Analysis Symposium (SAS). 2007)