Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP.

Bishop Brock, Warren A. Hunt Jr.

Browse the full ICCD paper archive.