{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T09:05:28Z","timestamp":1726045528416},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030311568"},{"type":"electronic","value":"9783030311575"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31157-5_1","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:03:06Z","timestamp":1569178986000},"page":"3-20","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["When Are Software Verification Results Valid for Approximate Hardware?"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Isenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Pauck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"1_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Boston (1986)"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1145\/2914770.2837628","volume":"51","author":"Aws Albarghouthi","year":"2016","unstructured":"Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: Proceedings of the POPL, pp. 789\u2013801. ACM (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"KR Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer, London (2009). \n                      https:\/\/doi.org\/10.1007\/978-1-84882-745-5"},{"issue":"1","key":"1_CR4","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. STTT 5(1), 49\u201358 (2003)","journal-title":"STTT"},{"key":"1_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). \n                      http:\/\/www.SMT-LIB.org"},{"key":"1_CR6","unstructured":"ABC, Berkeley: A system for sequential synthesis and verification (2005)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-71316-6_19","volume-title":"Programming Languages and Systems","author":"F Besson","year":"2007","unstructured":"Besson, F., Jensen, T.P., Turpin, T.: Small witnesses for abstract interpretation-based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 268\u2013283. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71316-6_19"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31"},{"key":"1_CR9","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proceedings of the FMCAD, pp. 189\u2013198. IEEE (2010)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"1_CR11","unstructured":"Biere, A.: Picosat (2013). \n                      http:\/\/fmv.jku.at\/picosat"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Carbin, M., Kim, D., Misailovic, S., Rinard, M.C.: Verified integrity properties for safe approximate program transformations. In: Proceedings of the PEPM, pp. 63\u201366. ACM (2013)","DOI":"10.1145\/2426890.2426901"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Carbin, M., Misailovic, S., Rinard, M.C.: Verifying quantitative reliability for programs that execute on unreliable hardware. In: Proceedings of the OOPSLA, pp. 33\u201352. ACM (2013)","DOI":"10.1145\/2544173.2509546"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of the PLDI, pp. 415\u2013426. ACM (2006)","DOI":"10.1145\/1133255.1134029"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Han, J., Orshansky, M.: Approximate computing: an emerging paradigm for energy-efficient design. In: Proceedings of the ETS, pp. 1\u20136. IEEE Computer Society (2013)","DOI":"10.1109\/ETS.2013.6569370"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-40648-0_19","volume-title":"NASA Formal Methods","author":"S He","year":"2016","unstructured":"He, S., Lahiri, S.K., Rakamari\u0107, Z.: Verifying relative safety, accuracy, and termination for program approximations. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 237\u2013254. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40648-0_19"},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/s10817-017-9421-9","volume":"60","author":"S He","year":"2018","unstructured":"He, S., Lahiri, S.K., Rakamaric, Z.: Verifying relative safety, accuracy, and termination for program approximations. JAR 60(1), 23\u201342 (2018)","journal-title":"JAR"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the POPL, pp. 232\u2013244. ACM (2004)","DOI":"10.1145\/982962.964021"},{"key":"1_CR21","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symposium on Semantics of Algorithmic Languages","author":"CAR Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 102\u2013116. Springer, Heidelberg (1971). \n                      https:\/\/doi.org\/10.1007\/BFb0059696"},{"key":"1_CR22","unstructured":"Isenberg, T., Jakobs, M.C., Pauck, F., Wehrheim, H.: Deriving Approximation Tolerance Constraints from Verification Runs. CoRR abs\/1604.08784 (2016). \n                      http:\/\/arxiv.org\/abs\/1604.08784"},{"issue":"1","key":"1_CR23","first-page":"22","volume":"10","author":"T Isenberg","year":"2018","unstructured":"Isenberg, T., Jakobs, M., Pauck, F., Wehrheim, H.: Validity of software verification results on approximate hardware. ESL 10(1), 22\u201325 (2018)","journal-title":"ESL"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-319-22969-0_12","volume-title":"Software Engineering and Formal Methods","author":"M-C Jakobs","year":"2015","unstructured":"Jakobs, M.-C.: Speed up configurable certificate validation by certificate reduction and partitioning. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 159\u2013174. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-22969-0_12"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-319-57288-8_28","volume-title":"NASA Formal Methods","author":"M-C Jakobs","year":"2017","unstructured":"Jakobs, M.-C., Wehrheim, H.: Compact proof witnesses. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 389\u2013403. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-57288-8_28"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Kahng, A.B., Kang, S.: Accuracy-configurable adder for approximate arithmetic designs. In: Proceedings of the DAC, pp. 820\u2013825. ACM (2012)","DOI":"10.1145\/2228360.2228509"},{"issue":"5","key":"1_CR27","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/2742482","volume":"58","author":"L Kugler","year":"2015","unstructured":"Kugler, L.: Is \u201cgood enough\u201d computing good enough? Commun. ACM 58(5), 12\u201314 (2015)","journal-title":"Commun. ACM"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: progress (1996)","DOI":"10.1007\/978-1-4612-4222-2"},{"issue":"10","key":"1_CR29","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1145\/2714064.2660231","volume":"49","author":"Sasa Misailovic","year":"2014","unstructured":"Misailovic, S., Carbin, M., Achour, S., Qi, Z., Rinard, M.C.: Chisel: reliability- and accuracy-aware optimization of approximate computational kernels. In: Proceedings of the OOPSLA, pp. 309\u2013328. ACM (2014)","journal-title":"ACM SIGPLAN Notices"},{"issue":"4","key":"1_CR30","first-page":"1","volume":"48","author":"Sparsh Mittal","year":"2016","unstructured":"Mittal, S.: A survey of techniques for approximate computing. ACM Comput. Surv. 48(4), 62:1\u201362:33 (2016)","journal-title":"ACM Computing Surveys"},{"key":"1_CR31","unstructured":"Pauck, F.: Generierung von Eigenschaftspr\u00fcfern in einem Hardware\/Software-Co-Verifikationsverfahren. Bachelor thesis, Paderborn University (2014)"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"issue":"6","key":"1_CR33","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1145\/1993316.1993518","volume":"46","author":"Adrian Sampson","year":"2011","unstructured":"Sampson, A., Dietl, W., Fortuna, E., Gnanapragasam, D., Ceze, L., Grossman, D.: EnerJ: approximate data types for safe and general low-power computation. In: Proceedings of the PLDI, pp. 164\u2013174. ACM (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-34188-5_15","volume-title":"Hardware and Software: Verification and Testing","author":"O Sery","year":"2012","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 160\u2013175. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-34188-5_15"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Shafique, M., Ahmad, W., Hafiz, R., Henkel, J.: A low latency generic accuracy configurable adder. In: Proceedings of the DAC, pp. 86:1\u201386:6. ACM (2015)","DOI":"10.1145\/2744769.2744778"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Verma, A.K., Brisk, P., Ienne, P.: Variable latency speculative addition: a new paradigm for arithmetic circuit design. In: Proceedings of the DATE, pp. 1250\u20131255. ACM (2008)","DOI":"10.1109\/DATE.2008.4484850"},{"key":"1_CR37","unstructured":"Wolf, C.: Yosys open synthesis suite. \n                      http:\/\/www.clifford.at\/yosys\/"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Ye, R., Wang, T., Yuan, F., Kumar, R., Xu, Q.: On reconfiguration-oriented approximate adder design and its application. In: Proceedings of the CAD, pp. 48\u201354. IEEE Press (2013)","DOI":"10.1109\/ICCAD.2013.6691096"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Zhu, N., Goh, W.L., Yeo, K.S.: An enhanced low-power high-speed adder for error-tolerant application. In: Proceedings of the International Symposium on Integrated Circuits, pp. 69\u201372. IEEE (2009)","DOI":"10.1109\/SOCDC.2010.5682905"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31157-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:23:46Z","timestamp":1569180226000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31157-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030311568","9783030311575"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31157-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tap.sosy-lab.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}