This special issue of Logical Methods in Computer Science (LMCS) contains extended versions of selected papers from the Conference on Computer Aided Verification (CAV'05), held in Edinburgh, Scotland, in July 2005.

The program chairs of the conference, in consultation with the program committee, selected papers that were judged to be among the best presented at the conference and invited them for the special issue. All submissions were refereed in accordance with the usual high standards of LMCS.