@book(DragonBook,
 author       = {Alfred V. Aho and Ravi Sethi and Jeffrey D. Ullman},
 year         = {1986},
 title        = {Compilers: Principles, Techniques, and Tools},
 publisher    = {Addison-Wesley Longman Publishing Co., Inc.},
 address      = {Boston, MA, USA},
)
@article(SLAM,
 author       = {Thomas Ball and Sriram K. Rajamani},
 year         = {2002},
 title        = {The {SLAM} Project: Debugging System Software via Static Analysis},
 journal      = {SIGPLAN Not.},
 volume       = {37},
 number       = {1},
 pages        = {1--3},
 doi          = {10.1145/565816.503274},
)
@incollection(Beyer16,
 author       = {Dirk Beyer},
 year         = {2016},
 title        = {Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on {SV-COMP} 2016)},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {9636},
 publisher    = {Springer},
 pages        = {887--904},
 doi          = {10.1007/978-3-662-49674-9_55},
)
@inproceedings(Beyer09,
 author       = {Dirk Beyer and Alessandro Cimatti and Alberto Griggio and M. Erkan Keremoglu and Roberto Sebastiani},
 year         = {2009},
 title        = {Software model checking via large-block encoding},
 booktitle    = {Proceedings of the 2009 Conference on Formal Methods in Computer-Aided Design},
 publisher    = {IEEE},
 pages        = {25--32},
 doi          = {10.1109/FMCAD.2009.5351147},
)
@incollection(Beyer16smt,
 author       = {Dirk Beyer and Matthias Dangl},
 year         = {2016},
 title        = {{SMT}-based Software Model Checking: An Experimental Comparison of Four Algorithms},
 booktitle    = {Verified Software. Theories, Tools, and Experiments},
 series       = {Lecture Notes in Computer Science},
 volume       = {9971},
 publisher    = {Springer},
 pages        = {181--198},
 doi          = {10.1007/978-3-319-48869-1_14},
)
@article(Blast,
 author       = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
 year         = {2007},
 title        = {The software model checker {B}last},
 journal      = {International Journal on Software Tools for Technology Transfer},
 volume       = {9},
 number       = {5},
 pages        = {505--525},
 doi          = {10.1007/s10009-007-0044-z},
)
@incollection(CPAChecker,
 author       = {Dirk Beyer and Thomas A. Henzinger and Gr{\'e}gory Th{\'e}oduloz},
 year         = {2007},
 title        = {Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {4590},
 publisher    = {Springer},
 pages        = {504--518},
 doi          = {10.1007/978-3-540-73368-3_51},
)
@incollection(Beyer15refinement,
 author       = {Dirk Beyer and Stefan L{\"o}we and Philipp Wendler},
 year         = {2015},
 title        = {Refinement Selection},
 booktitle    = {Model Checking Software: 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9232},
 publisher    = {Springer},
 pages        = {20--38},
 doi          = {10.1007/978-3-319-23404-5_3},
)
@article(Binkley07,
 author       = {David Binkley and Nicolas Gold and Mark Harman},
 year         = {2007},
 title        = {An Empirical Study of Static Program Slice Size},
 journal      = {ACM Transactions on Software Engineering and Methodology},
 volume       = {16},
 number       = {2},
 doi          = {10.1145/1217295.1217297},
)
@article(SLAB,
 author       = {Ingo Br\"{u}ckner and Klaus Dr\"{a}ger and Bernd Finkbeiner and Heike Wehrheim},
 year         = {2008},
 title        = {Slicing Abstractions},
 journal      = {Fundamenta Informaticae},
 volume       = {89},
 number       = {4},
 pages        = {369--392},
)
@article(clarke03,
 author       = {Edmund Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},
 year         = {2003},
 title        = {Counterexample-guided abstraction refinement for symbolic model checking},
 journal      = {Journal of the ACM},
 volume       = {50},
 number       = {5},
 pages        = {752--794},
 doi          = {10.1145/876638.876643},
)
@article(clarke04,
 author       = {Edmund Clarke and Anubhav Gupta and Ofer Strichman},
 year         = {2004},
 title        = {{SAT}-based counterexample-guided abstraction refinement},
 journal      = {IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems},
 volume       = {23},
 number       = {7},
 pages        = {1113--1123},
 doi          = {10.1109/TCAD.2004.829807},
)
@incollection(SATABS,
 author       = {Edmund Clarke and Daniel Kroening and Natasha Sharygina and Karen Yorav},
 year         = {2005},
 title        = {{SATABS}: {SAT}-Based Predicate Abstraction for {ANSI-C}},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {3440},
 publisher    = {Springer},
 pages        = {570--574},
 doi          = {10.1007/978-3-540-31980-1_40},
)
@article(Ferrante87,
 author       = {Jeanne Ferrante and Karl J. Ottenstein and Joe D. Warren},
 year         = {1987},
 title        = {The Program Dependence Graph and Its Use in Optimization},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {9},
 number       = {3},
 pages        = {319--349},
 doi          = {10.1145/24039.24041},
)
@incollection(graf97,
 author       = {Susanne Graf and Hassen Saidi},
 year         = {1997},
 title        = {Construction of abstract state graphs with {PVS}},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {1254},
 publisher    = {Springer},
 pages        = {72--83},
 doi          = {10.1007/3-540-63166-6_10},
)
@incollection(forte2016,
 author       = {\'Akos Hajdu and Tam\'as T\'oth and Andr\'as V\"or\"os and Istv\'an Majzik},
 year         = {2016},
 title        = {A Configurable {CEGAR} Framework with Interpolation-based Refinements},
 booktitle    = {Formal Techniques for Distributed Objects, Components and Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {9688},
 publisher    = {Springer},
 pages        = {158--174},
 doi          = {10.1007/978-3-319-39570-8_11},
)
@article(Horwitz90,
 author       = {Susan Horwitz and Thomas Reps and David Binkley},
 year         = {1990},
 title        = {Interprocedural Slicing Using Dependence Graphs},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {12},
 number       = {1},
 pages        = {26--60},
 doi          = {10.1145/77606.77608},
)
@incollection(Kumar15,
 author       = {Shrawan Kumar and Amitabha Sanyal and Uday P. Khedker},
 year         = {2015},
 title        = {Value Slice: A New Slicing Concept for Scalable Property Checking},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {9035},
 publisher    = {Springer},
 pages        = {101--115},
 doi          = {10.1007/978-3-662-46681-0_7},
)
@inproceedings(LLVM,
 author       = {Chris Lattner and Vikram Adve},
 year         = {2004},
 title        = {{LLVM}: A Compilation Framework for Lifelong Program Analysis \& Transformation},
 booktitle    = {Proceedings of the 2004 International Symposium on Code Generation and Optimization},
 publisher    = {IEEE},
 pages        = {75--86},
)
@inproceedings(leucker15,
 author       = {Martin Leucker and Grigory Markin and Neuh\"au{\ss}er, Martin R.},
 year         = {2015},
 title        = {A New Refinement Strategy for {CEGAR}-Based Industrial Model Checking},
 booktitle    = {Hardware and Software: Verification and Testing},
 series       = {Lecture Notes in Computer Science},
 volume       = {9434},
 publisher    = {Springer},
 pages        = {155--170},
 doi          = {10.1007/978-3-319-26287-1_10},
)
@incollection(mcmillan05,
 author       = {Kenneth L. McMillan},
 year         = {2005},
 title        = {Applications of {C}raig Interpolants in Model Checking},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {3440},
 publisher    = {Springer},
 pages        = {1--12},
 doi          = {10.1007/978-3-540-31980-1_1},
)
@inproceedings(Sridharan07,
 author       = {Manu Sridharan and Stephen J. Fink and Rastislav Bodik},
 year         = {2007},
 title        = {Thin Slicing},
 booktitle    = {Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 publisher    = {ACM},
 pages        = {112--122},
)
@inproceedings(vizel09,
 author       = {Yakir Vizel and Orna Grumberg},
 year         = {2009},
 title        = {Interpolation-sequence based model checking},
 booktitle    = {Proceedings of the 2009 Conference on Formal Methods in Computer-Aided Design},
 organization = {IEEE},
 pages        = {1--8},
 doi          = {10.1109/FMCAD.2009.5351148},
)
@inproceedings(Weiser81,
 author       = {Mark Weiser},
 year         = {1981},
 title        = {Program Slicing},
 booktitle    = {Proceedings of the 5th International Conference on Software Engineering},
 publisher    = {IEEE},
 pages        = {439--449},
)