@inproceedings(SVCOMP16,
 author       = {D. Beyer},
 year         = {2016},
 title        = {Reliable and Reproducible Competition Results with {{\sc BenchExec}} and Witnesses},
 booktitle    = {Proc.\ TACAS},
 publisher    = {Springer},
 pages        = {887--904},
 doi          = {10.1007/978-3-662-49674-9_55},
 url          = {http://www.sosy-lab.org/~dbeyer/Publications/2016-TACAS.Reliable_and_Reproducible_Competition_Results_with_BenchExec_and_Witnesses.pdf},
)
@article(BLAST,
 author       = {D. Beyer and T. A. Henzinger and R. Jhala and R. Majumdar},
 year         = {2007},
 title        = {The Software Model Checker {{\textsc{Blast}}}},
 journal      = {Int.\ J.\ Softw.\ Tools Technol.\ Transfer},
 volume       = {9},
 number       = {5-6},
 pages        = {505--525},
 doi          = {10.1007/s10009-007-0044-z},
 url          = {http://www.sosy-lab.org/~dbeyer/Publications/2007-STTT.The_Software_Model_Checker_BLAST.pdf},
)
@inproceedings(CPA,
 author       = {D. Beyer and T. A. Henzinger and G. Th{\'e}oduloz},
 year         = {2007},
 title        = {Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis},
 booktitle    = {Proc.\ CAV},
 series       = {LNCS~4590},
 publisher    = {Springer},
 pages        = {504--518},
 doi          = {10.1007/978-3-540-73368-3_51},
 url          = {http://www.sosy-lab.org/~dbeyer/Publications/2007-CAV.Configurable_Software_Verification.pdf},
)
@inproceedings(CPACHECKER,
 author       = {D. Beyer and M. E. Keremoglu},
 year         = {2011},
 title        = {{\textsc{CPAchecker}}: A Tool for Configurable Software Verification},
 booktitle    = {Proc.\ CAV},
 series       = {LNCS~6806},
 publisher    = {Springer},
 pages        = {184--190},
 doi          = {10.1007/978-3-642-22110-1_16},
 url          = {http://www.sosy-lab.org/~dbeyer/Publications/2011-CAV.CPAchecker_A_Tool_for_Configurable_Software_Verification.pdf},
)
@inproceedings(CPAexplicit,
 author       = {D. Beyer and S. L{\"o}we},
 year         = {2013},
 title        = {Explicit-State Software Model Checking Based on {CEGAR} and Interpolation},
 booktitle    = {Proc.\ FASE},
 series       = {LNCS~7793},
 publisher    = {Springer},
 pages        = {146--162},
 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},
)
@inproceedings(CPABDD,
 author       = {D. Beyer and A. Stahlbauer},
 year         = {2013},
 title        = {{BDD}-Based Software Model Checking with {\textsc{CPAchecker}}},
 booktitle    = {Proc.\ MEMICS},
 series       = {LNCS~7721},
 publisher    = {Springer},
 pages        = {1--11},
 doi          = {10.1007/978-3-642-36046-6_1},
 url          = {http://www.sosy-lab.org/~dbeyer/Publications/2013-MEMICS.BDD-Based_Software_Model_Checking_with_CPAchecker.pdf},
)
@article(ClarkeCEGAR,
 author       = {E. M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith},
 year         = {2003},
 title        = {Counterexample-guided abstraction refinement for symbolic model checking},
 journal      = {J. ACM},
 volume       = {50},
 number       = {5},
 pages        = {752--794},
 doi          = {10.1145/876638.876643},
)
@inproceedings(SATABS,
 author       = {E. M. Clarke and Kr\IeC{\"o}ning, D. and N. Sharygina and K. Yorav},
 year         = {2005},
 title        = {\textsc{SatAbs}: {SAT}-Based Predicate Abstraction for {ANSI-C}},
 booktitle    = {Proc.\ TACAS},
 series       = {LNCS~3440},
 publisher    = {Springer},
 pages        = {570--574},
 doi          = {10.1007/978-3-540-31980-1_40},
)
@inproceedings(CordeiroF11ESBMC,
 author       = {L. Cordeiro and B. Fischer},
 year         = {2011},
 title        = {Verifying multi-threaded software using smt-based context-bounded model checking},
 booktitle    = {Proc.\ ICSE},
 publisher    = {{ACM}},
 pages        = {331--340},
 doi          = {10.1145/1985793.1985839},
)
@inproceedings(CPACHECKER-COMP15,
 author       = {Matthias Dangl and L\IeC{\"o}we, Stefan and Philipp Wendler},
 year         = {2015},
 title        = {{\textsc{CPAchecker}} with Support for Recursive Programs and Floating-Point Arithmetic},
 booktitle    = {Proc.\ TACAS},
 series       = {LNCS~9035},
 publisher    = {Springer},
 pages        = {423--425},
 doi          = {10.1007/978-3-662-46681-0_34},
)
@inproceedings(CSEQ-COMP13,
 author       = {B. Fischer and O. Inverso and G. Parlato},
 year         = {2013},
 title        = {{CSeq}: {A} Sequentialization Tool for C (Competition Contribution)},
 booktitle    = {Proc.\ TACAS},
 series       = {LNCS~7795},
 publisher    = {Springer},
 pages        = {616--618},
 doi          = {10.1007/978-3-642-36742-7_46},
)
@book(Godefroid96POR,
 author       = {Patrice Godefroid},
 year         = {1996},
 title        = {Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem},
 series       = {LNCS~1032},
 publisher    = {Springer},
 doi          = {10.1007/3-540-60761-7},
)
@inproceedings(THREADER,
 author       = {A. Gupta and C. Popeea and A. Rybalchenko},
 year         = {2011},
 title        = {Threader: A Constraint-Based Verifier for Multi-threaded Programs},
 booktitle    = {CAV},
 series       = {LNCS~6806},
 publisher    = {Springer},
 pages        = {412--417},
 doi          = {10.1007/978-3-642-22110-1_32},
)
@inproceedings(LazyAbstraction,
 author       = {T. A. Henzinger and R. Jhala and R. Majumdar and G. Sutre},
 year         = {2002},
 title        = {Lazy abstraction},
 booktitle    = {Proc.\ POPL},
 publisher    = {ACM},
 pages        = {58--70},
 doi          = {10.1145/503272.503279},
)
@article(SPIN,
 author       = {G. J. Holzmann},
 year         = {1997},
 title        = {The {\textsc{Spin}} Model Checker},
 journal      = {IEEE Trans.\ Softw.\ Eng.},
 volume       = {23},
 number       = {5},
 pages        = {279--295},
 doi          = {10.1109/32.588521},
)
@inproceedings(Inverso15LazyCSeq,
 author       = {Omar Inverso and Truc L. Nguyen and Bernd Fischer and {La Torre}, Salvatore and Gennaro Parlato},
 year         = {2015},
 title        = {Lazy-CSeq: {A} Context-Bounded Model Checking Tool for Multi-threaded C-Programs},
 booktitle    = {Proc.\ ASE},
 publisher    = {{ACM}},
 pages        = {807--812},
 doi          = {10.1109/ASE.2015.108},
)
@article(IsloorM80Deadlock,
 author       = {Sreekaanth S. Isloor and T. Anthony Marsland},
 year         = {1980},
 title        = {The Deadlock Problem: An Overview},
 journal      = {{IEEE} Computer},
 volume       = {13},
 number       = {9},
 pages        = {58--78},
 doi          = {10.1109/MC.1980.1653786},
)
@inproceedings(Peled93POR,
 author       = {Doron A. Peled},
 year         = {1993},
 title        = {All from One, One for All: on Model Checking Using Representatives},
 booktitle    = {Proc.\ CAV},
 series       = {LNCS~697},
 publisher    = {Springer},
 pages        = {409--423},
 doi          = {10.1007/3-540-56922-7_34},
)
@inproceedings(Valmari89POR,
 author       = {Antti Valmari},
 year         = {1989},
 title        = {Stubborn sets for reduced state space generation},
 booktitle    = {Proc.\ Petri Nets},
 series       = {LNCS~483},
 publisher    = {Springer},
 pages        = {491--515},
 doi          = {10.1007/3-540-53863-1_36},
)