Algebraic models of behaviour and correctness of SMT and CMT processors - Neal Harman (The Journal of Logic and Algebraic Programming, 2007)