University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > An Executable Model of the JVM in Coq

An Executable Model of the JVM in Coq

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

  • UserRobert Atkey, LFCS, Edinburgh
  • ClockFriday 18 May 2007, 14:00-15:00
  • HouseFW11.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity