A. Albarghouthi, Y. Li, A. Gurfinkel, and M. Chechik, Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification, Proc. CAV, pp.672-678, 2012.
DOI : 10.1007/978-3-642-31424-7_48
URL : http://www.cs.toronto.edu/~chechik/pubs/cav12.pdf

F. Alberti, R. Bruttomesso, S. Ghilardi, S. Ranise, and N. Sharygina, An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods in System Design, pp.63-109, 2014.

S. Apel, D. Beyer, K. Friedberger, F. Raimondi, and A. Von-rhein, Domain Types: Abstract-Domain Selection Based on Variable Usage, Proc. HVC, pp.262-278, 2013.
DOI : 10.1007/978-3-319-03077-7_18
URL : http://www.infosun.fim.uni-passau.de/publications/docs/HVC2013.pdf

T. Ball, B. Cook, V. Levin, and S. K. Rajamani, SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft, Proc. IFM, LNCS 2999, pp.1-20, 2004.
DOI : 10.1007/978-3-540-24756-2_1

T. Ball and S. K. Rajamani, The Slam project: Debugging system software via static analysis, Proc. POPL, pp.1-3, 2002.

D. Beyer, Software Verification and Verifiable Witnesses, Proc. TACAS, pp.401-416, 2015.
DOI : 10.1007/978-3-662-46681-0_31

D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, The software model checker Blast, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.5-6505, 2007.
DOI : 10.1007/978-1-4757-3540-6

D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko, Path invariants, Proc. PLDI, pp.300-309, 2007.
DOI : 10.1145/1273442.1250769

D. Beyer, T. A. Henzinger, and G. Théoduloz, Program Analysis with Dynamic Precision Adjustment, 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pp.29-38, 2008.
DOI : 10.1109/ASE.2008.13

D. Beyer and M. E. Keremoglu, CPAchecker: A Tool for Configurable Software Verification, Proc. CAV, pp.184-190, 2011.
DOI : 10.1007/978-3-540-31980-1_40
URL : http://www.sosy-lab.org/%7Edbeyer/Publications/2011-CAV.CPAchecker_A_Tool_for_Configurable_Software_Verification.pdf

D. Beyer and S. Löwe, Explicit-State Software Model Checking Based on CEGAR and Interpolation, Proc. FASE, pp.146-162, 2013.
DOI : 10.1007/978-3-642-37057-1_11
URL : http://www.sosy-lab.org/~dbeyer/Publications/2013-FASE.Explicit-State_Software_Model_Checking_Based_on_CEGAR_and_Interpolation.pdf

D. Beyer, S. Löwe, and P. Wendler, Domain-type-guided refinement selection based on sliced path prefixes, 2015.

D. Beyer and A. K. Petrenko, Linux driver verification, Proc. ISoLA, pp.1-6, 2012.
DOI : 10.15514/ispras-2012-23-23

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A static analyzer for large safety-critical software, Proc. PLDI, pp.196-207, 2003.
DOI : 10.1145/781151.781153
URL : https://hal.archives-ouvertes.fr/hal-00128135

E. M. 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

W. Craig, Linear reasoning. A new form of the Herbrand-Gentzen theorem, The Journal of Symbolic Logic, vol.39, issue.03, pp.250-268, 1957.
DOI : 10.2307/2963593

V. D. Silva, D. Kröning, M. Purandare, and G. Weissenbacher, Interpolant strength, Proc. VMCAI, pp.129-145, 2010.

S. Graf and H. Saïdi, Construction of abstract state graphs with PVS, Proc. CAV, 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, Proc. POPL, pp.232-244, 2004.

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy abstraction, Proc. POPL, pp.58-70, 2002.

R. Jhala and R. Majumdar, Path slicing, Proc. PLDI, pp.38-47, 2005.
DOI : 10.1145/1065010.1065016

P. Rümmer and P. Subotic, Exploring interpolants, 2013 Formal Methods in Computer-Aided Design, pp.69-76, 2013.
DOI : 10.1109/FMCAD.2013.6679393