@inproceedings{'JMS5',
title = {{Towards Verified Faithful Simulation} },
author = {Joloboff, Vania and Monin, Jean-Fran\c{c}ois and Shi, Xiaomu},
year = {2015},
booktitle = {Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, {SETTA} 2015, Nanjing, China, November 4-6, 2015, Proceedings},
pages = {105--119},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {9409},
team = {PACSS},
pdf = {Docs/setta15.pdf},
abstract = {This paper presents an approach to construct a verified virtual prototyping framework of embedded software. The machine code executed on a simulated target architecture can be proven to provide the same results as the real hardware, and the proof is verified with a theorem prover. The method consists in proving each instruction of the instruction set independently, by proving that the execution of the C code simulating an instruction yields an identical result to that obtained by a formal executable model of the processor architecture. This formal model itself is obtained through an automated translation process from the architecture specifications. Each independent proof draws a number of lemmas from a generic lemma library and also uses the automation of inversion tactics in the theorem prover. The paper presents the proof of the ARM architecture version 6 Instruction Set Simulator of the SimSoC open source simulator, with all of the proofs being verified by the Coq proof assistant, using automated tactics to reduce manual proof development.},
}
