Automatic Verification of Linear Controller Software