QED is a tool that mechanizes correctness proofs in the QED method. The QED method is a novel approach to verifying concurrent programs. QED runs on top of the Boogie system and uses the Z3 theorem prover.
QED is developed at the CADT lab
at Koc University.
More information on the QED project can be found at http://theorem.ku.edu.tr/QED