Integrating Software and Hardware Verification

M.-C. Jakobs, M. Platzner, T. Wiersema, H. Wehrheim, in: E. Albert, E. Sekerinski (Eds.), Proceedings of the 11th International Conference on Integrated Formal Methods (IFM), 2014, pp. 307–322.

Download
Restricted 408-jakobs14_ifm.pdf 561.33 KB
Conference Paper
Editor
;
Abstract
Verification of hardware and software usually proceeds separately, software analysis relying on the correctness of processors executing instructions. This assumption is valid as long as the software runs on standard CPUs that have been extensively validated and are in wide use. However, for processors exploiting custom instruction set extensions to meet performance and energy constraints the validation might be less extensive, challenging the correctness assumption.In this paper we present an approach for integrating software analyses with hardware verification, specifically targeting custom instruction set extensions. We propose three different techniques for deriving the properties to be proven for the hardware implementation of a custom instruction in order to support software analyses. The techniques are designed to explore the trade-off between generality and efficiency and span from proving functional equivalence over checking the rules of a particular analysis domain to verifying actual pre and post conditions resulting from program analysis. We demonstrate and compare the three techniques on example programs with custom instructions, using stateof-the-art software and hardware verification techniques.
Publishing Year
Proceedings Title
Proceedings of the 11th International Conference on Integrated Formal Methods (iFM)
Page
307-322
LibreCat-ID

Cite this

Jakobs M-C, Platzner M, Wiersema T, Wehrheim H. Integrating Software and Hardware Verification. In: Albert E, Sekerinski E, eds. Proceedings of the 11th International Conference on Integrated Formal Methods (IFM). LNCS. ; 2014:307-322. doi:10.1007/978-3-319-10181-1_19
Jakobs, M.-C., Platzner, M., Wiersema, T., & Wehrheim, H. (2014). Integrating Software and Hardware Verification. In E. Albert & E. Sekerinski (Eds.), Proceedings of the 11th International Conference on Integrated Formal Methods (iFM) (pp. 307–322). https://doi.org/10.1007/978-3-319-10181-1_19
@inproceedings{Jakobs_Platzner_Wiersema_Wehrheim_2014, series={LNCS}, title={Integrating Software and Hardware Verification}, DOI={10.1007/978-3-319-10181-1_19}, booktitle={Proceedings of the 11th International Conference on Integrated Formal Methods (iFM)}, author={Jakobs, Marie-Christine and Platzner, Marco and Wiersema, Tobias and Wehrheim, Heike}, editor={Albert, Elvira and Sekerinski, EmilEditors}, year={2014}, pages={307–322}, collection={LNCS} }
Jakobs, Marie-Christine, Marco Platzner, Tobias Wiersema, and Heike Wehrheim. “Integrating Software and Hardware Verification.” In Proceedings of the 11th International Conference on Integrated Formal Methods (IFM), edited by Elvira Albert and Emil Sekerinski, 307–22. LNCS, 2014. https://doi.org/10.1007/978-3-319-10181-1_19.
M.-C. Jakobs, M. Platzner, T. Wiersema, and H. Wehrheim, “Integrating Software and Hardware Verification,” in Proceedings of the 11th International Conference on Integrated Formal Methods (iFM), 2014, pp. 307–322.
Jakobs, Marie-Christine, et al. “Integrating Software and Hardware Verification.” Proceedings of the 11th International Conference on Integrated Formal Methods (IFM), edited by Elvira Albert and Emil Sekerinski, 2014, pp. 307–22, doi:10.1007/978-3-319-10181-1_19.
Main File(s)
File Name
408-jakobs14_ifm.pdf 561.33 KB
Access Level
Restricted Closed Access
Last Uploaded
2018-03-16T11:35:28Z


Export

Marked Publications

Open Data LibreCat

Search this title in

Google Scholar