In my Ph.D. thesis work, I designed a logic that modularly verifies properties of program fragments. The logic works directly on program fragments with multiple entries and multiple exits. It provides inference rules to combine fragments together and eliminate intermediate entries and exits. I showed this logic to be both sound and (relatively) complete with respect to a small-step machine semantics. In the FPCC project, I used this logic to construct a soundness proof for a full-fledged Typed Assembly Language (TAL). All proofs were formally developed in a theorem prover and rigorously checked.
Construction of a Semantic Model for a Typed Assembly Language. Gang Tan, Andrew W. Appel, Kedar Swadi and Dinghao Wu. In Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 04), LNCS 2937, pages 30-43, Springer, January 2004.