[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS] Verification of assembly level code



Hi,

Pertti Kellomäki writes:
   Subject: [PVS] Verification of assembly level code
   
Assembly code is in the domain of proof-carrying code. Many
papers in this domain contain example verifications. However,
proof-carrying code only solves security and authentification
issues. In this application domain (eg. network filters) the
verification is usually trivial and can be automated, for
instance in a compiler.

There is also the work of M. Wahab (announced on this list some
years ago):

	@PhdThesis{Wahab:PhD,
	  language =	"english",
	  title =	 "Object Code Verification",
	  author =	 "M. Wahab",
	  month =	 dec,
	  year =	 "1998",
	  school =	 "Department of Computer Science, University of
			 Warwick",
	  address =	 "Coventry, UK",
	  note =	 "Available at URL www.dcs.warwick.ac.uk/reports/367.html",
	}

	@TechReport{Wahab:TechReport,
	  language =	"english",
	  author =	 "M. Wahab",
	  title =	 "Verification and Abstraction of Flow-Graph Programs
			 with Pointers and Computed Jumps",
	  number =	 "CS-RR-354",
	  year =	 "1998",
	  month =	 nov,
	  type =	 "Research Report",
	  url =		 "www.dcs.warwick.ac.uk/pub/reports/354.html",
	  institution =	 "Department of Computer Science, University of
			 Warwick",
	  address =	 "Coventry, UK",
	}


Further, there is work of Tobias Nipkow and his group on Java
bytecode.


If you find a non-trivial verification on assembly level I would
be very much interested. (With non-trivial I mean involving while
loops, recursion, or type casts.)


Bye,

Hendrik