{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:13:21Z","timestamp":1743099201377,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319406473"},{"type":"electronic","value":"9783319406480"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_19","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"237-254","source":"Crossref","is-referenced-by-count":6,"title":["Verifying Relative Safety, Accuracy, and Termination for Program Approximations"],"prefix":"10.1007","author":[{"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":[[2016,6,4]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"19_CR2","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability (2009)"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)","DOI":"10.1145\/964001.964003"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Boston, B., Sampson, A., Grossman, D., Ceze, L.: Probability type inference for flexible approximate programming. In: OOPSLA (2015)","DOI":"10.1145\/2814270.2814301"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Carbin, M., Kim, D., Misailovic, S., Rinard, M.C.: Proving acceptability properties of relaxed nondeterministic approximate programs. In: PLDI (2012)","DOI":"10.1145\/2254064.2254086"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Carbin, M., Misailovic, S., Rinard, M.C.: Verifying quantitative reliability for programs that execute on unreliable hardware. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509546"},{"key":"19_CR7","unstructured":"The Coq proof assistant. http:\/\/coq.inria.fr"},{"issue":"2","key":"19_CR8","first-page":"204","volume":"47","author":"D Elenbogen","year":"2015","unstructured":"Elenbogen, D., Katz, S., Strichman, O.: Proving mutual termination. FMSD 47(2), 204\u2013229 (2015)","journal-title":"FMSD"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: ASE (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 500. Springer, Heidelberg (2001)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: DAC (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/978-3-642-38574-2_20","volume-title":"Automated Deduction \u2013 CADE-24","author":"C Hawblitzel","year":"2013","unstructured":"Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Reb\u00ealo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 282\u2013299. Springer, Heidelberg (2013)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"He, S., Lahiri, S.K., Rakamari\u0107, Z.: Verifying relative safety, accuracy, and termination for program approximations. Tech. rep., Microsoft Research (2016)","DOI":"10.1007\/978-3-319-40648-0_19"},{"issue":"5","key":"19_CR15","doi-asserted-by":"crossref","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":"19_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Bryant, R.E.: Predicate abstraction with indexed predicates. ACM Trans. Comput. Log. 9(1) (2007)","DOI":"10.1145\/1297658.1297662"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2012","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712\u2013717. Springer, Heidelberg (2012)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: ESEC\/FSE (2013)","DOI":"10.1145\/2491411.2491452"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-319-08867-9_16","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2014","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 243\u2013259. Springer, Heidelberg (2014)"},{"key":"19_CR21","doi-asserted-by":"crossref","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, 309\u2013328 (2014)","journal-title":"SIGPLAN Not."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Misailovic, S., Sidiroglou, S., Hoffmann, H., Rinard, M.: Quality of service profiling. In: ICSE (2010)","DOI":"10.1145\/1806799.1806808"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI (2000)","DOI":"10.1145\/349299.349314"},{"key":"19_CR24","unstructured":"Nelson, J., Sampson, A., Ceze, L.: Dense approximate storage in phase-change memory. In: Ideas and Perspectives session at ASPLOS (2001)"},{"key":"19_CR25","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: ESEC\/FSE (2015)","DOI":"10.1145\/2786805.2786807"},{"key":"19_CR26","unstructured":"Park, J., Ni, K., Zhang, X., Esmaeilzadeh, H., Naik, M.: Expectation-oriented framework for automating approximate programming. In: WACAS (2014)"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M.D., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Rinard, M.: Acceptability-oriented computing. In: OOPSLA (2003)","DOI":"10.1145\/949344.949402"},{"key":"19_CR29","unstructured":"Ringenburg, M.F., Sampson, A., Ackerman, I., Ceze, L., Grossman, D.: Dynamic analysis of approximate program quality. Tech. Rep. UW-CSE-14-03-01, University of Washington"},{"key":"19_CR30","unstructured":"Ringenburg, M.F., Sampson, A., Ceze, L., Grossman, D.: Profiling and autotuning for energy-aware approximate programming. In: WACAS (2014)"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Roy, P., Ray, R., Wang, C., Wong, W.F.: ASAC: Automatic sensitivity analysis for approximate computing. In: LCTES (2014)","DOI":"10.1145\/2597809.2597812"},{"key":"19_CR32","unstructured":"Sampson, A.: Hardware and Software for Approximate Computing. Ph.D. thesis (2015)"},{"key":"19_CR33","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. Tech. Rep. UW-CSE-15-01-01, University of Washington"},{"key":"19_CR34","unstructured":"Sampson, A., Bornholt, J., Ceze, L.: Hardware-software co-design: not just a clich\u00e9. In: SNAPL (2015)"},{"key":"19_CR35","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: PLDI (2011)","DOI":"10.1145\/1993498.1993518"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Sharma, V.C., Haran, A., Rakamari\u0107, Z., Gopalakrishnan, G.: Towards formal approaches to system resilience. In: PRDC (2013)","DOI":"10.1109\/PRDC.2013.14"},{"key":"19_CR37","unstructured":"Thomas, A., Pattabiraman, K.: LLFI: an intermediate code level fault injector for soft computing applications. In: SELSE (2013)"},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"Vanegue, J., Lahiri, S.K.: Towards practical reactive security audit using extended static checkers. In: S&P (2013)","DOI":"10.1109\/SP.2013.12"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T03:10:49Z","timestamp":1567998649000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}