Jens Knoop, George C. Necula, Wolf Zimmermann
Proceedings of the Fourth International Workshop on Compiler Optimization meets Compiler Verification
COCV-J-2005, 2005.

@proceedings{COCV-J-2005,
	editor        = "Jens Knoop and George C. Necula and Wolf Zimmermann",
	journal       = "{Electronic Notes in Theoretical Computer Science}",
	number        = 2,
	title         = "{Proceedings of the Fourth International Workshop on Compiler Optimization meets Compiler Verification}",
	volume        = 141,
	year          = 2005,
}

Event page: http://www.complang.tuwien.ac.at/knoop/COCV2005/cocv2005.html

Contents (6 items)

2 ×#correctness
2 ×#optimisation
2 ×#proving

COCV-J-2005-Langmaack #question #reasoning #what

What Level of Mathematical Reasoning can Computer Science Demand of a Software Implementer? (HL), pp. 5–32.

COCV-J-2005-BlechGLM #code generation #comparison #correctness #higher-order #optimisation #proving

Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.

COCV-J-2005-SalcianuA #analysis #correctness #data flow #proving

Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses (AS, KA), pp. 53–68.

COCV-J-2005-HuBGP #optimisation #validation

Validating More Loop Optimizations (YH, CWB, BG, AP), pp. 69–84.

COCV-J-2005-GalPF05a #encoding

Structural Encoding of Static Single Assignment Form (AG, CWP, MF), pp. 85–102.

COCV-J-2005-AmmeRF #mobile

Quantifying the Benefits of SSA-Based Mobile Code (WA, JvR, MF), pp. 103–119.