Gerhard Goos, Wolf Zimmermann: Verifying Compilers and ASMs. Abstract State Machines 2000: 177-202