CORAL

What is CORAL?

CORAL is a meta-heuristic constraint solvers for dealing with numerical constraints involving floating-point variables and mathematical functions.

Target

The goal of CORAL is to improve symbolic execution of numeric applications. Symbolic execution is a technique to systematically generate test input data. It requires a constraint solver component to solve the constraints it generates during the analysis of a program. Certain classes of constraints admit a (decision) procedure that can deterministically answer whether or not a constraint is satisfiable (with a witness solution). The theory of linear integer arithmetic is an example of decidable theory. Unfortunately, symbolic execution of certain programs (e.g., scientific programs) can generate constraints involving undecidable or intractable theories. CORAL uses search to find solutions for such constraints. CORAL is integrated to the Symbolic PathFinder (SPF) symbolic execution tool.

Approach

CORAL treats constraint solving as a search problem. To that end, it explores alternatives to reduce the search space and strategies to search for solutions. Currently, CORAL includes three types of solvers: RANDOM, AVM (for alternating variable method) and PSO (for particle swarm optimization). We currently use the Opt4j library for implementing the search. Also, CORAL can use candidate solutions drawn from the intervals reported by interval-based solvers (like RealPaver and ICOS) to seed the population of the meta-heuristic search.

Contributors

• Mateus Borges
• Marcelo d'Amorim
• Corina Păsăreanu
• Matheus Souza
• Saswat Anand
• David Bushnell

Contact

Please send bug reports, comments, or questions to Mateus Borges (mab at cin dot ufpe dot br) or Matheus Souza (mbas at cin dot ufpe dot br)