×

Deciding floating-point logic with abstract conflict driven clause learning. (English) Zbl 1317.68110

Summary: We present a bit-precise decision procedure for the theory of floating-point arithmetic. The core of our approach is a non-trivial, lattice-theoretic generalisation of the conflict-driven clause learning algorithm in modern sat solvers to lattice-based abstractions. We use floating-point intervals to reason about the ranges of variables, which allows us to directly handle arithmetic and is more efficient than encoding a formula as a bit-vector as in current floating-point solvers. Interval reasoning alone is incomplete, and we obtain completeness by developing a conflict analysis algorithm that reasons natively about intervals. We have implemented this method in the mathsat5 smt solver and evaluated it on assertion checking problems that bound the values of program variables. Our new technique is faster than a bit-vector encoding approach on 80% of the benchmarks, and is faster by one order of magnitude or more on 60% of the benchmarks. The generalisation of cdcl we propose is widely applicable and can be used to derive abstraction-based smt solvers for other theories.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T05 Learning and adaptive systems in artificial intelligence
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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-488 · doi:10.1093/comjnl/bxp023
[2] Ayad, A.; Marché, C., Multi-prover verification of floating-point programs, 127-141 (2010), Berlin · Zbl 1291.68321 · doi:10.1007/978-3-642-14203-1_11
[3] Badban B, van de Pol J, Tveretina O, Zantema H (2007) Generalizing DPLL and satisfiability for equalities. Inf Comput 205(8):1188-1211 · Zbl 1121.68102 · doi:10.1016/j.ic.2007.03.003
[4] Barrett, C.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Splitting on demand in SAT modulo theories, 512-526 (2006) · Zbl 1165.68480 · doi:10.1007/11916277_35
[5] Barrett, C.; Sebastiani, R.; Seshia, SA; Tinelli, C., Satisfiability modulo theories, 825-885 (2009), Amsterdam
[6] Blanchet, B.; Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., A static analyzer for large safety-critical software, 196-207 (2003), New York
[7] Boldo, S.; Filliâtre, J., Formal verification of floating-point programs, 187-194 (2007), New York
[8] Botella B, Gotlieb A, Michel C (2006) Symbolic execution of floating-point computations. Softw Test Verif Reliab 16(2):97-121 · doi:10.1002/stvr.333
[9] Brain, M.; D’Silva, V.; Haller, L.; Griggio, A.; Kroening, D., An abstract interpretation of DPLL(T), 455-475 (2013), Berlin · Zbl 1426.68249 · doi:10.1007/978-3-642-35873-9_27
[10] Brain, M.; D’Silva, V.; Haller, L.; Griggio, A.; Kroening, D., Interpolation-based verification of floating-point programs with abstract CDCL, 412-432 (2013), Berlin · doi:10.1007/978-3-642-38856-9_22
[11] Brillout, A.; Kroening, D.; Wahl, T., Mixed abstractions for floating-point arithmetic, 69-76 (2009), New York
[12] Chapoutot, A., Interval slopes as a numerical abstract domain for floating-point variables, 184-200 (2010), Berlin · Zbl 1306.68001 · doi:10.1007/978-3-642-15769-1_12
[13] Chen, L.; Miné, A.; Cousot, P., A sound floating-point polyhedra abstract domain, 3-18 (2008), Berlin
[14] Chen, L.; Miné, A.; Wang, J.; Cousot, P., Interval polyhedra: an abstract domain to infer interval linear relationships, 309-325 (2009), Berlin · Zbl 1248.68140 · doi:10.1007/978-3-642-03237-0_21
[15] Chen, L.; Miné, A.; Wang, J.; Cousot, P., An abstract domain to discover interval linear equalities, 112-128 (2010), Berlin · Zbl 1273.68081 · doi:10.1007/978-3-642-11319-2_11
[16] Cimatti, A.; Griggio, A.; Schaafsma, B.; Sebastiani, R., The MathSAT5 SMT solver, 93-107 (2013), Berlin · Zbl 1381.68153 · doi:10.1007/978-3-642-36742-7_7
[17] Clarke, E.; Kroening, D.; Lerda, F., A tool for checking ANSI-C programs, 168-176 (2004), Berlin · Zbl 1126.68470 · doi:10.1007/978-3-540-24730-2_15
[18] Conchon, S.; Melquiond, G.; Roux, C.; Iguernelala, M., Built-in treatment of an axiomatic floating-point theory for SMT solvers (2012)
[19] Cotton, S., Natural domain SMT: a preliminary assessment, 77-91 (2010), Berlin · Zbl 1290.68112 · doi:10.1007/978-3-642-15297-9_8
[20] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, 238-252 (1977), New York
[21] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, 269-282 (1979), New York
[22] Cousot, P.; Cousot, R.; Mauborgne, L., The reduced product of abstract domains and the combination of decision procedures, 456-472 (2011), Berlin · Zbl 1326.68089
[23] Cowlishaw M (ed) (2008) IEEE standard for floating-point arithmetic. IEEE, New York, pp 1132-1138
[24] Daumas, M.; Rideau, L.; Théry, L., A generic library for floating-point numbers and its application to exact computing, 169-184 (2001), Berlin · Zbl 1005.68544 · doi:10.1007/3-540-44755-5_13
[25] Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. Commun ACM 5:394-397 · Zbl 0217.54002 · doi:10.1145/368273.368557
[26] Moura, L.; Bjørner, N., Z3: an efficient SMT solver, 337-340 (2008), Berlin · doi:10.1007/978-3-540-78800-3_24
[27] Delmas, D.; Goubault, E.; Putot, S.; Souyris, J.; Tekkal, K.; Védrine, F., Towards an industrial use of FLUCTUAT on safety-critical avionics software, 53-69 (2009), Berlin · doi:10.1007/978-3-642-04570-7_6
[28] D’Silva, V.; Haller, L.; Kroening, D., Satisfiability solvers are static analyzers, 317-333 (2012), Berlin · doi:10.1007/978-3-642-33125-1_22
[29] D’Silva, V.; Haller, L.; Kroening, D.; Tautschnig, M., Numeric bounds analysis with conflict-driven learning, 48-63 (2012), Berlin · Zbl 1352.68060 · doi:10.1007/978-3-642-28756-5_5
[30] D’Silva, V.; Haller, L.; Kroening, D., Abstract conflict driven learning, 143-154 (2013), New York · Zbl 1301.68156
[31] D’Silva V, Haller L, Kroening D (2014) Abstract satisfaction. In: Proc of principles of programming languages (to appear). ACM, New York · Zbl 1284.68392
[32] Feret, J., Static analysis of digital filters, 33-48 (2004), Berlin · Zbl 1126.68347
[33] Fränzle 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-4):209-236 · Zbl 1144.68371
[34] Ganzinger, H.; Hagen, G.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., DPLL(T): fast decision procedures, 175-188 (2004), Berlin · Zbl 1103.68616 · doi:10.1007/978-3-540-27813-9_14
[35] Ghorbal, K.; Goubault, E.; Putot, S., The zonotope abstract domain Taylor1+, 627-633 (2009), Berlin · doi:10.1007/978-3-642-02658-4_47
[36] Goldwasser, D.; Strichman, O.; Fine, S., A theory-based decision heuristic for DPLL(T), 1-8 (2008), New York
[37] Goubault, E., Static analyses of the precision of floating-point operations, 234-259 (2001), Berlin · Zbl 0997.68518 · doi:10.1007/3-540-47764-0_14
[38] Goubault, E.; Putot, S.; Baufreton, P.; Gassino, J., Static analysis of the accuracy in control systems: principles and experiments, 3-20 (2007), Berlin
[39] Harris, WR; Sankaranarayanan, S.; Ivančić, F.; Gupta, A., Program analysis via satisfiability modulo path programs, 71-82 (2010) · Zbl 1312.68058
[40] Harrison, J., A machine-checked theory of floating point arithmetic, 113-130 (1999), Berlin · doi:10.1007/3-540-48256-3_9
[41] Harrison J (2000) Floating point verification in HOL light: the exponential function. Form Methods Syst Des 16(3):271-305 · doi:10.1023/A:1008712907154
[42] Harrison, J., Formal verification of floating point trigonometric functions, 217-233 (2000), Berlin
[43] Harrison J (2003) Formal verification of square root algorithms. Form Methods Syst Des 22(2):143-153 · Zbl 1021.68058 · doi:10.1023/A:1022973506233
[44] Harrison J (2007) Floating-point verification. J Univers Comput Sci 13(5):629-638
[45] Jan Peleska, EV; Lapschies, F., Automated test case generation with SMT-solving and abstract interpretation, 298-312 (2011), Berlin · doi:10.1007/978-3-642-20398-5_22
[46] Jeannet, B.; Miné, A., Apron: a library of numerical abstract domains for static analysis, 661-667 (2009), Berlin · doi:10.1007/978-3-642-02658-4_52
[47] Jovanovic, D.; Moura, L., Cutting to the chase: solving linear integer arithmetic, 338-353 (2011), Berlin · Zbl 1314.90054
[48] Jovanovic, D.; Moura, L., Solving non-linear arithmetic, 339-354 (2012), Berlin · Zbl 1358.68257 · doi:10.1007/978-3-642-31365-3_27
[49] Kaivola, R.; Aagaard, M., Divider circuit verification with model checking and theorem proving, 338-355 (2000), Berlin · Zbl 0974.68519 · doi:10.1007/3-540-44659-1_21
[50] Lapschies, F.; Peleska, J.; Gorbachuk, E.; Mangels, T., sonolar SMT-solver (2012)
[51] McMillan, K.; Kuehlmann, A.; Sagiv, M., Generalizing DPLL to richer logics, 462-476 (2009), Berlin · Zbl 1242.68282 · doi:10.1007/978-3-642-02658-4_35
[52] McMillan, KL, Lazy annotation for program testing and verification, 104-118 (2010), Berlin · doi:10.1007/978-3-642-14295-6_10
[53] Melquiond G (2012) Floating-point arithmetic in the Coq system. Inf Comput 216:14-23 · Zbl 1257.68131 · doi:10.1016/j.ic.2011.09.005
[54] Michel, C., Exact projection functions for floating point number constraints (2002)
[55] Michel, C.; Rueher, M.; Lebbah, Y., Solving constraints over floating-point numbers, 524-538 (2001), Berlin · Zbl 1067.68658
[56] Miné, A., Relational abstract domains for the detection of floating-point run-time errors, 3-17 (2004), Berlin · Zbl 1126.68353
[57] Miner PS (1995) Defining the IEEE-854 floating-point standard in PVS. PVS. Technical Memorandum 110167, NASA, Langley Research
[58] Monniaux, D., Compositional analysis of floating-point linear numerical filters, 199-212 (2005), Berlin · Zbl 1081.93028 · doi:10.1007/11513988_21
[59] Monniaux D (2008) The pitfalls of verifying floating-point computations. ACM Trans Program Lang Syst 30(3)
[60] 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-916 · Zbl 1392.68051 · doi:10.1109/12.713311
[61] Muller JM, Brisebarre N, de Dinechin F, Jeannerod CP, Lefèvre V, Melquiond G, Revol N, Stehlé D, Torres S (2010) Handbook of floating-point arithmetic, 1st edn. Springer, Berlin · Zbl 1197.65001 · doi:10.1007/978-0-8176-4705-6
[62] Rival X, Mauborgne L (2007) The trace partitioning abstract domain. ACM Trans Program Lang Syst 29(5):26 · doi:10.1145/1275497.1275501
[63] Rümmer, P.; Wahl, T., An SMT-LIB theory of binary floating-point arithmetic (2010)
[64] 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-200 · Zbl 0910.68008 · doi:10.1112/S1461157000000176
[65] Sakallah KA, Marques-Silva J (2011) Anatomy and empirical evaluation of modern SAT solvers. Bull Eur Assoc Theor Comput Sci 103:96-121 · Zbl 1258.68137
[66] Silva, JPM; Lynce, I.; Malik, S., Conflict-driven clause learning SAT solvers, 131-153 (2009), Amsterdam
[67] Silva JPM, Sakallah KA (1999) GRASP: a search algorithm for propositional satisfiability. Trans Comput 48(5):506-521 · Zbl 1392.68388 · doi:10.1109/12.769433
[68] Thakur, A.; Reps, T., A generalization of Stålmarck’s method, 334-351 (2012), Berlin · doi:10.1007/978-3-642-33125-1_23
[69] Thakur, A.; Reps, T., A method for symbolic computation of abstract operations, 174-192 (2012), Berlin · doi:10.1007/978-3-642-31424-7_17
[70] Zhang, L.; Madigan, CF; Moskewicz, MW; Malik, S., Efficient conflict driven learning in a Boolean satisfiability solver, 279-285 (2001), New York
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.