{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:57Z","timestamp":1740123297809,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,7,18]],"date-time":"2017-07-18T00:00:00Z","timestamp":1500336000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,7,18]],"date-time":"2017-07-18T00:00:00Z","timestamp":1500336000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF 1255776"],"award-info":[{"award-number":["CCF 1255776"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["2013-TJ-2426"],"award-info":[{"award-number":["2013-TJ-2426"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1552975"],"award-info":[{"award-number":["1552975"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,1]]},"DOI":"10.1007\/s10817-017-9421-9","type":"journal-article","created":{"date-parts":[[2017,7,18]],"date-time":"2017-07-18T15:24:42Z","timestamp":1500391482000},"page":"23-42","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Verifying Relative Safety, Accuracy, and Termination for Program Approximations"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9899-6226","authenticated-orcid":false,"given":"Shaobo","family":"He","sequence":"first","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,18]]},"reference":[{"key":"9421_CR1","doi-asserted-by":"crossref","unstructured":"Baek, W., Chilimbi, T.M.: Green: a framework for supporting energy-conscious programming using controlled approximation. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 198\u2013209 (2010)","DOI":"10.1145\/1809028.1806620"},{"key":"9421_CR2","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: International Symposium on Formal Methods for Components and Objects (FMCO), pp. 364\u2013387 (2006)","DOI":"10.1007\/11804192_17"},{"key":"9421_CR3","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, chap. 26, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"9421_CR4","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 14\u201325 (2004)","DOI":"10.1145\/982962.964003"},{"key":"9421_CR5","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Mytkowicz, T., McKinley, K.S.: Uncertain<T>: a first-order type for uncertain data. In: ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 51\u201366 (2014)","DOI":"10.1145\/2541940.2541958"},{"key":"9421_CR6","doi-asserted-by":"crossref","unstructured":"Boston, B., Sampson, A., Grossman, D., Ceze, L.: Probability type inference for flexible approximate programming. In: ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 470\u2013487 (2015)","DOI":"10.1145\/2858965.2814301"},{"key":"9421_CR7","doi-asserted-by":"crossref","unstructured":"Carbin, M., Kim, D., Misailovic, S., Rinard, M.C.: Proving acceptability properties of relaxed nondeterministic approximate programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 169\u2013180 (2012)","DOI":"10.1145\/2345156.2254086"},{"key":"9421_CR8","doi-asserted-by":"crossref","unstructured":"Carbin, M., Misailovic, S., Rinard, M.C.: Verifying quantitative reliability for programs that execute on unreliable hardware. In: ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pp. 33\u201352 (2013)","DOI":"10.1145\/2544173.2509546"},{"key":"9421_CR9","doi-asserted-by":"crossref","unstructured":"Chakrapani, L.N., George, J., Marr, B., Akgul, B.E.S., Palem, K.V.: Probabilistic design: a survey of probabilistic CMOS technology and future directions for terascale IC design. In: International Conference on Very Large Scale Integration of System on Chip (VLSI-SoC), pp. 101\u2013118 (2006)","DOI":"10.1007\/978-0-387-74909-9_7"},{"key":"9421_CR10","unstructured":"The Coq proof assistant. \n                    http:\/\/coq.inria.fr"},{"issue":"2","key":"9421_CR11","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10703-015-0234-3","volume":"47","author":"D Elenbogen","year":"2015","unstructured":"Elenbogen, D., Katz, S., Strichman, O.: Proving mutual termination. Form. Methods Syst. Des. 47(2), 204\u2013229 (2015)","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"9421_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/2589750","volume":"58","author":"H Esmaeilzadeh","year":"2014","unstructured":"Esmaeilzadeh, H., Sampson, A., Ceze, L., Burger, D.: Neural acceleration for general-purpose approximate programs. Commun. ACM 58(1), 105\u2013115 (2014)","journal-title":"Commun. ACM"},{"key":"9421_CR13","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: ACM\/IEEE International Conference on Automated Software Engineering (ASE), pp. 349\u2013360 (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"9421_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Internationa Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity (FME), pp. 500\u2013517 (2001)","DOI":"10.1007\/3-540-45251-6_29"},{"key":"9421_CR15","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: Design Automation Conference (DAC), pp. 466\u2013471 (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"9421_CR16","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: International Conference on Computer Aided Verification (CAV), pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"issue":"1","key":"9421_CR17","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/TCAD.2012.2223467","volume":"32","author":"P Gupta","year":"2013","unstructured":"Gupta, P., Agarwal, Y., Dolecek, L., Dutt, N., Gupta, R.K., Kumar, R., Mitra, S., Nicolau, A., Rosing, T.S., Srivastava, M.B., Swanson, S., Sylvester, D.: Underdesigned and opportunistic computing in presence of hardware variability. IEEE Trans. CAD of Integr. Circuits Syst. 32(1), 8\u201323 (2013)","journal-title":"IEEE Trans. CAD of Integr. Circuits Syst."},{"key":"9421_CR18","doi-asserted-by":"crossref","unstructured":"Han, J., Orshansky, M.: Approximate computing: an emerging paradigm for energy-efficient design. In: IEEE European Test Symposium (ETS), pp. 1\u20136 (2013)","DOI":"10.1109\/ETS.2013.6569370"},{"key":"9421_CR19","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebelo, H.: Towards modularly comparing programs using automated theorem provers. In: International Conference on Automated Deduction (CADE), pp. 282\u2013299 (2013)","DOI":"10.1007\/978-3-642-38574-2_20"},{"key":"9421_CR20","doi-asserted-by":"crossref","unstructured":"Hoffmann, H., Sidiroglou, S., Carbin, M., Misailovic, S., Agarwal, A., Rinard, M.: Dynamic knobs for responsive power-aware computing. In: ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 199\u2013212 (2011)","DOI":"10.1145\/1961295.1950390"},{"issue":"5","key":"9421_CR21","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":"9421_CR22","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SymDiff: a language-agnostic semantic diff tool for imperative programs. In: International Conference on Computer Aided Verification (CAV), pp. 712\u2013717 (2012)","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"9421_CR23","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 345\u2013355 (2013)","DOI":"10.1145\/2491411.2491452"},{"key":"9421_CR24","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: International Conference on Computer Aided Verification (CAV), pp. 243\u2013259 (2014)","DOI":"10.1007\/978-3-319-08867-9_16"},{"issue":"10","key":"9421_CR25","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1145\/2714064.2660231","volume":"49","author":"S 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. SIGPLAN Not. 49(10), 309\u2013328 (2014)","journal-title":"SIGPLAN Not."},{"key":"9421_CR26","doi-asserted-by":"crossref","unstructured":"Misailovic, S., Sidiroglou, S., Hoffmann, H., Rinard, M.: Quality of service profiling. In: ACM\/IEEE International Conference on Software Engineering (ICSE), pp. 25\u201334 (2010)","DOI":"10.1145\/1806799.1806808"},{"key":"9421_CR27","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 83\u201394 (2000)","DOI":"10.1145\/358438.349314"},{"key":"9421_CR28","unstructured":"Nelson, J., Sampson, A., Ceze, L.: Dense approximate storage in phase-change memory. In: Ideas and Perspectives session at ASPLOS (2001)"},{"key":"9421_CR29","doi-asserted-by":"crossref","unstructured":"Park, J., Esmaeilzadeh, H., Zhang, X., Naik, M., Harris, W.: FlexJava: Language support for safe and modular approximate programming. In: ACM SIGSOFT Symp. on the Foundations of Software Engineering (FSE), pp. 745\u2013757 (2015)","DOI":"10.1145\/2786805.2786807"},{"key":"9421_CR30","unstructured":"Park, J., Ni, K., Zhang, X., Esmaeilzadeh, H., Naik, M.: Expectation-oriented framework for automating approximate programming. In: Workshop on Approximate Computing Across the System Stack (WACAS) (2014)"},{"key":"9421_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 151\u2013166 (1998)","DOI":"10.1007\/BFb0054170"},{"key":"9421_CR32","doi-asserted-by":"crossref","unstructured":"Rinard, M.: Acceptability-oriented computing. In: ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 221\u2013239 (2003)","DOI":"10.1145\/949344.949402"},{"key":"9421_CR33","unstructured":"Ringenburg, M.F., Sampson, A., Ackerman, I., Ceze, L., Grossman, D.: Dynamic analysis of approximate program quality. Technical Report UW-CSE-14-03-01, University of Washington (2014)"},{"key":"9421_CR34","unstructured":"Ringenburg, M.F., Sampson, A., Ceze, L., Grossman, D.: Profiling and autotuning for energy-aware approximate programming. In: Workshop on Approximate Computing Across the System Stack (WACAS) (2014)"},{"key":"9421_CR35","doi-asserted-by":"crossref","unstructured":"Roy, P., Ray, R., Wang, C., Wong, W.-F.: ASAC: Automatic sensitivity analysis for approximate computing. In: ACM SIGPLAN\/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems (LCTES), pp. 95\u2013104 (2014)","DOI":"10.1145\/2666357.2597812"},{"key":"9421_CR36","unstructured":"Sampson, A.: Hardware and Software for Approximate Computing. PhD thesis, University of Washington (2015)"},{"key":"9421_CR37","unstructured":"Sampson, A., Baixo, A., Ransford, B., Moreau, T., Yip, J., Ceze, L., Oskin, M.: ACCEPT: A programmer-guided compiler framework for practical approximate computing. Technical Report UW-CSE-15-01-01, University of Washington (2015)"},{"key":"9421_CR38","unstructured":"Sampson, A., Bornholt, J., Ceze, L.: Hardware-software co-design: not just a clich\u00e9. In: Summit on Advances in Programming Languages (SNAPL), pp. 262\u2013273 (2015)"},{"key":"9421_CR39","doi-asserted-by":"crossref","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: ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 164\u2013174 (2011)","DOI":"10.1145\/1993316.1993518"},{"key":"9421_CR40","doi-asserted-by":"crossref","unstructured":"Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K.S., Grossman, D., Ceze, L.: Expressing and verifying probabilistic assertions. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 112\u2013122 (2014)","DOI":"10.1145\/2666356.2594294"},{"key":"9421_CR41","doi-asserted-by":"crossref","unstructured":"Sharma, V.C., Haran, A., Rakamari\u0107, Z., Gopalakrishnan, G.: Towards formal approaches to system resilience. In: IEEE Pacific Rim International Symposium on Dependable Computing (PRDC), pp. 41\u201350 (2013)","DOI":"10.1109\/PRDC.2013.14"},{"key":"9421_CR42","doi-asserted-by":"crossref","unstructured":"Sidiroglou-Douskos, S., Misailovic, S., Hoffmann, H., Rinard, M.C.: Managing performance vs. accuracy trade-offs with loop perforation. In: Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 124\u2013134 (2011)","DOI":"10.1145\/2025113.2025133"},{"key":"9421_CR43","doi-asserted-by":"crossref","unstructured":"Sui, X., Lenharth, A., Fussell, D.S., Pingali, K.: Proactive control of approximate programs. In: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 607\u2013621 (2016)","DOI":"10.1145\/2954680.2872402"},{"key":"9421_CR44","unstructured":"Thomas, A., Pattabiraman, K.: LLFI: An intermediate code level fault injector for soft computing applications. In: Workshop on Silicon Errors in Logic System Effects (SELSE) (2013)"},{"key":"9421_CR45","doi-asserted-by":"crossref","unstructured":"Vanegue, J., Lahiri, S.K.: Towards practical reactive security audit using extended static checkers. In: IEEE Symposium on Security and Privacy, pp. 33\u201347 (2013)","DOI":"10.1109\/SP.2013.12"},{"key":"9421_CR46","doi-asserted-by":"crossref","unstructured":"Zhu, Z.A., Misailovic, S., Kelner, J.A., Rinard, M.: Randomized accuracy-aware program transformations for efficient approximate computations. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 441\u2013454 (2012)","DOI":"10.1145\/2103621.2103710"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9421-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9421-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9421-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T23:00:14Z","timestamp":1589410814000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9421-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,18]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["9421"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9421-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,7,18]]},"assertion":[{"value":"30 November 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 July 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}