D. Beyer and S. Löwe, Explicit-State Software Model Checking Based on CEGAR and Interpolation, Fundamental Approaches to Software Engineering, pp.146-162, 2013.
DOI : 10.1007/978-3-642-37057-1_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.297.8753

D. Beyer, S. Löwe, and P. Wendler, Refinement Selection, Model Checking Software, pp.20-38, 2015.
DOI : 10.1007/978-3-319-23404-5_3

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs, Tools and Algorithms for the Construction and Analysis of Systems, pp.193-207, 1999.
DOI : 10.1007/3-540-49059-0_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.8033

I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim, Slicing Abstractions, International Symposium on Fundamentals of Software Engineering, pp.17-32, 2007.
DOI : 10.1007/978-3-540-75698-9_2

G. Cabodi, C. Loiacono, M. Palena, P. Pasini, D. Patti et al., Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks, Journal on Satisfiability Boolean Modeling and Computation, vol.9, pp.135-172, 2016.

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM, vol.50, issue.5, pp.752-794, 2003.
DOI : 10.1145/876638.876643
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.8938

E. M. Clarke, O. Grumberg, and D. Peled, Model checking, 1999.

E. M. Clarke, A. Gupta, and O. Strichman, SAT-Based Counterexample-Guided Abstraction Refinement, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.23, issue.7, pp.1113-1123, 2004.
DOI : 10.1109/TCAD.2004.829807
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.2429

W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The Journal of Symbolic Logic, vol.14, issue.03, pp.269-285, 1957.
DOI : 10.2307/2963594

B. Dutertre and M. Sorea, Timed systems in SAL, Tech. rep., SRI International, 2004.

E. Ermis, J. Hoenicke, and A. Podelski, Splitting via Interpolants, Model Checking, and Abstract Interpretation, pp.186-201, 2012.
DOI : 10.1007/11817963_14

F. Adiego, B. Darvas, D. Blanco-viñuela, E. Tournier, J. C. Bliudze et al., Applying Model Checking to Industrial-Sized PLC Programs, IEEE Transactions on Industrial Informatics, vol.11, issue.6, pp.1400-1410, 2015.
DOI : 10.1109/TII.2015.2489184

S. Graf and H. Saidi, Construction of abstract state graphs with PVS, Computer Aided Verification, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. Mcmillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.232-244, 2004.
DOI : 10.1145/964001.964021
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.1200

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.58-70, 2002.
DOI : 10.1145/565816.503279

K. L. Mcmillan, Lazy Abstraction with Interpolants, Computer Aided Verification, pp.123-136, 2006.
DOI : 10.1007/11817963_14

K. Mcmillan, Applications of Craig Interpolants in Model Checking, LNCS, vol.3440, pp.1-12, 2005.
DOI : 10.1007/978-3-540-31980-1_1

L. De-moura and N. Bjørner, Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.4963, pp.337-340, 2008.

Y. Vizel and O. Grumberg, Interpolation-sequence based model checking, 2009 Formal Methods in Computer-Aided Design, pp.1-8, 2009.
DOI : 10.1109/FMCAD.2009.5351148
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.159.2713