{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:24Z","timestamp":1750220844360,"version":"3.41.0"},"reference-count":83,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["Contract No. HR0011-18-C-0122"],"award-info":[{"award-number":["Contract No. HR0011-18-C-0122"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1629431, CCF-1703637, CCF-1846354,"],"award-info":[{"award-number":["CCF-1629431, CCF-1703637, CCF-1846354,"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>We present Parallely, a programming language and a system for verification of approximations in parallel message-passing programs. Parallely's language can express various software and hardware level approximations that reduce the computation and communication overheads at the cost of result accuracy.<\/jats:p>\n          <jats:p>Parallely's safety analysis can prove the absence of deadlocks in approximate computations and its type system can ensure that approximate values do not interfere with precise values. Parallely's quantitative accuracy analysis can reason about the frequency and magnitude of error. To support such analyses, Parallely presents an approximation-aware version of canonical sequentialization, a recently proposed verification technique that generates sequential programs that capture the semantics of well-structured parallel programs (i.e., ones that satisfy a symmetric nondeterminism property). To the best of our knowledge, Parallely is the first system designed to analyze parallel approximate programs.<\/jats:p>\n          <jats:p>We demonstrate the effectiveness of Parallely on eight benchmark applications from the domains of graph analytics, image processing, and numerical analysis. We also encode and study five approximation mechanisms from literature. Our implementation of Parallely automatically and efficiently proves type safety, reliability, and accuracy properties of the approximate benchmarks.<\/jats:p>","DOI":"10.1145\/3360545","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Verifying safety and accuracy of approximate parallel programs via canonical sequentialization"],"prefix":"10.1145","volume":"3","author":[{"given":"Vimuth","family":"Fernando","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Keyur","family":"Joshi","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Sasa","family":"Misailovic","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18","author":"Lipton R. J.","year":"1975","unstructured":"R. J. Lipton . 1975 . Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18 (1975). R. J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18 (1975)."},{"key":"e_1_2_2_2_1","volume-title":"Petri nets. ACM Computing Surveys (CSUR) 3","author":"Peterson J. L.","year":"1977","unstructured":"J. L. Peterson . 1977. Petri nets. ACM Computing Surveys (CSUR) 3 ( 1977 ). J. L. Peterson. 1977. Petri nets. ACM Computing Surveys (CSUR) 3 (1977)."},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"G. Agha and C. Hewitt. 1985. Concurrent Programming Using Actors: Exploiting Large-Scale Parallelism. Technical Report. Cambridge MA USA.  G. Agha and C. Hewitt. 1985. Concurrent Programming Using Actors: Exploiting Large-Scale Parallelism. Technical Report. Cambridge MA USA.","DOI":"10.1007\/3-540-16042-6_2"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"G. Agha. 1986. An Overview of Actor Languages. In OOPWORK.  G. Agha. 1986. An Overview of Actor Languages. In OOPWORK.","DOI":"10.1145\/323779.323743"},{"volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"Godefroid P.","key":"e_1_2_2_5_1","unstructured":"P. Godefroid . 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem . Springer-Verlag . P. Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag."},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"G. Smith and D. Volpano. 1998. Secure Information Flow in a Multi-threaded Imperative Language. In POPL.  G. Smith and D. Volpano. 1998. Secure Information Flow in a Multi-threaded Imperative Language. In POPL.","DOI":"10.1145\/268946.268975"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","unstructured":"F. Huch. 1999. Verification of Erlang programs using abstract interpretation and model checking.  F. Huch. 1999. Verification of Erlang programs using abstract interpretation and model checking.","DOI":"10.1145\/317636.317908"},{"volume-title":"Communicating and mobile systems: the pi calculus","author":"Milner R.","key":"e_1_2_2_8_1","unstructured":"R. Milner . 1999. Communicating and mobile systems: the pi calculus . Cambridge university press . R. Milner. 1999. Communicating and mobile systems: the pi calculus. Cambridge university press."},{"key":"e_1_2_2_9_1","unstructured":"L. Page S. Brin R. Motwani and T. Winograd. 1999. The PageRank citation ranking: Bringing order to the web. Technical Report.  L. Page S. Brin R. Motwani and T. Winograd. 1999. The PageRank citation ranking: Bringing order to the web. Technical Report."},{"key":"e_1_2_2_10_1","unstructured":"A. Gaffar O. Mencer W. Luk P. Cheung and N. Shirazi. 2002. Floating-point bitwidth analysis via automatic differentiation. In FPT.  A. Gaffar O. Mencer W. Luk P. Cheung and N. Shirazi. 2002. Floating-point bitwidth analysis via automatic differentiation. In FPT."},{"key":"e_1_2_2_11_1","unstructured":"J. Dean and S. Ghemawat. 2004. MapReduce: Simplified data processing on large clusters. OSDI (2004).  J. Dean and S. Ghemawat. 2004. MapReduce: Simplified data processing on large clusters. OSDI (2004)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"C. Flanagan and P. Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In POPL.  C. Flanagan and P. Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In POPL.","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"S. F. Siegel. 2005. Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. In VMCAI.  S. F. Siegel. 2005. Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. In VMCAI.","DOI":"10.1007\/978-3-540-30579-8_27"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"S. F. Siegel and G. S. Avrunin. 2005. Modeling Wildcard-free MPI Programs for Verification. In PPoPP.  S. F. Siegel and G. S. Avrunin. 2005. Modeling Wildcard-free MPI Programs for Verification. In PPoPP.","DOI":"10.1145\/1065944.1065957"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"M. Rinard. 2006. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. In ICS.  M. Rinard. 2006. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. In ICS.","DOI":"10.1145\/1183401.1183447"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"L.-\u00c5. Fredlund and H. Svensson. 2007. McErlang: a model checker for a distributed functional programming language. In ICFP.  L.-\u00c5. Fredlund and H. Svensson. 2007. McErlang: a model checker for a distributed functional programming language. In ICFP.","DOI":"10.1145\/1291151.1291171"},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"W. Osborne R. Cheung J. Coutinho W. Luk and O. Mencer. 2007. Automatic accuracy-guaranteed bit-width optimization for fixed and floating-point systems. In FPL.  W. Osborne R. Cheung J. Coutinho W. Luk and O. Mencer. 2007. Automatic accuracy-guaranteed bit-width optimization for fixed and floating-point systems. In FPL.","DOI":"10.1109\/FPL.2007.4380730"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"M. Rinard. 2007. Using Early Phase Termination to Eliminate Load Imbalances at Barrier Synchronization Points. In OOPSLA.  M. Rinard. 2007. Using Early Phase Termination to Eliminate Load Imbalances at Barrier Synchronization Points. In OOPSLA.","DOI":"10.1145\/1297027.1297055"},{"volume-title":"International Conference on Computer Aided Verification. 37\u201351","author":"Lal A.","key":"e_1_2_2_19_1","unstructured":"A. Lal and T. Reps . 2008. Reducing concurrent analysis under a context bound to sequential analysis . In International Conference on Computer Aided Verification. 37\u201351 . A. Lal and T. Reps. 2008. Reducing concurrent analysis under a context bound to sequential analysis. In International Conference on Computer Aided Verification. 37\u201351."},{"key":"e_1_2_2_20_1","unstructured":"S. Chakradhar A. Raghunathan and J. Meng. 2009. Best-Effort Parallel Execution Framework for Recognition and Mining Applications. In IPDPS.  S. Chakradhar A. Raghunathan and J. Meng. 2009. Best-Effort Parallel Execution Framework for Recognition and Mining Applications. In IPDPS."},{"volume-title":"International Conference on Computer Aided Verification. 477\u2013492","author":"La Torre S.","key":"e_1_2_2_21_1","unstructured":"S. La Torre , P. Madhusudan , and G. Parlato . 2009. Reducing context-bounded concurrent reachability to sequential reachability . In International Conference on Computer Aided Verification. 477\u2013492 . S. La Torre, P. Madhusudan, and G. Parlato. 2009. Reducing context-bounded concurrent reachability to sequential reachability. In International Conference on Computer Aided Verification. 477\u2013492."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806620"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"S. Misailovic S. Sidiroglou H. Hoffmann and M. Rinard. 2010. Quality of service profiling. In ICSE.  S. Misailovic S. Sidiroglou H. Hoffmann and M. Rinard. 2010. Quality of service profiling. In ICSE.","DOI":"10.1145\/1806799.1806808"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"J. Ansel Y. Wong C. Chan M. Olszewski A. Edelman and S. Amarasinghe. 2011. Language and compiler support for auto-tuning variable-accuracy algorithms. In CGO.  J. Ansel Y. Wong C. Chan M. Olszewski A. Edelman and S. Amarasinghe. 2011. Language and compiler support for auto-tuning variable-accuracy algorithms. In CGO.","DOI":"10.1109\/CGO.2011.5764677"},{"key":"e_1_2_2_25_1","unstructured":"C. Bienia. 2011. Benchmarking modern multiprocessors.  C. Bienia. 2011. Benchmarking modern multiprocessors."},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"S. Chaudhuri S. Gulwani R. Lublinerman and S. Navidpour. 2011. Proving Programs Robust. In ESEC\/FSE.  S. Chaudhuri S. Gulwani R. Lublinerman and S. Navidpour. 2011. Proving Programs Robust. In ESEC\/FSE.","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"H. Hoffmann S. Sidiroglou M. Carbin S. Misailovic A. Agarwal and M. Rinard. 2011. Dynamic Knobs for Responsive Power-Aware Computing. In ASPLOS.  H. Hoffmann S. Sidiroglou M. Carbin S. Misailovic A. Agarwal and M. Rinard. 2011. Dynamic Knobs for Responsive Power-Aware Computing. In ASPLOS.","DOI":"10.1145\/1950365.1950390"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"S. Liu K. Pattabiraman T. Moscibroda and B. G. Zorn. 2011. Flikker: saving DRAM refresh-power through critical data partitioning. (2011).  S. Liu K. Pattabiraman T. Moscibroda and B. G. Zorn. 2011. Flikker: saving DRAM refresh-power through critical data partitioning. (2011).","DOI":"10.1145\/1950365.1950391"},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"S. Misailovic D. Roy and M. Rinard. 2011. Probabilistically Accurate Program Transformations. In SAS.  S. Misailovic D. Roy and M. Rinard. 2011. Probabilistically Accurate Program Transformations. In SAS.","DOI":"10.1007\/978-3-642-23702-7_24"},{"key":"e_1_2_2_30_1","volume-title":"Hogwild: A lock-free approach to parallelizing stochastic gradient descent. In Advances in neural information processing systems.","author":"Recht B.","year":"2011","unstructured":"B. Recht , C. Re , S. Wright , and F. Niu . 2011 . Hogwild: A lock-free approach to parallelizing stochastic gradient descent. In Advances in neural information processing systems. B. Recht, C. Re, S. Wright, and F. Niu. 2011. Hogwild: A lock-free approach to parallelizing stochastic gradient descent. In Advances in neural information processing systems."},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"A. Sampson W. Dietl E. Fortuna D. Gnanapragasam L. Ceze and D. Grossman. 2011. EnerJ: Approximate data types for safe and general low-power computation. In PLDI.  A. Sampson W. Dietl E. Fortuna D. Gnanapragasam L. Ceze and D. Grossman. 2011. EnerJ: Approximate data types for safe and general low-power computation. In PLDI.","DOI":"10.1145\/1993498.1993518"},{"key":"e_1_2_2_32_1","unstructured":"S. Sidiroglou S. Misailovic H. Hoffmann and M. Rinard. 2011. Managing Performance vs. Accuracy Trade-offs With Loop Perforation. In FSE.  S. Sidiroglou S. Misailovic H. Hoffmann and M. Rinard. 2011. Managing Performance vs. Accuracy Trade-offs With Loop Perforation. In FSE."},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"S. F. Siegel and G. Gopalakrishnan. 2011. Formal Analysis of Message Passing. In VMCAI.  S. F. Siegel and G. Gopalakrishnan. 2011. Formal Analysis of Message Passing. In VMCAI.","DOI":"10.1007\/978-3-642-18275-4_2"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993555"},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"M. Carbin D. Kim S. Misailovic and M. Rinard. 2012. Proving Acceptability Properties of Relaxed Nondeterministic Approximate Programs. In PLDI.  M. Carbin D. Kim S. Misailovic and M. Rinard. 2012. Proving Acceptability Properties of Relaxed Nondeterministic Approximate Programs. In PLDI.","DOI":"10.1145\/2254064.2254086"},{"volume-title":"Relax Workshop.","author":"Renganarayana L.","key":"e_1_2_2_36_1","unstructured":"L. Renganarayana , V. Srinivasan , R. Nair , and D. Prener . 2012. Programming with relaxed synchronization . In Relax Workshop. L. Renganarayana, V. Srinivasan, R. Nair, and D. Prener. 2012. Programming with relaxed synchronization. In Relax Workshop."},{"key":"e_1_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Z. Zhu S. Misailovic J. Kelner and M. Rinard. 2012. Randomized Accuracy-Aware Program Transformations for Efficient Approximate Computations. In POPL.  Z. Zhu S. Misailovic J. Kelner and M. Rinard. 2012. Randomized Accuracy-Aware Program Transformations for Efficient Approximate Computations. In POPL.","DOI":"10.1145\/2103656.2103710"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"M. Carbin D. Kim S. Misailovic and M. Rinard. 2013a. Verified integrity properties for safe approximate program transformations. In PEPM.  M. Carbin D. Kim S. Misailovic and M. Rinard. 2013a. Verified integrity properties for safe approximate program transformations. In PEPM.","DOI":"10.1145\/2426890.2426901"},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","unstructured":"M. Carbin S. Misailovic and M. C. Rinard. 2013b. Verifying Quantitative Reliability for Programs That Execute on Unreliable Hardware. In OOPSLA.  M. Carbin S. Misailovic and M. C. Rinard. 2013b. Verifying Quantitative Reliability for Programs That Execute on Unreliable Hardware. In OOPSLA.","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_24"},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"S. Misailovic D. Kim and M. Rinard. 2013. Parallelizing Sequential Programs With Statistical Accuracy Tests. ACM TECS Special Issue on Probabilistic Embedded Computing (2013).  S. Misailovic D. Kim and M. Rinard. 2013. Parallelizing Sequential Programs With Statistical Accuracy Tests. ACM TECS Special Issue on Probabilistic Embedded Computing (2013).","DOI":"10.1145\/2465787.2465790"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503210.2503296"},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"P. Abdulla S. Aronis B. Jonsson and K. Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In POPL.  P. Abdulla S. Aronis B. Jonsson and K. Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In POPL.","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628071.2628092"},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"A. Desai P. Garg and P. Madhusudan. 2014. Natural Proofs for Asynchronous Programs Using Almost-synchronous Reductions. In OOPSLA.  A. Desai P. Garg and P. Madhusudan. 2014. Natural Proofs for Asynchronous Programs Using Almost-synchronous Reductions. In OOPSLA.","DOI":"10.1145\/2660193.2660211"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660231"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541948"},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"E. Schkufza R. Sharma and A. Aiken. 2014. Stochastic optimization of floating-point programs with tunable precision. In PLDI.  E. Schkufza R. Sharma and A. Aiken. 2014. Stochastic optimization of floating-point programs with tunable precision. In PLDI.","DOI":"10.1145\/2594291.2594302"},{"key":"e_1_2_2_49_1","unstructured":"S. Achour and M. Rinard. 2015. Energy Efficient Approximate Computation with Topaz. In OOPSLA.  S. Achour and M. Rinard. 2015. Energy Efficient Approximate Computation with Topaz. In OOPSLA."},{"key":"e_1_2_2_50_1","volume-title":"CRONO: A Benchmark Suite for Multithreaded Graph Algorithms Executing on Futuristic Multicores. In IISWC.","author":"Ahmad M.","year":"2015","unstructured":"M. Ahmad , F. Hijaz , Q. Shi , and O. Khan . 2015 . CRONO: A Benchmark Suite for Multithreaded Graph Algorithms Executing on Futuristic Multicores. In IISWC. M. Ahmad, F. Hijaz, Q. Shi, and O. Khan. 2015. CRONO: A Benchmark Suite for Multithreaded Graph Algorithms Executing on Futuristic Multicores. In IISWC."},{"volume-title":"International Conference on Fundamental Approaches to Software Engineering. 202\u2013217","author":"Blom S.","key":"e_1_2_2_51_1","unstructured":"S. Blom , S. Darabi , and M. Huisman . 2015. Verification of loop parallelisations . In International Conference on Fundamental Approaches to Software Engineering. 202\u2013217 . S. Blom, S. Darabi, and M. Huisman. 2015. Verification of loop parallelisations. In International Conference on Fundamental Approaches to Software Engineering. 202\u2013217."},{"key":"e_1_2_2_52_1","doi-asserted-by":"crossref","unstructured":"B. Boston A. Sampson D. Grossman and L. Ceze. 2015. Probability type inference for flexible approximate programming. (2015).  B. Boston A. Sampson D. Grossman and L. Ceze. 2015. Probability type inference for flexible approximate programming. (2015).","DOI":"10.1145\/2814270.2814301"},{"key":"e_1_2_2_53_1","doi-asserted-by":"crossref","unstructured":"S. Campanoni G. Holloway G.-Y. Wei and D. Brooks. 2015. HELIX-UP: Relaxing program semantics to unleash parallelization. In CGO.  S. Campanoni G. Holloway G.-Y. Wei and D. Brooks. 2015. HELIX-UP: Relaxing program semantics to unleash parallelization. In CGO.","DOI":"10.1109\/CGO.2015.7054203"},{"key":"e_1_2_2_54_1","doi-asserted-by":"crossref","unstructured":"Y. Ding J. Ansel K. Veeramachaneni X. Shen U. M. O\u2019Reilly and S. Amarasinghe. 2015. Autotuning Algorithmic Choice for Input Sensitivity. In PLDI.  Y. Ding J. Ansel K. Veeramachaneni X. Shen U. M. O\u2019Reilly and S. Amarasinghe. 2015. Autotuning Algorithmic Choice for Input Sensitivity. In PLDI.","DOI":"10.1145\/2737924.2737969"},{"key":"e_1_2_2_55_1","doi-asserted-by":"crossref","unstructured":"I. Goiri R. Bianchini S. Nagarakatte and T. Nguyen. 2015. ApproxHadoop: Bringing Approximations to MapReduce Frameworks. In ASPLOS.  I. Goiri R. Bianchini S. Nagarakatte and T. Nguyen. 2015. ApproxHadoop: Bringing Approximations to MapReduce Frameworks. In ASPLOS.","DOI":"10.1145\/2694344.2694351"},{"key":"e_1_2_2_56_1","volume-title":"ACCEPT: A Programmer-Guided Compiler Framework for Practical Approximate Computing. Technical Report.","author":"Sampson A.","year":"2015","unstructured":"A. Sampson , A. Baixo , B. Ransford , T. Moreau , J. Yip , L. Ceze , and M. Oskin . 2015 . ACCEPT: A Programmer-Guided Compiler Framework for Practical Approximate Computing. Technical Report. A. Sampson, A. Baixo, B. Ransford, T. Moreau, J. Yip, L. Ceze, and M. Oskin. 2015. ACCEPT: A Programmer-Guided Compiler Framework for Practical Approximate Computing. Technical Report."},{"key":"e_1_2_2_57_1","unstructured":"M. Abadi P. Barham J. Chen Z. Chen A. Davis J. Dean M. Devin S. Ghemawat G. Irving M. Isard M. Kudlur J. Levenberg R. Monga S. Moore D. G. Murray B. Steiner P. Tucker V. Vasudevan P. Warden M. Wicke Y. Yu and X. Zheng. 2016. TensorFlow: A System for Large-Scale Machine Learning. In OSDI.  M. Abadi P. Barham J. Chen Z. Chen A. Davis J. Dean M. Devin S. Ghemawat G. Irving M. Isard M. Kudlur J. Levenberg R. Monga S. Moore D. G. Murray B. Steiner P. Tucker V. Vasudevan P. Warden M. Wicke Y. Yu and X. Zheng. 2016. TensorFlow: A System for Large-Scale Machine Learning. In OSDI."},{"key":"e_1_2_2_58_1","volume-title":"Approximate Lock: Trading off Accuracy for Performance by Skipping Critical Sections. In ISSRE.","author":"Akram R.","year":"2016","unstructured":"R. Akram , M. M. U. Alam , and A. Muzahid . 2016 . Approximate Lock: Trading off Accuracy for Performance by Skipping Critical Sections. In ISSRE. R. Akram, M. M. U. Alam, and A. Muzahid. 2016. Approximate Lock: Trading off Accuracy for Performance by Skipping Critical Sections. In ISSRE."},{"key":"e_1_2_2_59_1","doi-asserted-by":"crossref","unstructured":"A. Bakst K. v. Gleissenthall R. G. Kici and R. Jhala. 2017. Verifying Distributed Programs via Canonical Sequentialization. In OOPSLA.  A. Bakst K. v. Gleissenthall R. G. Kici and R. Jhala. 2017. Verifying Distributed Programs via Canonical Sequentialization. In OOPSLA.","DOI":"10.1145\/3133934"},{"key":"e_1_2_2_60_1","doi-asserted-by":"crossref","unstructured":"R. Boyapati J. Huang P. Majumder K. H. Yum and E. J. Kim. 2017. APPROX-NoC: A Data Approximation Framework for Network-On-Chip Architectures. In ISCA.  R. Boyapati J. Huang P. Majumder K. H. Yum and E. J. Kim. 2017. APPROX-NoC: A Data Approximation Framework for Network-On-Chip Architectures. In ISCA.","DOI":"10.1145\/3079856.3080241"},{"key":"e_1_2_2_61_1","doi-asserted-by":"crossref","unstructured":"A. Canino and Y. D. Liu. 2017. Proactive and Adaptive Energy-aware Programming with Mixed Typechecking. In PLDI.  A. Canino and Y. D. Liu. 2017. Proactive and Adaptive Energy-aware Programming with Mixed Typechecking. In PLDI.","DOI":"10.1145\/3062341.3062356"},{"key":"e_1_2_2_62_1","doi-asserted-by":"crossref","unstructured":"W.-F. Chiang M. Baranowski I. Briggs A. Solovyev G. Gopalakrishnan and Z. Rakamari\u0107. 2017. Rigorous floating-point mixed-precision tuning. In POPL.  W.-F. Chiang M. Baranowski I. Briggs A. Solovyev G. Gopalakrishnan and Z. Rakamari\u0107. 2017. Rigorous floating-point mixed-precision tuning. In POPL.","DOI":"10.1145\/3009837.3009846"},{"key":"e_1_2_2_63_1","doi-asserted-by":"crossref","unstructured":"M. Huisman. 2017. A Verification Technique for Deterministic Parallel Programs. In PPDP.  M. Huisman. 2017. A Verification Technique for Deterministic Parallel Programs. In PPDP.","DOI":"10.1145\/3131851.3131852"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"e_1_2_2_65_1","doi-asserted-by":"crossref","unstructured":"S. Mitra M. K. Gupta S. Misailovic and S. Bagchi. 2017. Phase-aware optimization in approximate computing. In CGO.  S. Mitra M. K. Gupta S. Misailovic and S. Bagchi. 2017. Phase-aware optimization in approximate computing. In CGO.","DOI":"10.1109\/CGO.2017.7863739"},{"key":"e_1_2_2_66_1","doi-asserted-by":"crossref","unstructured":"B. Nongpoh R. Ray S. Dutta and A. Banerjee. 2017. AutoSense: A Framework for Automated Sensitivity Analysis of Program Data. IEEE Transactions on Software Engineering 43 (2017).  B. Nongpoh R. Ray S. Dutta and A. Banerjee. 2017. AutoSense: A Framework for Automated Sensitivity Analysis of Program Data. IEEE Transactions on Software Engineering 43 (2017).","DOI":"10.1109\/TSE.2017.2654251"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2016.2630270"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3145812"},{"key":"e_1_2_2_69_1","doi-asserted-by":"crossref","unstructured":"B. Boston Z. Gong and M. Carbin. 2018. Leto: verifying application-specific hardware fault tolerance with programmable execution models. In OOPSLA.  B. Boston Z. Gong and M. Carbin. 2018. Leto: verifying application-specific hardware fault tolerance with programmable execution models. In OOPSLA.","DOI":"10.1145\/3276533"},{"key":"e_1_2_2_70_1","doi-asserted-by":"crossref","unstructured":"E. Darulova A. Izycheva F. Nasir F. Ritter H. Becker and R. Bastian. 2018. Daisy-Framework for Analysis and Optimization of Numerical Programs (Tool Paper). In TACAS.  E. Darulova A. Izycheva F. Nasir F. Ritter H. Becker and R. Bastian. 2018. Daisy-Framework for Analysis and Optimization of Numerical Programs (Tool Paper). In TACAS.","DOI":"10.1007\/978-3-319-89960-2_15"},{"key":"e_1_2_2_71_1","doi-asserted-by":"crossref","unstructured":"E. A. Deiana V. St-Amour P. A. Dinda N. Hardavellas and S. Campanoni. 2018. Unconventional Parallelization of Nondeterministic Applications. In ASPLOS.  E. A. Deiana V. St-Amour P. A. Dinda N. Hardavellas and S. Campanoni. 2018. Unconventional Parallelization of Nondeterministic Applications. In ASPLOS.","DOI":"10.1145\/3173162.3173181"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9421-9"},{"key":"e_1_2_2_73_1","doi-asserted-by":"crossref","unstructured":"S. K. Khatamifard I. Akturk and U. R. Karpuzcu. 2018. On Approximate Speculative Lock Elision. IEEE Transactions on Multi-Scale Computing Systems 2 (2018).  S. K. Khatamifard I. Akturk and U. R. Karpuzcu. 2018. On Approximate Speculative Lock Elision. IEEE Transactions on Multi-Scale Computing Systems 2 (2018).","DOI":"10.1109\/TMSCS.2017.2773488"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156017"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2018.043191122"},{"key":"e_1_2_2_76_1","doi-asserted-by":"crossref","unstructured":"J. R. Stevens A. Ranjan and A. Raghunathan. 2018. AxBA: an approximate bus architecture framework. In ICCAD.  J. R. Stevens A. Ranjan and A. Raghunathan. 2018. AxBA: an approximate bus architecture framework. In ICCAD.","DOI":"10.1145\/3240765.3240782"},{"key":"e_1_2_2_77_1","unstructured":"R. Xu J. Koo R. Kumar P. Bai S. Mitra S. Misailovic and S. Bagchi. 2018. Videochef: efficient approximation for streaming video processing pipelines. In USENIX ATC.  R. Xu J. Koo R. Kumar P. Bai S. Mitra S. Misailovic and S. Bagchi. 2018. Videochef: efficient approximation for streaming video processing pipelines. In USENIX ATC."},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304033"},{"volume-title":"Identifying Optimal Parameters for Randomized Approximate Algorithms. In Workshop on Approximate Computing Across the Stack.","author":"Fernando V.","key":"e_1_2_2_79_1","unstructured":"V. Fernando , K. Joshi , D. Marinov , and S. Misailovic . 2019c . Identifying Optimal Parameters for Randomized Approximate Algorithms. In Workshop on Approximate Computing Across the Stack. V. Fernando, K. Joshi, D. Marinov, and S. Misailovic. 2019c. Identifying Optimal Parameters for Randomized Approximate Algorithms. In Workshop on Approximate Computing Across the Stack."},{"key":"e_1_2_2_80_1","unstructured":"V. Fernando K. Joshi and S. Misailovic. 2019b. Appendix to Parallely https:\/\/vimuth.github.io\/parallely\/appendix.pdf.  V. Fernando K. Joshi and S. Misailovic. 2019b. Appendix to Parallely https:\/\/vimuth.github.io\/parallely\/appendix.pdf."},{"key":"e_1_2_2_81_1","unstructured":"K. Gleissenthall R. G. Kici A. Bakst D. Stefan and R. Jhala. 2019. Pretend Synchrony. In POPL.  K. Gleissenthall R. G. Kici A. Bakst D. Stefan and R. Jhala. 2019. Pretend Synchrony. In POPL."},{"key":"e_1_2_2_82_1","doi-asserted-by":"crossref","unstructured":"K. Joshi V. Fernando and S. Misailovic. 2019. Statistical Algorithmic Profiling for Randomized Approximate Programs. In ICSE.  K. Joshi V. Fernando and S. Misailovic. 2019. Statistical Algorithmic Profiling for Randomized Approximate Programs. In ICSE.","DOI":"10.1109\/ICSE.2019.00071"},{"key":"e_1_2_2_83_1","doi-asserted-by":"crossref","unstructured":"E. Michael D. Woos T. Anderson M. D. Ernst and Z. Tatlock. 2019. Teaching Rigorous Distributed Systems With Efficient Model Checking. In EuroSys.  E. Michael D. Woos T. Anderson M. D. Ernst and Z. Tatlock. 2019. Teaching Rigorous Distributed Systems With Efficient Model Checking. In EuroSys.","DOI":"10.1145\/3302424.3303947"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360545","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360545","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360545","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360545"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":83,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360545"],"URL":"https:\/\/doi.org\/10.1145\/3360545","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}