{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:32Z","timestamp":1775873492024,"version":"3.50.1"},"reference-count":82,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1109\/ase.2017.8115670","type":"proceedings-article","created":{"date-parts":[[2017,11,23]],"date-time":"2017-11-23T22:03:57Z","timestamp":1511474637000},"page":"601-612","source":"Crossref","is-referenced-by-count":30,"title":["Floating-point symbolic execution: A case study in N-version programming"],"prefix":"10.1109","author":[{"given":"Daniel","family":"Liew","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Schemmel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafael","family":"Zahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Wehrle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref73","first-page":"532","article-title":"Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions","volume":"9109","author":"solovyev","year":"2015","journal-title":"FM 2015 Formal Methods — 20th International Symposium Oslo Norway June 24–26 2015 Proceedings ser Lecture Notes in Computer Science"},{"key":"ref72","year":"2006","journal-title":"SMT-COMP competition 2006"},{"key":"ref71","article-title":"Address-Sanitizer: A fast address sanity checker","author":"serebryany","year":"2012","journal-title":"Proc 2012 USENIX Annual Technical Conference (USENIX ATC'12)"},{"key":"ref70","article-title":"CUTE: A concolic unit testing engine for C","author":"sen","year":"2005","journal-title":"Proc of the joint meeting of the European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering (ESEC\/FSE'05)"},{"key":"ref76","year":"2017","journal-title":"Undefined behavior sanitizer"},{"key":"ref77","article-title":"Z3 issue 1035: Unexpected huge performance difference between solver using “default","year":"2017","journal-title":"tactic Z3_mk_solver() and Z3_mk_simple_solver()"},{"key":"ref74","first-page":"359","author":"souza","year":"2011","journal-title":"CORAL Solving Complex Constraints for Symbolic PathFinder"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48096-0_43"},{"key":"ref75","article-title":"Pex: white box test generation for. NET","author":"tillmann","year":"2008","journal-title":"Proc of the 2nd International Conference on Tests and Proofs (TAP'08)"},{"key":"ref38","year":"2017","journal-title":"Gnu scientific library"},{"key":"ref78","year":"2017","journal-title":"Z3 issue 1251 Overflow encountered when expanding vector"},{"key":"ref79","year":"0","journal-title":"Z3 issue 577 No theory of floating point bitvectors and arrays and mixed performance?"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref32","year":"2017","journal-title":"GCOV-a Test Coverage Program"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115662"},{"key":"ref30","year":"0","journal-title":"Imperial floating point correctness benchmark repository"},{"key":"ref37","author":"granlund","year":"2016","journal-title":"GMP Development Team GNU MP The GNU Multiple Precision Arithmetic Library"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45927-8_15"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_14"},{"key":"ref34","article-title":"Automated whitebox fuzz testing","author":"godefroid","year":"2008","journal-title":"Proc 15th Ann Network and Distributed System Security Symp (NDSS 08)"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.175"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-013-0122-2"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-014-0154-2"},{"key":"ref28","year":"0","journal-title":"Floating Point correctness infrastructure repository"},{"key":"ref64","author":"press","year":"2007","journal-title":"Numerical Recipes 3rd Edition The Art of Scientific Computing"},{"key":"ref27","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Proc of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)"},{"key":"ref65","first-page":"306","article-title":"Static Analysis-Based Validation of Floating-Point Computations","author":"putot","year":"2003","journal-title":"Numerical Software with Result Verification International Dagstuhl Seminar Dagstuhl Castle Germany"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2983966"},{"key":"ref29","year":"0","journal-title":"Aachen floating point correctness benchmark repository"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/2693208.2693242"},{"key":"ref68","first-page":"151","article-title":"An SMT-LIB Theory of Binary Floating-Point Arithmetic","author":"r\u00fcmmer","year":"2010","journal-title":"Workshop on Satisfiability Modulo Theories"},{"key":"ref69","author":"schemmel","year":"0","journal-title":"KLEE Floating Point Extensions Team Aachen"},{"key":"ref2","year":"0","journal-title":"KLEE pull request 657 Implement basic support for vectorized instructions"},{"key":"ref1","year":"0","journal-title":"Competition On Software Verification - (SV-COMP)"},{"key":"ref20","article-title":"Symbolic Execution for Software Testing in Practice-Preliminary Assessment","author":"cadar","year":"2011","journal-title":"Proc of the 33rd International Conference on Software Engineering Impact Track (ICSE Impact'11)"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2593735.2593737"},{"key":"ref21","article-title":"N-version programming: A fault-tolerance approach to reliability of software operation","author":"chen","year":"1978","journal-title":"Proc of the 8th IEEE International Symposium on Fault Tolerant Computing (FTCS'78)"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966475"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47443-4_13"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"ref25","article-title":"Symbolic testing of OpenCL code","year":"2011","journal-title":"Proc Haifa Verification Conference (HVC)"},{"key":"ref50","first-page":"1","article-title":"Make it real: Effective floating-point reasoning via exact arithmetic","author":"leeser","year":"2014","journal-title":"2014 Design Automation and Test in Europe Conference and Exhibition"},{"key":"ref51","author":"liew","year":"0","journal-title":"KLEE Floating Point Extensions Team Imperial"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/1353445.1353446"},{"key":"ref58","article-title":"Docker: Lightweight Linux Containers for Consistent Development and Deployment","volume":"2014","author":"merkel","year":"2014","journal-title":"Linux J"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_16"},{"key":"ref56","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"mckeeman","year":"1998","journal-title":"Digital Technical Journal"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"ref54","year":"0","journal-title":"LLVM Bug 31294 llvm APFloat when using x87DoubleExtended semantics does not handle unsupported operands properly"},{"key":"ref53","year":"0","journal-title":"LLVM Bug 31292 llvm APFloat Assertion ‘lost_fraction==lfExact-lyZero’ failed"},{"key":"ref52","year":"0","journal-title":"LLVM Bug 30781 APFloat does not correctly handle signaling NaN"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.91"},{"key":"ref40","first-page":"131","article-title":"Deciding floating-point logic with systematic abstraction","author":"haller","year":"2012","journal-title":"Formal Methods in Computer-Aided Design FMCAD 2012 Cambridge UK"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.333"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_22"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0203-7"},{"key":"ref15","article-title":"An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic","author":"brain","year":"2015","journal-title":"Tech Rep"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9393-1"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"ref81","first-page":"344","article-title":"Approximations for Model Construction","author":"zeljic","year":"2014","journal-title":"Automated Reasoning — 7th International Joint Conference IJCAR 2014 Held as Part of the Vienna Summer of Logic VSL 2014"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"ref18","article-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs","author":"cadar","year":"2008","journal-title":"8th USENIX Symposium on Operating System Design and Implementation (OSDI '08)"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"ref80","year":"0","journal-title":"Z3 issue 740 Invalid model generated without warning"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2003.1252469"},{"key":"ref3","year":"0","journal-title":"[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.17"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231893"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429133"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429133"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16573-3_11"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2007.20"},{"key":"ref46","author":"kahan","year":"1987","journal-title":"Paranoia"},{"key":"ref45","article-title":"Information technology - Programming languages - C","year":"2011","journal-title":"International Organization for Standardization Geneva Switzerland"},{"key":"ref48","first-page":"160","author":"kroening","year":"2008","journal-title":"Decision Procedures An Algorithmic Point of View"},{"key":"ref47","first-page":"223","article-title":"Paranoia-a floating-point benchmark","volume":"10","author":"karpinski","year":"1985","journal-title":"Byte"},{"key":"ref42","article-title":"Intel, Intel(R) 64 and IA-32 Architectures Software Devloper's Manual","volume":"1","year":"2016","journal-title":"8 2 2 Unsupported Double Extended-Precision Floating-Point Encodings and Pseudo-Denormals"},{"key":"ref41","article-title":"IEEE Standard for Floating-Point Arithmetic","year":"2008","journal-title":"Institute of Electrical and Electronics Engineers Standard"},{"key":"ref44","article-title":"Programming languages - C","year":"1999","journal-title":"International Organization for Standardization Geneva Switzerland"},{"key":"ref43","article-title":"Information technology - Microprocessor Systems - Floating-Point arithmetic","year":"2011","journal-title":"International Organization for Standardization Geneva Switzerland"}],"event":{"name":"2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)","location":"Urbana, IL","start":{"date-parts":[[2017,10,30]]},"end":{"date-parts":[[2017,11,3]]}},"container-title":["2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8106906\/8115603\/08115670.pdf?arnumber=8115670","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T22:47:14Z","timestamp":1515451634000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8115670\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":82,"URL":"https:\/\/doi.org\/10.1109\/ase.2017.8115670","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}