{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T18:23:27Z","timestamp":1740162207053,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T00:00:00Z","timestamp":1479340800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Cryptogr Eng"],"published-print":{"date-parts":[[2017,4]]},"DOI":"10.1007\/s13389-016-0145-2","type":"journal-article","created":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T06:27:05Z","timestamp":1479364025000},"page":"63-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["SMASHUP: a toolchain for unified verification of hardware\/software co-designs"],"prefix":"10.1007","volume":"7","author":[{"given":"Florian","family":"Lugou","sequence":"first","affiliation":[]},{"given":"Ludovic","family":"Apvrille","sequence":"additional","affiliation":[]},{"given":"Aur\u00e9lien","family":"Francillon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,17]]},"reference":[{"key":"145_CR1","doi-asserted-by":"crossref","unstructured":"Allamigeon, X., Blanchet, B.: Reconstruction of attacks against cryptographic protocols. In: 18th IEEE Workshop on Computer Security Foundations, 2005 (CSFW-18, 2005) (2005)","DOI":"10.1109\/CSFW.2005.25"},{"key":"145_CR2","unstructured":"Apvrille, L., Roudier, Y.: SysML-Sec: A SysML environment for the design and development of secure embedded systems. In: APCOSEC 2013 (2013)"},{"key":"145_CR3","unstructured":"Arias, O., Davi, L., Hanreich, M., Jin, Y., Koeberl, P., Paul, D., Sadeghi, A.R., Sullivan, D.: HAFIX: hardware-assisted flow integrity extension. In: 52nd Design Automation Conference (DAC) (2015)"},{"key":"145_CR4","doi-asserted-by":"crossref","unstructured":"Armstrong, R.C., Punnoose, R.J., Wong, M.H., Mayo, J.R.: Survey of existing tools for formal verification. Tech. rep., Sandia National Laboratories (2014)","DOI":"10.2172\/1166644"},{"key":"145_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"145_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings 14th IEEE Computer Security Foundations Workshop, 2001 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"145_CR7","unstructured":"Blanchet, B., Smyth, B., Cheval, V.: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. CNRS, Departement dInformatique, Ecole Normale Superieure, Paris (2015)"},{"key":"145_CR8","doi-asserted-by":"crossref","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.: BAP: a binary analysis platform. In: Proceedings of the 23rd International Conference on Computer Aided Verification (2011)","DOI":"10.1007\/978-3-642-22110-1_37"},{"issue":"7","key":"145_CR9","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.65","volume":"21","author":"P Camurati","year":"1988","unstructured":"Camurati, P., Prinetto, P.: Formal verification of hardware correctness: introduction and survey of current research. Computer 21(7), 8\u201319 (1988)","journal-title":"Computer"},{"key":"145_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification (2000)","DOI":"10.1007\/10722167_15"},{"issue":"3","key":"145_CR11","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TSE.1976.233817","volume":"2","author":"L Clarke","year":"1976","unstructured":"Clarke, L.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215\u2013222 (1976)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"145_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-55481-0","volume-title":"Programming in PROLOG","author":"W Clocksin","year":"2003","unstructured":"Clocksin, W., Mellish, C.S.: Programming in PROLOG. Springer, New York (2003)"},{"key":"145_CR13","doi-asserted-by":"crossref","unstructured":"Danger, J.L., Guilley, S., Porteboeuf, T., Praden, F., Timbert, M.: HCODE: hardware-enhanced real-time CFI. In: Proceedings of the 4th Program Protection and Reverse Engineering Workshop (2014)","DOI":"10.1145\/2689702.2689708"},{"key":"145_CR14","unstructured":"Davidson, D., Moench, B., Ristenpart, T., Jha, S.: FIE on firmware: finding vulnerabilities in embedded systems using symbolic execution. In: Proceedings of the 22nd USENIX Security Symposium (USENIX Security 13) (2013)"},{"issue":"2","key":"145_CR15","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"145_CR16","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165\u20131178 (2008)","DOI":"10.1109\/TCAD.2008.923410"},{"key":"145_CR17","unstructured":"Dullien, T., Porst, S.: REIL: A Platform-Independent Intermediate Representation of Disassembled Code for Static Code Analysis (2009). http:\/\/www.zynamics.com\/downloads\/csw09.pdf"},{"key":"145_CR18","unstructured":"El\u00a0Defrawy, K., Francillon, A., Perito, D., Tsudik, G.: SMART: secure and minimal architecture for (establishing a dynamic) root of trust. In: Proceedings of the Network and Distributed System Security Symposium (NDSS), San Diego (2012)"},{"key":"145_CR19","doi-asserted-by":"crossref","unstructured":"Fox, A., Myreen, M.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Interactive Theorem Proving (2010)","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"145_CR20","doi-asserted-by":"crossref","unstructured":"Hong, S., Oguntebi, T., Casper, J., Bronson, N., Kozyrakis, C., Olukotun, K.: A case of system-level hardware\/software co-design and co-verification of a commodity multi-processor system with custom hardware. In: Proceedings of the Eighth IEEE\/ACM\/IFIP International Conference on Hardware\/Software Codesign and System Synthesis (2012)","DOI":"10.1145\/2380445.2380524"},{"issue":"2","key":"145_CR21","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.R.: Formal verification in hardware design: a survey. ACM Trans. Des. Autom. Electron. Syst. 4(2), 123\u2013193 (1999)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"145_CR22","doi-asserted-by":"crossref","unstructured":"Koeberl, P., Schulz, S., Sadeghi, A.R., Varadharajan, V.: TrustLite: a security architecture for tiny embedded devices. In: Proceedings of the Ninth European Conference on Computer Systems (2014)","DOI":"10.1145\/2592798.2592824"},{"key":"145_CR23","doi-asserted-by":"crossref","unstructured":"Kroening, D., Sharygina, N.: Formal verification of systemC by automatic hardware\/software partitioning. In: Proceedings of the 2nd ACM\/IEEE International Conference on Formal Methods and Models for Co-Design (2005)","DOI":"10.1109\/MEMCOD.2005.1487900"},{"key":"145_CR24","unstructured":"Noorman, J., Agten, P., Daniels, W., Strackx, R., Van\u00a0Herrewege, A., Huygens, C., Preneel, B., Verbauwhede, I., Piessens, F.: Sancus: low-cost trustworthy extensible networked devices with a zero-software trusted computing base. In: Presented as part of the 22nd USENIX Security Symposium (USENIX Security 13) (2013)"},{"key":"145_CR25","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th Colloquium on International Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"4","key":"145_CR26","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/1721695.1721702","volume":"9","author":"B Schlich","year":"2010","unstructured":"Schlich, B.: Model checking of software for microcontrollers. ACM Trans. Embed. Comput. Syst. 9(4), 36 (2010)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"145_CR27","doi-asserted-by":"crossref","first-page":"135","DOI":"10.2197\/ipsjtsldm.6.135","volume":"6","author":"B Schmidt","year":"2013","unstructured":"Schmidt, B., Villarraga, C., Fehmel, T., Bormann, J., Wedler, M., Nguyen, M., Stoffel, D., Kunz, W.: A new formal verification approach for hardware-dependent embedded system software. IPSJ Trans. Syst. LSI Des. Methodol. 6, 135\u2013145 (2013)","journal-title":"IPSJ Trans. Syst. LSI Des. Methodol."},{"key":"145_CR28","unstructured":"Semeria, L., Ghosh, A.: Methodology for hardware\/software co-verification in C\/C++. In: Proceedings of the Asia and South Pacific Design Automation Conference, 2000 (ASP-DAC 2000) (2000)"},{"key":"145_CR29","doi-asserted-by":"crossref","unstructured":"Subramanyan, P., Arora, D.: Formal verification of taint-propagation security properties in a commercial SoC design. In: Design, Automation and Test in Europe Conference and Exhibition (DATE) (2014)","DOI":"10.7873\/DATE.2014.326"},{"key":"145_CR30","unstructured":"Villarraga, C., Schmidt, B., Bormann, J., Bartsch, C., Stoffel, D., Kunz, W.: An equivalence checker for hardware-dependent embedded system software. In: 2013 Eleventh IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE) (2013)"},{"key":"145_CR31","doi-asserted-by":"crossref","unstructured":"Villarraga, C., Schmidt, B., Bao, B., Raman, R., Bartsch, C., Fehmel, T., Stoffel, D., Kunz, W.: Software in a hardware view: new models for hw-dependent software in soc verification and test. In: 2014 International Test Conference (2014)","DOI":"10.1109\/TEST.2014.7035308"}],"container-title":["Journal of Cryptographic Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-016-0145-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s13389-016-0145-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-016-0145-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T14:03:23Z","timestamp":1568556203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s13389-016-0145-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,17]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["145"],"URL":"https:\/\/doi.org\/10.1007\/s13389-016-0145-2","relation":{},"ISSN":["2190-8508","2190-8516"],"issn-type":[{"type":"print","value":"2190-8508"},{"type":"electronic","value":"2190-8516"}],"subject":[],"published":{"date-parts":[[2016,11,17]]}}}