B. Beckert, R. Hähnle, and P. H. Schmitt, Verification of Object-Oriented Software: The KeY Approach, LNCS, vol.4334, 2007.
DOI : 10.1007/978-3-540-69061-0

A. R. Bradley, Z. Manna, and H. B. Sipma, What's decidable about arrays? In VMCAI, LNCS, vol.3855, pp.427-442, 2006.

C. Csallner and Y. Smaragdakis, Check 'n' crash, Proceedings of the 27th international conference on Software engineering , ICSE '05, pp.422-431, 2005.
DOI : 10.1145/1062455.1062533

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

X. Deng, R. , J. Hatcliff, /. Kiasan, and . Kunit, Kiasan/KUnit: Automatic Test Case Generation and Analysis Feedback for Open Object-oriented Systems, Testing: Academic and Industrial Conference Practice and Research Techniques, MUTATION (TAICPART-MUTATION 2007), pp.3-12, 2007.
DOI : 10.1109/TAIC.PART.2007.32

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102

L. Bousquet, Y. Ledru, O. Maury, C. Oriat, and J. Lanet, A case study in JML-based software validation, Proceedings. 19th International Conference on Automated Software Engineering, 2004., pp.294-297, 2004.
DOI : 10.1109/ASE.2004.1342750

B. Dutertre and L. De-moura, The YICES SMT solver, 2006.

C. Engel, C. Gladisch, V. Klebanov, and P. Rümmer, Integrating Verification and Testing of Object-Oriented Software, LNCS, vol.4966, pp.182-191, 2008.
DOI : 10.1007/978-3-540-79124-9_13

Y. Ge and L. M. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, CAV, pp.306-320, 2009.
DOI : 10.1007/978-3-642-02658-4_25

S. Ghilardi, Quantifier Elimination and Provers Integration, Electronic Notes in Theoretical Computer Science, vol.86, issue.1, 2003.
DOI : 10.1016/S1571-0661(04)80650-9
URL : http://doi.org/10.1016/s1571-0661(04)80650-9

C. Gladisch, Verification-Based Test Case Generation for Full Feasible Branch Coverage, 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, pp.159-168, 2008.
DOI : 10.1109/SEFM.2008.22
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.161.4999

C. Gladisch, Could we have chosen a better loop invariant or method contract? In TAP, LNCS, vol.5668, pp.74-89, 2009.

D. Harel, D. Kozen, and J. Tiuryn, Dynamic Logic, 2000.

J. R. Kiniry, A. E. Morkan, and B. Denby, Soundness and completeness warnings in ESC/Java2, Proceedings of the 2006 conference on Specification and verification of component-based systems , SAVCBS '06, pp.19-24, 2006.
DOI : 10.1145/1181195.1181200

G. Leavens and Y. Cheon, Design by contract with JML, 2006.

P. Mcminn, Search-based software test data generation: a survey, Software Testing, Verification and Reliability, vol.14, issue.2, pp.105-156, 2004.
DOI : 10.1002/stvr.294

M. Moskal, J. Lopuszanski, and J. R. Kiniry, E-matching for Fun and Profit, Electronic Notes in Theoretical Computer Science, vol.198, issue.2, pp.19-35, 2008.
DOI : 10.1016/j.entcs.2008.04.078
URL : http://doi.org/10.1016/j.entcs.2008.04.078

R. Nieuwenhuis, A. Oliveras, E. Rodríguez-carbonell, and A. Rubio, Challenges in Satisfiability Modulo Theories, RTA, pp.2-18, 2007.
DOI : 10.1007/978-3-540-73449-9_2

P. Rümmer, Sequential, Parallel, and Quantified Updates of First-Order Structures, LPAR, pp.422-436, 2006.
DOI : 10.1007/11916277_29

W. Visser, C. P?as?areanup?as?p?as?areanu, and S. Khurshid, Test input generation with Java PathFinder, ISSTA, pp.97-107, 2004.
DOI : 10.1145/1007512.1007526
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.4263

J. Zhang and H. Zhang, Extending Finite Model Searching with Congruence Closure Computation, AISC, pp.94-102, 2004.
DOI : 10.1007/978-3-540-30210-0_9