Exploiting Binary Floating-Point Representations for Constraint Propagation

References

• Ammann PE, Knight JC (1988) Data diversity: An approach to software fault tolerance. IEEE Trans. Comput. 37:418–425.Crossref, Google Scholar
• Arcuri A (2009) Theoretical analysis of local search in software testing. Watanabe O, Zeugmann T, eds. Proc. 5th Internat. Sympos. Stochastic Algorithms: Foundations Appl. (SAGA 2009), Lecture Notes in Computer Science, Vol. 5792 (Springer-Verlag, Berlin), 156–168.Crossref, Google Scholar
• Bagnara R, Carlier M, Gori R, Gotlieb A (2013) Symbolic path-oriented test data generation for floating-point programs. Proc. 6th IEEE Internat. Conf. Software Testing, Verification and Validation (IEEE Press, New York).Crossref, Google Scholar
• Bagnara R, Carlier M, Gori R, Gotlieb A (2015) Online supplement to: Exploiting binary floating-point representations for constraint filtering. INFORMS J. Comput. Forthcoming.Google Scholar
• Belaid MS (2013) Résolution de contraintes sur les flottants dédié à la vérification de programmes. Thèse pour obtenir le titre de “Docteur en Sciences,” École doctorale STIC, Université de Nice—Sophia Antipolis, Nice, France.Google Scholar
• Belaid MS, Michel C, Rueher M (2012) Boosting local consistency algorithms over floating-point numbers. Milano M, ed. Proc. 18th Internat. Conf. Principles and Practice of Constraint Programming, Lecture Notes in Computer Science, Vol. 7514 (Springer-Verlag, Berlin), 127–140.Crossref, Google Scholar
• Blanc B, Bouquet F, Gotlieb A, Jeannet B, Jeron T, Legeard B, Marre B, Michel C, Rueher M (2006) The V3F project. Proc. 1st Workshop on Constraints in Software Testing, Verification and Anal. (CSTVA’06), Nantes, France, 5–21.Google Scholar
• Borges M, d’Amorim M, Anand S, Bushnell D, Pasareanu CS (2012) Symbolic execution with interval solving and meta-heuristic search. Proc. 5th IEEE Internat. Conf. Software Testing, Verification and Validation (IEEE Computer Society, Washington, DC),111–120.Crossref, Google Scholar
• Botella B, Gotlieb A, Michel C (2006) Symbolic execution of floating-point computations. Software Testing, Verification Reliability 16:97–121.Crossref, Google Scholar
• Burdy L, Dufour J-L, Lecomte T (2012) The B method takes up floating-point numbers. Proc. 6th Internat. Conf. Exhibition on Embedded Real Time Software and Systems (ERTS 2012), Toulouse, France.Google Scholar
• Carlier M, Gotlieb A (2011) Filtering by ULP maximum. Proc. 23rd IEEE Internat. Conf. Tools with Artificial Intelligence (ICTAI 2011) (IEEE Computer Society, Washington, DC), 209–214.Crossref, Google Scholar
• Chabert G, Jaulin L (2009) Contractor programming. Artificial Intelligence 173:1079–1100.Crossref, Google Scholar
• Chan FT, Chen TY, Cheung SC, Lau MF, Yiu SM (1998) Application of metamorphic testing in numerical analysis. Proc. IASTED Internat. Conf. Software Engrg. (SE’98) (ACTA Press, Calgary, Alberta, Canada), 191–197.Google Scholar
• Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. Jensen K, Podelski A, eds. Tools and Algorithms for the Construction and Analysis of Systems, Proc. 10th Internat. Conf. (TACAS 2004), Lecture Notes in Computer Science, Vol. 2988 (Springer-Verlag, Berlin), 168–176.Crossref, Google Scholar
• Cousot P, Cousot R (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proc. Fourth Annual ACM Sympos. Principles of Programming Languages (ACM Press, New York), 238–252.Crossref, Google Scholar
• Denmat T, Gotlieb A, Ducassé M (2007) Improving constraint-based testing with dynamic linear relaxations. Proc. 18th IEEE Internat. Sympos. Software Reliability (ISSRE 2007) (IEEE Computer Society, Washington, DC), 181–190.Crossref, Google Scholar
• D’Silva V, Haller L, Kroening D, Tautschnig M (2012) Numeric bounds analysis with conflict-driven learning. Flanagan C, König B, eds. Tools Algorithms Construction Anal. Systems, Proc. 18th Internat. Conf. (TACAS 2012), Lecture Notes in Computer Science, Vol. 7214 (Springer, Berlin), 48–63.Crossref, Google Scholar
• Godefroid P, Klarlund N, Sen K (2005) DART: Directed automated random testing. Sarkar V, Hall MW, eds. Proc. ACM SIGPLAN 2005 Conf. Programming Language Design Implementation (PLDI 2005) (ACM, New York), 213–223.Crossref, Google Scholar
• Goldberg D (1991) What every computer scientist should know about floating-point arithmetic. ACM Comput. Surveys 23:5–48.Crossref, Google Scholar
• Goubault E (2001) Static analyses of the precision of floating-point operations. Cousot P, ed. Static Anal.: 8th Internat. Sympos., SAS 2001, Lecture Notes in Computer Science, Vol. 2126 (Springer-Verlag, Berlin), 234–259.Crossref, Google Scholar
• Granvilliers L, Benhamou F (2006) Algorithm 852: RealPaver: An interval solver using constraint satisfaction techniques. ACM Trans. Math. Software 32:138–156.Crossref, Google Scholar
• IBM Labs in Haifa, FPgen Team (2008) Floating-point test-suite for IEEE, version 1.02. Accessed December 29, 2015, https://www.research.ibm.com/haifa/projects/verification/fpgen/papers/ieee-test-suite-v2.pdf.Google Scholar
• IEEE Computer Society (2008) IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008 (IEEE, New York).Google Scholar
• Korel B (1990) Automated software test data generation. IEEE Trans. Software Engrg. 16:870–879.Crossref, Google Scholar
• Kuliamin VV (2010) Standardization and testing of mathematical functions. Pnueli A, Virbitskaite I, Voronkov A, eds. Perspectives Systems Informatics, Revised Papers 7th Internat. Andrei Ershov Memorial Conf. (PSI 2009), Lecture Notes in Computer Science, Vol. 5947 (Springer-Verlag, Berlin), 257–268.Crossref, Google Scholar
• Lakhotia K, Harman M, Gross H (2010a) AUSTIN: A tool for search based software testing for the C language and its evaluation on deployed automotive systems. Proc. 2nd Internat. Sympos. Search Based Software Engrg. (SSBSE ’10) (IEEE Computer Society, Washington, DC), 101–110.Crossref, Google Scholar
• Lakhotia K, Tillmann N, Harman M, De Halleux J (2010b) FloPSy: Search-based floating point constraint solving for symbolic execution. Proc. 22nd IFIP WG 6.1 Internat. Conf. Testing Software Systems (Springer-Verlag, Berlin), 142–157.Crossref, Google Scholar
• Lebbah Y (2009) ICOS: A branch and bound based solver for rigorous global optimization. Optim. Methods Software 24:709–726.Crossref, Google Scholar
• Marre B, Blanc B (2005) Test selection strategies for Lustre descriptions in GATeL. Gurevich Y, Petrenko AK, Kossatchev A, eds. Proc. Workshop Model Based Testing (MBT 2004), Electronic Notes in Theoretical Computer Science, Vol. 111 (Elsevier Science Publishers B. V., Amsterdam), 93–111.Crossref, Google Scholar
• Marre B, Michel C (2010) Improving the floating point addition and subtraction constraints. Cohen D, ed. Proc. 16th Internat. Conf. Principles Practice Constraint Programming (CP 2010), Lecture Notes in Computer Science, Vol. 6308 (Springer, Berlin), 360–367.Crossref, Google Scholar
• McMinn P (2004) Search-based software test data generation: A survey. Software Testing, Verification Reliability 14:105–156.Crossref, Google Scholar
• Michel C (2002) Exact projection functions for floating point number constraints. Proc. 7th Internat. Sympos. Artificial Intelligence Math., Fort Lauderdale, FL.Google Scholar
• Michel C (2013) Personal communication with authors, December.Google Scholar
• Michel C, Rueher M, Lebbah Y (2001) Solving constraints over floating-point numbers. Walsh T, ed. Proc. 7th Internat. Conf. Principles and Practice of Constraint Programming (CP 2001), Lecture Notes in Computer Science, Vol. 2239 (Springer-Verlag, Berlin), 524–538.Crossref, Google Scholar
• Miller W, Spooner DL (1976) Automatic generation of floating-point test data. IEEE Trans. Software Engrg. 2:223–226.Crossref, Google Scholar
• Monniaux D (2008) The pitfalls of verifying floating-point computations. ACM Trans. Programming Languages Systems 30:Article no. 12.Crossref, Google Scholar
• Muller J-M (2005) On the definition of ulp(x). Technical report RR-5504, INRIA, Montbonnot-Saint-Martin, France.Google Scholar
• Scott NS, Jézéquel F, Denis C, Chesneaux J-M (2007) Numerical “health check” for scientific codes: The CADNA approach. Comput. Physics Comm. 176:507–521.Crossref, Google Scholar
• Skeel R (1992) Roundoff error and the Patriot missile. SIAM News 25:11.Google Scholar
• Tang E, Barr ET, Li X, Su Z (2010) Perturbing numerical calculations for statistical analysis of floating-point program (in)stability. Tonella P, Orso A, eds. Proc. 19th Internat. Sympos. Software Testing and Analysis (ISSTA 2010) (ACM Press, New York), 131–142.Crossref, Google Scholar
• Weyuker EJ (1982) On testing non-testable programs. Comput. J. 25:465–470.Crossref, Google Scholar