Verification of Safety-critical Software. - B. Scott Andersen; George Romanski (ACM Queue, 2011)