[36] ILOG-S.A. Ilog solver 6.0: Reference manual. 2003.

[37] Joxan Jaffar and Michael J. Maher. Constraint logic programming: A survey. Journal of Logic Programming**, 19/20:503–581, 1994.**
[38] Himanshu Jain and Edmund M. Clarke. Efficient SAT solving **for non-clausal formulas using DPLL,**
graphs, and watched cuts. In Design Automation Conference**, pages 563–568. ACM, 2009.**
[39] Dejan Jovanovi´c and Predrag Janiˇci´c. Logical analysis of hash functions. In **Frontiers of Combining**
Systems (FroCoS)**, LNCS 3717, pages 200–215. Springer, 2005.**
[40] James C. King. Symbolic execution and program testing. Communications of the ACM**, 19(7):385–394,**
1976.

[41] Ali Sinan K¨oksal, Viktor Kuncak, and Philippe Suter. Scala to the power of z3: Integrating smt and programming. In 23rd International Conference on Automated Deduction - CADE-23**, LNCS 6803,** pages 400–406. Springer, 2011.

[42] Nicola Leone, Gerald Pfeifer, Wolfgang Faber, Thomas Eiter, Georg Gottlob, Simona Perri, and Francesco Scarcello. The DLV system for knowledge representation and reasoning. **ACM Transactions**
on Computational Logic**, 7(3):499–562, 2006.**
[43] Toni Mancini, Davide Micaletto, Fabio Patrizi, and Marco Cadoli. Evaluating ASP and Commercial Solvers on the CSPLib. Constraints**, 13(4):407–436, 2008.**
[44] Filip Mari´c. Formalization and Implementation of Modern SAT Solvers. Journal of Automated Reasoning**, 43(1):81–119, 2009.**
[45] Filip Mari´c and Predrag Janiˇci´c. Formal Correctness Proof for DPLL Procedure. Informatica**, 21(1):57–**
78, 2009.

[46] Filip Mari´c and Predrag Janiˇci´c. Urbiva: Uniform reduction to bit-vector arithmetic. In **Automated**
Reasoning (IJCAR 2010)**, LNCS 6173, pages 346–352. Springer, 2010.**
[47] Kim Marriott, Nicholas Nethercote, Reza Rafeh, Peter J. Stuckey, Maria Garcia de la Banda, and Mark Wallace. The design of the zinc modelling language. Constraints**, 13(3), 2008.**
[48] Fabio Massacci and Laura Marraro. Logical cryptanalysis as a SAT problem. **Journal of Automated**
Reasoning**, 24(1-2):165–203, 2000.**
[49] Laurent Michel and Pascal Van Hentenryck. The comet programming language and system. In **Principles**
and Practice of Constraint Programming - CP 2005**, LNCS 3709, pages 881–881. Springer, 2005.**
[50] Ilya Mironov and Lintao Zhang. Applications of sat solvers to cryptanalysis of hash functions. In **Theory**
and Applications of Satisfiability Testing - SAT 2006**, LNCS 4121, pages 102–115. Springer, 2006.**
[51] David G. Mitchell and Eugenia Ternovska. A framework for representing and solving np search problems.

In National Conference on Artificial Intelligence - AAAI 2005**, pages 430–435. AAAI Press / The MIT**
Press, 2005.

[52] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: engineering an efficient SAT solver. In **DAC '01: Proceedings of the 38th Conference on Design Automation**,
pages 530–535. ACM Press, 2001.

[53] Rafiq Muhammad and Peter J. Stuckey. A Stochastic Non-CNF SAT Solver. In **PRICAI 2006: Trends**
in Artificial Intelligence**, LNCS 4099, pages 120–129. Springer, 2006.**
[54] Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. Minizinc: Towards a standard cp modelling language. In **Principles and Practice of Constraint** Programming - CP 2007**, LNCS 4741, pages 529–543. Springer, 2007.**
[55] Mladen Nikoli´c, Filip Mari´c, and Predrag Janiˇci´c. **Instance-based selection of policies for SAT solvers.**
In Theory and Applications of Satisfiability Testing - SAT 2009**, LNCS 5584, pages 326–340. Springer,**
2009.

[56] Corina S. Pasareanu and Willem Visser. Verification of Java programs using symbolic execution and invariant generation. In Model Checking Software - SPIN**, LNCS 2989, pages 164–181. Springer, 2004.**
[57] Corina S. Pasareanu and Willem Visser. A survey of new trends in symbolic execution for software testing and analysis. International Journal on Software Tools for Technology Transfer (STTT)**, 11(4):339–**
353, 2009.

[58] Nikolay Pelov and Eugenia Ternovska. Reducing inductive definitions to propositional satisfiability. In International Conference on Logic Programming - ICLP 2005**, LNCS 3668, pages 221–234. Springer,**
2005.

[59] Gordon D. Plotkin. A Structural Approach to Operational Semantics. Technical Report Tech. Rep.

DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark., 1981.