An Executable Model of the JVM in Coq

Add to your list(s) Download to your calendar using vCal

• Robert Atkey, LFCS, Edinburgh
• Friday 18 May 2007, 14:00-15:00
• FW11.

If you have a question about this talk, please contact Tom Ridge.

CoqJVM is an executable formalisation of the Java Virtual Machine written in the Coq proof assistant. On one hand it can be extracted from Coq as an O’Caml program and used to execute Java bytecode. On the other hand it can be used to prove the soundness of program logics for bytecode. We intend to use the model to prove the soundness of a program logic and proof checker for proof carrying code. The fact that the model can be executed helps to ensure that the formalisation faithfully models a real Java Virtual Machine.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.