A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded Model Checking, Handbook of Satisfiability, pp.457-481, 2009.
DOI : 10.1016/S0065-2458(03)58003-2

A. Biere, M. Heule, H. Van-maaren, and T. Walsh, Conflict-driven clause learning SAT solvers, Handbook of Satisfiability, pp.131-153, 2009.

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, SATABS: SAT-Based Predicate Abstraction for ANSI-C, LNCS, vol.3440, pp.570-574, 2005.
DOI : 10.1007/978-3-540-31980-1_40

S. Edelkamp, A. L. Lafuente, and S. Leue, Directed explicit model checking with HSF-SPIN, LNCS, vol.2057, pp.57-79, 2001.
DOI : 10.1007/3-540-45139-0_5
URL : http://www.di.unipi.it/~lafuente/papers/directed_model_checking.ps.gz

D. Le-berre and A. , Parrain: The Sat4J library, release 2.2, Journal on Satisfiability Boolean Modeling and Computation, vol.7, pp.59-64, 2010.

F. Reffe and S. , Edelkamp: Error detection with directed symbolic model checking, Proceedings FM'99, pp.195-211, 1999.
DOI : 10.1007/3-540-48119-2_13
URL : http://www.informatik.uni-freiburg.de/~edelkamp/publications/./heu_se.pdf

O. Shtrichman, Tuning SAT Checkers for Bounded Model Checking, Computer Aided Verification, pp.480-494, 2000.
DOI : 10.1007/10722167_36
URL : http://www.research.ibm.com/pics/verification/ps/sat-bmc1.ps

C. Wang, H. Jin, G. D. Hachtel, and F. Somenzi, Refining the SAT decision ordering for bounded model checking, Proceedings of the 41st annual conference on Design automation , DAC '04, pp.535-538, 2004.
DOI : 10.1145/996566.996713

E. Zarpas, Benchmarking SAT Solvers for Bounded Model Checking, Theory and Applications of Satisfiability Testing, pp.340-354, 2005.
DOI : 10.1007/11499107_25
URL : http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/ps/sat05.pdf

B. Demsky and P. Lam, SATCheck: SAT-directed stateless model checking for SC and TSO, In: ACM SIGPLAN Notices, pp.20-36, 2015.
DOI : 10.1145/2858965.2814297

G. Audemard and L. Simon, Predicting Learnt Clauses Quality in Modern SAT Solvers, IJCAI, pp.399-404, 2009.

A. S. Andisha, M. Wehrle, and B. Westphal, Directed Model Checking for PROMELA with Relaxation-Based Distance Functions, pp.153-159, 2015.
DOI : 10.1007/978-3-319-23404-5_11

J. Maeoka, Y. Tanabe, and F. , Ishikawa: Depth-First Heuristic Search for Software Model Checking, Science, pp.75-96, 2016.
DOI : 10.1007/978-3-319-23467-0_6

J. Schrieb, H. Wehrheim, and D. , Wonisch: Three-valued spotlight abstractions, International Symposium on Formal Methods, pp.106-122, 2009.
DOI : 10.1007/978-3-642-05089-3_8
URL : http://www.cs.uni-paderborn.de/uploads/tx_sibibtex/spotlight.pdf

G. S. Tseytin, On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic, pp.115-125, 1970.

A. Van-gelder, Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces, pp.141-146, 2009.
DOI : 10.1007/978-3-540-72788-0_31

H. Zhang and M. , Stickel: An efficient algorithm for unit-propagation, 4th Int. Symposium on Artificial Intelligence and Mathematics, pp.166-169, 1996.