Editing Model-based testing (section)

===Constraint logic programming and symbolic execution===
[[Constraint programming]] can be used to select test cases satisfying specific constraints by solving a set of constraints over a set of variables. The system is described by the means of constraints.<ref>Jefferson Offutt. Constraint-Based Automatic Test Data Generation. IEEE Transactions on Software Engineering, 17:900-910, 1991</ref>  Solving the set of constraints can be done by Boolean solvers (e.g. SAT-solvers based on the [[Boolean satisfiability problem]]) or by [[numerical analysis]], like the [[Gaussian elimination]]. A solution found by solving the set of constraints formulas can serve as a test cases for the corresponding system.

Constraint programming can be combined with symbolic execution. In this approach a system model is executed symbolically, i.e. collecting data constraints over different control paths, and then using the constraint programming method for solving the constraints and producing test cases.<ref>Antti Huima. Implementing Conformiq Qtronic. 
Testing of Software and Communicating Systems,
Lecture Notes in Computer Science, 2007, Volume 4581/2007, 1-12, DOI: 10.1007/978-3-540-73066-8_1
</ref>