Section 5.2, Validation: "Code sequences are converted into SMT formulae ... and used to produce a query which asks whether both sequences produce the same side effects on live outputs when executed from the same initial machine state."