SymDiff is a differential or relational program verifier for a pair of Boogie programs, with applications on regression verification, compiler translation validation and hyper-safety verification. More information can be found at SymDiff webpage
Instructions to get started: Documentation