@inproceedings(Banda2010CAS,
 author       = {Gourinath Banda and John P. Gallagher},
 year         = {2010},
 title        = {Constraint-based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation},
 booktitle    = {Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
 series       = {LPAR'10},
 doi          = {10.1007/978-3-642-17511-4\_3},
)
@inproceedings(ehsf,
 author       = {Tewodros A. Beyene and Corneliu Popeea and Andrey Rybalchenko},
 year         = {2013},
 title        = {Solving Existentially Quantified Horn Clauses},
 booktitle    = {Proceedings of the 25th International Conference on Computer Aided Verification},
 series       = {CAV'13},
 doi          = {10.1007/978-3-642-39799-8\_61},
)
@article(Bradley05polyrankingfor,
 author       = {Aaron R. Bradley and Zohar Manna and Henny B. Sipma},
 year         = {2005},
 title        = {Polyranking for Polynomial Loops},
 journal      = {Automata, Languages and Programming},
 pages        = {1349--1361},
)
@inproceedings(Burch1990,
 author       = {J.R. Burch and E.M. Clarke and K.L. McMillan and D.L. Dill and L.J. Hwang},
 year         = {1990},
 title        = {Symbolic model checking: 10$^{20}$ states and beyond},
 doi          = {10.1016/0890-5401(92)90017-A},
)
@inproceedings(Chaki2005,
 author       = {Sagar Chaki and Edmund M. Clarke and Orna Grumberg and Joël Ouaknine and Natasha Sharygina and Tayssir Touili and Helmut Veith},
 year         = {2005},
 title        = {State/Event Software Verification for Branching-Time Specifications.},
 booktitle    = {IFM},
 volume       = {3771},
 publisher    = {Springer},
 pages        = {53--69},
 doi          = {10.1007/11589976\_5},
)
@inproceedings(Clarke1983AVF,
 author       = {E. M. Clarke and E. A. Emerson and A. P. Sistla},
 year         = {1983},
 title        = {Automatic Verification of Finite State Concurrent System Using Temporal Logic Specifications: A Practical Approach},
 booktitle    = {Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
 series       = {POPL '83},
 doi          = {10.1145/567067.567080},
)
@inproceedings(Clarke02treelikeCEX,
 author       = {Edmund Clarke and Yuan Lu and Broadcom Com and Helmut Veith and Somesh Jha},
 year         = {2002},
 title        = {Tree-Like Counterexamples in Model Checking},
 booktitle    = {In Proceedings of the 17 th Annual IEEE Symposium on Logic in Computer Science (LICS’02)},
 publisher    = {IEEE Computer Society},
 doi          = {10.1109/LICS.2002.1029814},
)
@inproceedings(Clarke1990TLM,
 author       = {Edmund M. Clarke},
 year         = {1991},
 title        = {Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem},
 series       = {CAV '90},
)
@inproceedings(Cook2014FTR,
 author       = {Byron Cook and Heidy Khlaaf and Nir Piterman},
 year         = {2014},
 title        = {Faster Temporal Reasoning for Infinite-State Programs},
 doi          = {10.1109/FMCAD.2014.6987598},
)
@inproceedings(CookPLDI13,
 author       = {Byron Cook and Eric Koskinen},
 year         = {2013},
 title        = {Reasoning about Nondeterminism in Programs},
 booktitle    = {PLDI},
 doi          = {10.1145/2491956.2491969},
)
@article(Cook2012TPV,
 author       = {Byron Cook and Eric Koskinen and Moshe Vardi},
 year         = {2012},
 title        = {Temporal Property Verification As a Program Analysis Task},
 journal      = {Form. Methods Syst. Des.},
 doi          = {10.1007/s10703-012-0153-5},
)
@inproceedings(TerminatorPLDI06,
 author       = {Byron Cook and Andreas Podelski and Andrey Rybalchenko},
 year         = {2006},
 title        = {Termination proofs for systems code},
 booktitle    = {PLDI},
 doi          = {10.1145/1133981.1134029},
)
@article(Demri2010checkingctl,
 author       = {St\'ephane Demri and Alain Finkel and Valentin Goranko Govert and Van Drimmelen},
 year         = {2010},
 title        = {Model checking CTL* over flat Presburger counter systems},
 journal      = {JANCL},
 doi          = {10.3166/jancl.20.313-344},
)
@incollection(Emerson1991TM,
 author       = {E. Allen Emerson},
 year         = {1990},
 title        = {Handbook of Theoretical Computer Science (Vol. B)},
 chapter      = {Temporal and Modal Logic},
)
@inproceedings(Emerson1996,
 author       = {E. Allen Emerson and Kedar S. Namjoshi},
 year         = {1996},
 title        = {Automatic Verification of Parameterized Synchronous Systems (Extended Abstract)},
 booktitle    = {Proceedings of the 8th International Conference on Computer Aided Verification},
 series       = {CAV '96},
 doi          = {10.1007/3-540-61474-5\_60},
)
@inproceedings(GrebenshchikovTACAS12,
 author       = {Sergey Grebenshchikov and Ashutosh Gupta and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko},
 year         = {2012},
 title        = {{HSF(C)}: A Software Verifier Based on {H}orn Clauses},
 booktitle    = {TACAS},
 doi          = {10.1007/978-3-642-28756-5\_46},
)
@inproceedings(TNTPOPL08,
 author       = {Ashutosh Gupta and Thomas A. Henzinger and Rupak Majumdar and Andrey Rybalchenko and Ru-Gang Xu},
 year         = {2008},
 title        = {Proving non-termination},
 booktitle    = {POPL},
 doi          = {10.1145/1328438.1328459},
)
@inproceedings(GurfinkelWC06,
 author       = {Arie Gurfinkel and Ou Wei and Marsha Chechik},
 year         = {2006},
 title        = {Yasm: A Software Model-Checker for Verification and Refutation.},
 editor       = {Thomas Ball and Robert B. Jones},
 booktitle    = {CAV},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer},
 pages        = {170--174},
 doi          = {10.1007/11817963\_18},
)
@inproceedings(Hassan2012IIC,
 author       = {Zyad Hassan and Aaron R. Bradley and Fabio Somenzi},
 year         = {2012},
 title        = {Incremental, Inductive CTL Model Checking},
 booktitle    = {Proceedings of the 24th International Conference on Computer Aided Verification},
 doi          = {10.1007/978-3-642-31424-7\_38},
)
@inproceedings(muz,
 author       = {Krystof Hoder and Bj{\o}rner, Nikolaj and Leonardo de Moura},
 year         = {2011},
 title        = {{$\mu$Z}- An Efficient Engine for Fixed Points with Constraints},
 booktitle    = {CAV},
 doi          = {10.1007/978-3-642-22110-1\_36},
)
@article(KestenTCS95,
 author       = {Yonit Kesten and Amir Pnueli},
 year         = {2005},
 title        = {A compositional approach to {CTL}* verification},
 journal      = {Theor. Comput. Sci.},
 volume       = {331},
 number       = {2-3},
 pages        = {397--428},
 doi          = {10.1016/j.tcs.2004.09.023},
)
@article(Kupferman2000,
 author       = {Orna Kupferman and Moshe Y. Vardi and Pierre Wolper},
 year         = {2000},
 title        = {An Automata-theoretic Approach to Branching-time Model Checking},
 journal      = {J. ACM},
 doi          = {10.1145/333979.333987},
)
@book(Manna1992,
 author       = {Zohar Manna and Amir Pnueli},
 year         = {1992},
 title        = {The Temporal Logic of Reactive and Concurrent Systems},
 publisher    = {Springer-Verlag New York, Inc.},
 address      = {New York, NY, USA},
 doi          = {10.1007/978-1-4612-0931-7},
)
@book(McMillan1993SMC,
 author       = {Kenneth L. McMillan},
 year         = {1993},
 title        = {Symbolic Model Checking},
 doi          = {10.1007/978-1-4615-3190-6},
)
@article(Penczek2002BMC,
 author       = {Wojciech Penczek and Bozena Wozna and Andrzej Zbrzezny},
 year         = {2002},
 title        = {Bounded Model Checking for the Universal Fragment of CTL},
 journal      = {Fundam. Inf.},
)
@inproceedings(Pnueli1977,
 author       = {Amir Pnueli},
 year         = {1977},
 title        = {The Temporal Logic of Programs},
 booktitle    = {Proceedings of the 18th Annual Symposium on Foundations of Computer Science},
 doi          = {10.1109/SFCS.1977.32},
)
@inproceedings(Song2011,
 author       = {Fu Song and Tayssir Touili},
 year         = {2011},
 title        = {Efficient CTL model-checking for pushdown systems},
 booktitle    = {In CONCUR},
 doi          = {10.1007/978-3-642-23217-6\_29},
)
@inproceedings(Song2013,
 author       = {Fu Song and Tayssir Touili},
 year         = {2013},
 title        = {PoMMaDe: Pushdown Model-checking for Malware Detection},
 booktitle    = {Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering},
 publisher    = {ACM},
 doi          = {10.1007/978-3-642-28756-5\_9},
)
@inproceedings(Walukiewicz2000,
 author       = {Igor Walukiewicz},
 year         = {2000},
 title        = {Model Checking CTL Properties of Pushdown Systems.},
 booktitle    = {FSTTCS},
 series       = {Lecture Notes in Computer Science},
 doi          = {10.1007/3-540-44450-5\_10},
)
@article(walukiewicz2001pushdown,
 author       = {Igor Walukiewicz},
 year         = {2001},
 title        = {Pushdown processes: Games and model-checking},
 journal      = {Information and computation},
 doi          = {10.1007/3-540-61474-5\_58},
)