Results from the Verification of Models of Spectrum Auctions