{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,18]],"date-time":"2024-01-18T07:41:53Z","timestamp":1705563713802},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,12,20]],"date-time":"2013-12-20T00:00:00Z","timestamp":1387497600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1007\/s10703-013-0203-7","type":"journal-article","created":{"date-parts":[[2013,12,19]],"date-time":"2013-12-19T11:25:38Z","timestamp":1387452338000},"page":"213-245","source":"Crossref","is-referenced-by-count":39,"title":["Deciding floating-point logic with abstract conflict driven clause learning"],"prefix":"10.1007","volume":"45","author":[{"given":"Martin","family":"Brain","sequence":"first","affiliation":[]},{"given":"Vijay","family":"D\u2019Silva","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[]},{"given":"Leopold","family":"Haller","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,20]]},"reference":[{"issue":"4","key":"203_CR1","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1093\/comjnl\/bxp023","volume":"53","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour B, Abdel-Hamid A, Tahar S, Harrison J (2010) Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. Comput J 53(4):465\u2013488","journal-title":"Comput J"},{"key":"203_CR2","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-642-14203-1_11","volume-title":"Proc of international joint conference on automated reasoning","author":"A Ayad","year":"2010","unstructured":"Ayad A, March\u00e9 C (2010) Multi-prover verification of floating-point programs. In: Proc of international joint conference on automated reasoning. Springer, Berlin, pp 127\u2013141"},{"issue":"8","key":"203_CR3","doi-asserted-by":"crossref","first-page":"1188","DOI":"10.1016\/j.ic.2007.03.003","volume":"205","author":"B Badban","year":"2007","unstructured":"Badban B, van\u00a0de Pol J, Tveretina O, Zantema H (2007) Generalizing DPLL and satisfiability for equalities. Inf Comput 205(8):1188\u20131211","journal-title":"Inf Comput"},{"key":"203_CR4","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Proc of logic programming, artificial intelligence and reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C (2006) Splitting on demand in SAT modulo theories. In: Proc of logic programming, artificial intelligence and reasoning, pp 512\u2013526"},{"key":"203_CR5","first-page":"825","volume-title":"Handbook of satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett C, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability modulo theories. In: Handbook of satisfiability. IOS Press, Amsterdam, pp 825\u2013885"},{"key":"203_CR6","first-page":"196","volume-title":"Proc of programming language design and implementation","author":"B Blanchet","year":"2003","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proc of programming language design and implementation. ACM, New York, pp 196\u2013207"},{"key":"203_CR7","first-page":"187","volume-title":"Proc of computer arithmetic","author":"S Boldo","year":"2007","unstructured":"Boldo S, Filli\u00e2tre J (2007) Formal verification of floating-point programs. In: Proc of computer arithmetic. IEEE, New York, pp 187\u2013194"},{"issue":"2","key":"203_CR8","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B Botella","year":"2006","unstructured":"Botella B, Gotlieb A, Michel C (2006) Symbolic execution of floating-point computations. Softw Test Verif Reliab 16(2):97\u2013121","journal-title":"Softw Test Verif Reliab"},{"key":"203_CR9","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/978-3-642-35873-9_27","volume-title":"Proc of verification, model checking and abstract interpretation","author":"M Brain","year":"2013","unstructured":"Brain M, D\u2019Silva V, Haller L, Griggio A, Kroening D (2013) An abstract interpretation of DPLL(T). In: Proc of verification, model checking and abstract interpretation. Springer, Berlin, pp\u00a0455\u2013475"},{"key":"203_CR10","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1007\/978-3-642-38856-9_22","volume-title":"Proc of static analysis symposium","author":"M Brain","year":"2013","unstructured":"Brain M, D\u2019Silva V, Haller L, Griggio A, Kroening D (2013) Interpolation-based verification of floating-point programs with abstract CDCL. In: Proc of static analysis symposium. Springer, Berlin, pp\u00a0412\u2013432"},{"key":"203_CR11","first-page":"69","volume-title":"Proc of formal methods in computer-aided design","author":"A Brillout","year":"2009","unstructured":"Brillout A, Kroening D, Wahl T (2009) Mixed abstractions for floating-point arithmetic. In: Proc of formal methods in computer-aided design. IEEE, New York, pp 69\u201376"},{"key":"203_CR12","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-642-15769-1_12","volume-title":"Proc of static analysis symposium","author":"A Chapoutot","year":"2010","unstructured":"Chapoutot A (2010) Interval slopes as a numerical abstract domain for floating-point variables. In: Proc of static analysis symposium. Springer, Berlin, pp 184\u2013200"},{"key":"203_CR13","first-page":"3","volume-title":"Proc of Asian symposium on programming languages","author":"L Chen","year":"2008","unstructured":"Chen L, Min\u00e9 A, Cousot P (2008) A sound floating-point polyhedra abstract domain. In: Proc of Asian symposium on programming languages. Springer, Berlin, pp 3\u201318"},{"key":"203_CR14","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/978-3-642-03237-0_21","volume-title":"Proc of static analysis symposium","author":"L Chen","year":"2009","unstructured":"Chen L, Min\u00e9 A, Wang J, Cousot P (2009) Interval polyhedra: an abstract domain to infer interval linear relationships. In: Proc of static analysis symposium. Springer, Berlin, pp 309\u2013325"},{"key":"203_CR15","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/978-3-642-11319-2_11","volume-title":"Proc of verification, model checking and abstract interpretation","author":"L Chen","year":"2010","unstructured":"Chen L, Min\u00e9 A, Wang J, Cousot P (2010) An abstract domain to discover interval linear equalities. In: Proc of verification, model checking and abstract interpretation. Springer, Berlin, pp 112\u2013128"},{"key":"203_CR16","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Proc of tools and algorithms for the construction and analysis of systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT solver. In: Proc of tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp\u00a093\u2013107"},{"key":"203_CR17","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Proc of tools and algorithms for the construction and analysis of systems","author":"E Clarke","year":"2004","unstructured":"Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Proc of tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 168\u2013176"},{"key":"203_CR18","volume-title":"SMT workshop","author":"S Conchon","year":"2012","unstructured":"Conchon S, Melquiond G, Roux C, Iguernelala M (2012) Built-in treatment of an axiomatic floating-point theory for SMT solvers. In: SMT workshop"},{"key":"203_CR19","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-3-642-15297-9_8","volume-title":"Proc of formal modeling and analysis of timed systems","author":"S Cotton","year":"2010","unstructured":"Cotton S (2010) Natural domain SMT: a preliminary assessment. In: Proc of formal modeling and analysis of timed systems. Springer, Berlin, pp 77\u201391"},{"key":"203_CR20","first-page":"238","volume-title":"Proc of principles of programming languages","author":"P Cousot","year":"1977","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc of principles of programming languages. ACM Press, New York, pp 238\u2013252"},{"key":"203_CR21","first-page":"269","volume-title":"Proc of principles of programming languages","author":"P Cousot","year":"1979","unstructured":"Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: Proc of principles of programming languages. ACM Press, New York, pp 269\u2013282"},{"key":"203_CR22","first-page":"456","volume-title":"Proc of foundations of software science and computation structures","author":"P Cousot","year":"2011","unstructured":"Cousot P, Cousot R, Mauborgne L (2011) The reduced product of abstract domains and the combination of decision procedures. In: Proc of foundations of software science and computation structures. Springer, Berlin, pp 456\u2013472"},{"key":"203_CR23","first-page":"1132","volume-title":"IEEE standard for floating-point arithmetic","year":"2008","unstructured":"Cowlishaw M (ed) (2008) IEEE standard for floating-point arithmetic. IEEE, New York, pp\u00a01132\u20131138"},{"key":"203_CR24","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","volume-title":"Proc of theorem proving in higher order logics","author":"M Daumas","year":"2001","unstructured":"Daumas M, Rideau L, Th\u00e9ry L (2001) A generic library for floating-point numbers and its application to exact computing. In: Proc of theorem proving in higher order logics. Springer, Berlin, pp 169\u2013184"},{"key":"203_CR25","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. Commun ACM 5:394\u2013397","journal-title":"Commun ACM"},{"key":"203_CR26","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Proc of tools and algorithms for the construction and analysis of systems","author":"L Moura de","year":"2008","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Proc of tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 337\u2013340"},{"key":"203_CR27","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-642-04570-7_6","volume-title":"Proc of formal methods for industrial critical systems","author":"D Delmas","year":"2009","unstructured":"Delmas D, Goubault E, Putot S, Souyris J, Tekkal K, V\u00e9drine F (2009) Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Proc of formal methods for industrial critical systems. Springer, Berlin, pp 53\u201369"},{"key":"203_CR28","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-3-642-33125-1_22","volume-title":"Proc of static analysis symposium","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva V, Haller L, Kroening D (2012) Satisfiability solvers are static analyzers. In: Proc of static analysis symposium. Springer, Berlin, pp 317\u2013333"},{"key":"203_CR29","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Proc of tools and algorithms for the construction and analysis of systems","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva V, Haller L, Kroening D, Tautschnig M (2012) Numeric bounds analysis with conflict-driven learning. In: Proc of tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 48\u201363"},{"key":"203_CR30","first-page":"143","volume-title":"Proc of principles of programming languages","author":"V D\u2019Silva","year":"2013","unstructured":"D\u2019Silva V, Haller L, Kroening D (2013) Abstract conflict driven learning. In: Proc of principles of programming languages. ACM Press, New York, pp 143\u2013154"},{"key":"203_CR31","doi-asserted-by":"crossref","unstructured":"D\u2019Silva V, Haller L, Kroening D (2014) Abstract satisfaction. In: Proc of principles of programming languages (to appear). ACM, New York","DOI":"10.1145\/2535838.2535868"},{"key":"203_CR32","first-page":"33","volume-title":"Proc of European symposium on programming","author":"J Feret","year":"2004","unstructured":"Feret J (2004) Static analysis of digital filters. In: Proc of European symposium on programming. Springer, Berlin, pp 33\u201348"},{"issue":"3\u20134","key":"203_CR33","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J Satisf Boolean Model Comput 1(3\u20134):209\u2013236","journal-title":"J Satisf Boolean Model Comput"},{"key":"203_CR34","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Proc of computer aided verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger H, Hagen G, Nieuwenhuis R, Oliveras A, Tinelli C (2004) DPLL(T): fast decision procedures. In: Proc of computer aided verification. Springer, Berlin, pp 175\u2013188"},{"key":"203_CR35","doi-asserted-by":"crossref","first-page":"627","DOI":"10.1007\/978-3-642-02658-4_47","volume-title":"Proc of computer aided verification","author":"K Ghorbal","year":"2009","unstructured":"Ghorbal K, Goubault E, Putot S (2009) The zonotope abstract domain Taylor1+. In: Proc of computer aided verification. Springer, Berlin, pp 627\u2013633"},{"key":"203_CR36","first-page":"1","volume-title":"Proc of formal methods in computer-aided design","author":"D Goldwasser","year":"2008","unstructured":"Goldwasser D, Strichman O, Fine S (2008) A theory-based decision heuristic for DPLL(T). In: Proc of formal methods in computer-aided design. IEEE Press, New York, pp 1\u20138"},{"key":"203_CR37","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/3-540-47764-0_14","volume-title":"Proc of static analysis symposium","author":"E Goubault","year":"2001","unstructured":"Goubault E (2001) Static analyses of the precision of floating-point operations. In: Proc of static analysis symposium. Springer, Berlin, pp 234\u2013259"},{"key":"203_CR38","first-page":"3","volume-title":"Proc of formal methods for industrial critical systems","author":"E Goubault","year":"2007","unstructured":"Goubault E, Putot S, Baufreton P, Gassino J (2007) Static analysis of the accuracy in control systems: principles and experiments. In: Proc of formal methods for industrial critical systems. Springer, Berlin, pp 3\u201320"},{"key":"203_CR39","first-page":"71","volume-title":"Proc of principles of programming languages","author":"WR Harris","year":"2010","unstructured":"Harris WR, Sankaranarayanan S, Ivan\u010di\u0107 F, Gupta A (2010) Program analysis via satisfiability modulo path programs. In: Proc of principles of programming languages, pp 71\u201382"},{"key":"203_CR40","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Proc of theorem proving in higher order logics","author":"J Harrison","year":"1999","unstructured":"Harrison J (1999) A machine-checked theory of floating point arithmetic. In: Proc of theorem proving in higher order logics. Springer, Berlin, pp 113\u2013130"},{"issue":"3","key":"203_CR41","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1023\/A:1008712907154","volume":"16","author":"J Harrison","year":"2000","unstructured":"Harrison J (2000) Floating point verification in HOL light: the exponential function. Form Methods Syst Des 16(3):271\u2013305","journal-title":"Form Methods Syst Des"},{"key":"203_CR42","first-page":"217","volume-title":"Proc of formal methods in computer-aided design","author":"J Harrison","year":"2000","unstructured":"Harrison J (2000) Formal verification of floating point trigonometric functions. In: Proc of formal methods in computer-aided design. Springer, Berlin, pp 217\u2013233"},{"issue":"2","key":"203_CR43","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1023\/A:1022973506233","volume":"22","author":"J Harrison","year":"2003","unstructured":"Harrison J (2003) Formal verification of square root algorithms. Form Methods Syst Des 22(2):143\u2013153","journal-title":"Form Methods Syst Des"},{"issue":"5","key":"203_CR44","first-page":"629","volume":"13","author":"J Harrison","year":"2007","unstructured":"Harrison J (2007) Floating-point verification. J Univers Comput Sci 13(5):629\u2013638","journal-title":"J Univers Comput Sci"},{"key":"203_CR45","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"Proc of nasa formal methods","author":"EV Jan Peleska","year":"2011","unstructured":"Jan Peleska EV, Lapschies F (2011) Automated test case generation with SMT-solving and abstract interpretation. In: Proc of nasa formal methods. Springer, Berlin, pp 298\u2013312"},{"key":"203_CR46","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Proc of computer aided verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet B, Min\u00e9 A (2009) Apron: a library of numerical abstract domains for static analysis. In: Proc of computer aided verification. Springer, Berlin, pp 661\u2013667"},{"key":"203_CR47","first-page":"338","volume-title":"Proc of conference on automated deduction","author":"D Jovanovic","year":"2011","unstructured":"Jovanovic D, de Moura L (2011) Cutting to the chase: solving linear integer arithmetic. In: Proc of conference on automated deduction. Springer, Berlin, pp 338\u2013353"},{"key":"203_CR48","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Proc of international joint conference on automated reasoning","author":"D Jovanovic","year":"2012","unstructured":"Jovanovic D, de Moura L (2012) Solving non-linear arithmetic. In: Proc of international joint conference on automated reasoning. Springer, Berlin, pp 339\u2013354"},{"key":"203_CR49","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-44659-1_21","volume-title":"Proc of theorem proving in higher order logics","author":"R Kaivola","year":"2000","unstructured":"Kaivola R, Aagaard M (2000) Divider circuit verification with model checking and theorem proving. In: Proc of theorem proving in higher order logics. Springer, Berlin, pp 338\u2013355"},{"key":"203_CR50","volume-title":"Satisfiability modulo theories competition 2012 system description","author":"F Lapschies","year":"2012","unstructured":"Lapschies F, Peleska J, Gorbachuk E, Mangels T (2012) sonolar SMT-solver. In: Satisfiability modulo theories competition 2012 system description"},{"key":"203_CR51","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Proc of computer aided verification","author":"K McMillan","year":"2009","unstructured":"McMillan K, Kuehlmann A, Sagiv M (2009) Generalizing DPLL to richer logics. In: Proc of computer aided verification. Springer, Berlin, pp 462\u2013476"},{"key":"203_CR52","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Proc of computer aided verification","author":"KL McMillan","year":"2010","unstructured":"McMillan KL (2010) Lazy annotation for program testing and verification. In: Proc of computer aided verification. Springer, Berlin, pp 104\u2013118"},{"key":"203_CR53","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1016\/j.ic.2011.09.005","volume":"216","author":"G Melquiond","year":"2012","unstructured":"Melquiond G (2012) Floating-point arithmetic in the Coq system. Inf Comput 216:14\u201323","journal-title":"Inf Comput"},{"key":"203_CR54","volume-title":"Annals of mathematics and artificial intelligence","author":"C Michel","year":"2002","unstructured":"Michel C (2002) Exact projection functions for floating point number constraints. In: Annals of mathematics and artificial intelligence"},{"key":"203_CR55","first-page":"524","volume-title":"Seventh international conference on principles and practice of constraint programming","author":"C Michel","year":"2001","unstructured":"Michel C, Rueher M, Lebbah Y (2001) Solving constraints over floating-point numbers. In: Seventh international conference on principles and practice of constraint programming. Springer, Berlin, pp 524\u2013538"},{"key":"203_CR56","first-page":"3","volume-title":"Proc of European symposium on programming","author":"A Min\u00e9","year":"2004","unstructured":"Min\u00e9 A (2004) Relational abstract domains for the detection of floating-point run-time errors. In: Proc of European symposium on programming. Springer, Berlin, pp 3\u201317"},{"key":"203_CR57","unstructured":"Miner PS (1995) Defining the IEEE-854 floating-point standard in PVS. PVS. Technical Memorandum 110167, NASA, Langley Research"},{"key":"203_CR58","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/11513988_21","volume-title":"Proc of computer aided verification","author":"D Monniaux","year":"2005","unstructured":"Monniaux D (2005) Compositional analysis of floating-point linear numerical filters. In: Proc of computer aided verification. Springer, Berlin, pp 199\u2013212"},{"key":"203_CR59","doi-asserted-by":"crossref","unstructured":"Monniaux D (2008) The pitfalls of verifying floating-point computations. ACM Trans Program Lang Syst 30(3)","DOI":"10.1145\/1353445.1353446"},{"key":"203_CR60","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"JS Moore","year":"1996","unstructured":"Moore JS, Lynch T, Kaufmann M (1996) A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating-point division algorithm. Trans Comput 47:913\u2013916","journal-title":"Trans Comput"},{"key":"203_CR61","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of floating-point arithmetic","author":"JM Muller","year":"2010","unstructured":"Muller JM, Brisebarre N, de Dinechin F, Jeannerod CP, Lef\u00e8vre V, Melquiond G, Revol N, Stehl\u00e9 D, Torres S (2010) Handbook of floating-point arithmetic, 1st edn. Springer, Berlin","edition":"1"},{"issue":"5","key":"203_CR62","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X Rival","year":"2007","unstructured":"Rival X, Mauborgne L (2007) The trace partitioning abstract domain. ACM Trans Program Lang Syst 29(5):26","journal-title":"ACM Trans Program Lang Syst"},{"key":"203_CR63","volume-title":"SMT workshop","author":"P R\u00fcmmer","year":"2010","unstructured":"R\u00fcmmer P, Wahl T (2010) An SMT-LIB theory of binary floating-point arithmetic. In: SMT workshop"},{"key":"203_CR64","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D Russinoff","year":"1998","unstructured":"Russinoff D (1998) A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS J Comput Math 1:148\u2013200","journal-title":"LMS J Comput Math"},{"key":"203_CR65","first-page":"96","volume":"103","author":"KA Sakallah","year":"2011","unstructured":"Sakallah KA, Marques-Silva J (2011) Anatomy and empirical evaluation of modern SAT solvers. Bull Eur Assoc Theor Comput Sci 103:96\u2013121","journal-title":"Bull Eur Assoc Theor Comput Sci"},{"key":"203_CR66","first-page":"131","volume-title":"Handbook of satisfiability","author":"JPM Silva","year":"2009","unstructured":"Silva JPM, Lynce I, Malik S (2009) Conflict-driven clause learning SAT solvers. In: Handbook of satisfiability. IOS Press, Amsterdam, pp 131\u2013153"},{"issue":"5","key":"203_CR67","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva JPM, Sakallah KA (1999) GRASP: a search algorithm for propositional satisfiability. Trans Comput 48(5):506\u2013521","journal-title":"Trans Comput"},{"key":"203_CR68","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-642-33125-1_23","volume-title":"Proc of static analysis symposium","author":"A Thakur","year":"2012","unstructured":"Thakur A, Reps T (2012) A generalization of St\u00e5lmarck\u2019s method. In: Proc of static analysis symposium Springer, Berlin, pp\u00a0334\u2013351"},{"key":"203_CR69","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Proc of computer aided verification","author":"A Thakur","year":"2012","unstructured":"Thakur A, Reps T (2012) A method for symbolic computation of abstract operations. In: Proc of computer aided verification. Springer, Berlin, pp\u00a0174\u2013192"},{"key":"203_CR70","first-page":"279","volume-title":"International conference on computer-aided design","author":"L Zhang","year":"2001","unstructured":"Zhang L, Madigan CF, Moskewicz MW, Malik S (2001) Efficient conflict driven learning in a Boolean satisfiability solver. In: International conference on computer-aided design. ACM, New York, pp 279\u2013285"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0203-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0203-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0203-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,5]],"date-time":"2019-08-05T04:31:48Z","timestamp":1564979508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0203-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,20]]},"references-count":70,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["203"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0203-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,20]]}}}