Validating Semantics

Joe Kiniry gave a talk entitled Validating Semantics to the IFIP working group on "Verified Software" (WG 1.9/2.15) on Wednesday the 14th of December, 2011 in York, UK.

Validating Semantics Abstract:

How might one automatically check that a formalized theory that is meant to describe a real, physical system actually describes the system in question? For example, if one wishes to reason about Java programs, and one mechanizes a semantics of Java in a theorem prover, how can you be sure that your semantics matches the actual behavior of the Java compiler and virtual machine?