{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:11:14Z","timestamp":1750306274010,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,12,19]],"date-time":"2017-12-19T00:00:00Z","timestamp":1513641600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2018,3,31]]},"abstract":"<jats:p>Modern systems are increasingly susceptible to soft errors that manifest themselves as bit flips and possibly alter the semantics of an application. We would like to measure the quality degradation on semantics due to such bit flips, and thus we introduce a Hyperball abstract domain that allows us to determine the worst-case distance between expected and actual results. Similar to intervals, hyperballs describe a connected and dense space. The semantics of low-level code in the presence of bit flips is hard to accurately describe in such a space. We therefore combine the Hyperball domain with an existing affine system abstract domain that we extend to handle bit flips, which are introduce as disjunctions. Bit-flips can reduce the precision of our analysis, and we therefor introduce the Scale domain as a disjunctive refinement to minimize precision loss. This domain bounds the number of disjunctive elements by quantifying the over-approximation of different partitions and uses submodular optimization to find a good partitioning (within a bound of optimal). We evaluate these domains to show benefits and potential problems. For the application we examine here, adding the Scale domain to the Hyperball abstraction improves accuracy by up to two orders of magnitude. Our initial results demonstrate the feasibility of this approach, although we would like to further improve execution efficiency.<\/jats:p>","DOI":"10.1145\/3156017","type":"journal-article","created":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T14:54:00Z","timestamp":1513781640000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Reliability Properties Using the Hyperball Abstract Domain"],"prefix":"10.1145","volume":"40","author":[{"given":"Jacob","family":"Lidman","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]},{"given":"Sally A.","family":"Mckee","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2017,12,19]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882103"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(97)00009-9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2005.862424"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.09.003"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001450010016"},{"volume-title":"Static Analysis Symposium. Springer-Verlag, 312--327","author":"Claris R.","key":"e_1_2_1_6_1","unstructured":"R. Claris and J. Cortadella. 2004. The octahedron abstract domain. In Static Analysis Symposium. Springer-Verlag, 312--327."},{"key":"e_1_2_1_7_1","volume-title":"Formal Methods and Software Engineering. Lecture Notes in Computer Science","volume":"8144","author":"Costantini G.","unstructured":"G. Costantini, P. Ferrara, G. Maggiore, and A. Cortesi. 2013. The domain of parametric hypercubes for static analysis of computer games software. In Formal Methods and Software Engineering. Lecture Notes in Computer Science, Vol. 8144. Springer, Berlin, 447--463."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1880443.1880448"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651361"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1496770.1496829"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2751504.2751512"},{"key":"e_1_2_1_15_1","unstructured":"Sylvain Guilley Houssem Maghrebi Youssef Souissi Laurent Sauvage and J. Danger. 2011. Quantifying the quality of side-channel acquisition. COSADE (Feb. 2011) 16--28."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882112"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_26"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646764.703989"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1756006.1756044"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.47"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14325-5_45"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_25"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDMR.2005.855685"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660231"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185651"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_2"},{"volume-title":"Circuits and Systems Conference (DCAS\u201915)","author":"Saraf N.","key":"e_1_2_1_30_1","unstructured":"N. Saraf and K. Bazargan. 2015. Improving linear feedback shift registers using similarity transformations. In Circuits and Systems Conference (DCAS\u201915). 1--4."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535853"},{"key":"e_1_2_1_32_1","volume-title":"Technical Report TR-1789. Computer Sciences Department","author":"Sharma T.","year":"2013","unstructured":"T. Sharma, A. Thakur, and T. Reps. 2013. An Abstract Domain for Bit-vector Inequalities. Technical Report TR-1789. Computer Sciences Department, University of Wisconsin\u2014Madison, WI."},{"key":"e_1_2_1_33_1","unstructured":"P. Sotin. 2010. Quantifying the Precision of Numerical Abstract Domains. Research Report Inria-00457324. Inria."},{"volume-title":"CGAL User and Reference Manual (4.5.2 ed.)","author":"Project The CGAL","key":"e_1_2_1_34_1","unstructured":"The CGAL Project. 2015. CGAL User and Reference Manual (4.5.2 ed.). CGAL Editorial Board. Retrieved from http:\/\/doc.cgal.org\/4.5.2\/Manual\/packages.html."},{"volume-title":"Proceedings of the 2015 6th Asia Symposium on Quality Electronic Design (ASQED\u201915)","author":"Wang Z.","key":"e_1_2_1_35_1","unstructured":"Z. Wang, H. Xie, S. Chafekar, and A. Chattopadhyay. 2015. Architectural error prediction using probabilistic error masking matrices. In Proceedings of the 2015 6th Asia Symposium on Quality Electronic Design (ASQED\u201915). 31--36."},{"volume-title":"CRC Concise Encyclopedia of Mathematics","author":"Weisstein E. W.","key":"e_1_2_1_36_1","unstructured":"E. W. Weisstein. 2002. CRC Concise Encyclopedia of Mathematics. Chapman 8 Hall\/CRC."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-004-0510-2"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3156017","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3156017","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3156017"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,19]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,3,31]]}},"alternative-id":["10.1145\/3156017"],"URL":"https:\/\/doi.org\/10.1145\/3156017","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2017,12,19]]},"assertion":[{"value":"2016-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}