@incollection(foctl,
 author       = "J{\"u}rgen Bohn and Werner Damm and Orna Grumberg and Hardi Hungar and Karen Laster",
 year         = "1998",
 title        = "First-Order-CTL Model Checking",
 editor       = "Vikraman Arvind and Sundar Ramanujam",
 booktitle    = "Foundations of Software Technology and Theoretical Computer Science",
 series       = "Lecture Notes in Computer Science",
 volume       = "1530",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "283--294",
 doi          = "10.1007/978-3-540-49382-2\_27",
)
@article(clarkemc,
 author       = "E. M. Clarke and E. A. Emerson and A. P. Sistla",
 year         = "1986",
 title        = "Automatic verification of finite-state concurrent systems using temporal logic specifications",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "8",
 pages        = "244--263",
 doi          = "10.1145/5397.5399",
)
@article(logiccomp,
 author       = "He Jifeng and Jonathan Bowen",
 year         = "1994",
 title        = "Specification, Verification and Prototyping of an Optimized Compiler",
 journal      = "Formal Aspects of Computing",
 volume       = "6",
 number       = "6",
 pages        = "643--658",
 doi          = "10.1007/BF03259390",
)
@article(kalvala,
 author       = "Sara Kalvala and Richard Warburton and David Lacey",
 year         = "2009",
 title        = "Program transformations using temporal logic side conditions",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "31",
 number       = "4",
 pages        = "1--48",
 doi          = "10.1145/1516507.1516509",
)
@article(tcfg,
 author       = "Jens Krinke",
 year         = "2003",
 title        = "Context-sensitive slicing of concurrent programs",
 journal      = "{SIGSOFT} Softw. Eng. Notes",
 volume       = "28",
 number       = "5",
 pages        = "178--187",
 doi          = "10.1145/949952.940096",
)
@article(lacey,
 author       = "David Lacey and Neil D. Jones and Eric Van Wyk and Carl Christian Frederiksen",
 year         = "2002",
 title        = "Proving correctness of compiler optimizations by temporal logic",
 journal      = "SIGPLAN Not.",
 volume       = "37",
 number       = "1",
 pages        = "283--294",
 doi          = "10.1145/565816.503299",
)
@inproceedings(llvm,
 author       = "C. Lattner and V. Adve",
 year         = "2004",
 title        = "LLVM: a compilation framework for lifelong program analysis transformation",
 booktitle    = "Code Generation and Optimization, 2004. CGO 2004. International Symposium on",
 pages        = "75--86",
 doi          = "10.1109/CGO.2004.1281665",
)
@article(cobalt,
 author       = "Sorin Lerner and Todd Millstein and Craig Chambers",
 year         = "2003",
 title        = "Automatically proving the correctness of compiler optimizations",
 journal      = "SIGPLAN Not.",
 volume       = "38",
 pages        = "220--231",
 doi          = "10.1145/780822.781156",
)
@article(compcert,
 author       = "Xavier Leroy",
 year         = "2009",
 title        = "A Formally Verified Compiler Back-end",
 journal      = "J. Autom. Reason.",
 volume       = "43",
 number       = "4",
 pages        = "363--446",
 doi          = "10.1007/s10817-009-9155-4",
)
@article(conccsmith,
 author       = "Robin Morisset and Pankaj Pawan and Francesco Zappa Nardelli",
 year         = "2013",
 title        = "Compiler Testing via a Theory of Sound Optimisations in the C11/C++11 Memory Model",
 journal      = "SIGPLAN Not.",
 volume       = "48",
 number       = "6",
 pages        = "187--196",
 doi          = "10.1145/2499370.2491967",
)
@incollection(z3,
 author       = "Leonardo Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "Z3: An Efficient SMT Solver",
 editor       = "C.R. Ramakrishnan and Jakob Rehof",
 booktitle    = "Tools and Algorithms for the Construction and Analysis of Systems",
 series       = "Lecture Notes in Computer Science",
 volume       = "4963",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "337--340",
 doi          = "10.1007/978-3-540-78800-3\_24",
)
@article(isabelle,
 author       = "Lawrence C. Paulson",
 year         = "1993",
 title        = "Isabelle: The Next 700 Theorem Provers",
 journal      = "CoRR",
 volume       = "cs.LO/9301106",
 url          = "http://arxiv.org/abs/cs.LO/9301106",
)
@article(koverview,
 author       = "Grigore Ro{\c s}u and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a}",
 year         = "2010",
 title        = "An Overview of the {K} Semantic Framework",
 journal      = "Journal of Logic and Algebraic Programming",
 volume       = "79",
 number       = "6",
 pages        = "397--434",
 doi          = "10.1016/j.jlap.2010.03.012",
)
@article(conccompcert,
 author       = "Jaroslav \^{S}ev\v {c}ik and Viktor Vafeiadis and Francesco Zappa Nardelli and Suresh Jagannathan and Peter Sewell",
 year         = "2011",
 title        = "Relaxed-memory concurrency and verified compilation",
 journal      = "SIGPLAN Not.",
 volume       = "46",
 number       = "1",
 pages        = "43--54",
 doi          = "10.1145/1925844.1926393",
)
@book(fsharp,
 author       = "Don Syme and Adam Granicz and Antonio Cisternino",
 year         = "2012",
 title        = "Expert F\# 3.0",
 edition      = "3rd",
 publisher    = "Apress",
 address      = "Berkely, CA, USA",
 doi          = "10.1007/978-1-4302-4651-0",
)
@article(csmith,
 author       = "Xuejun Yang and Yang Chen and Eric Eide and John Regehr",
 year         = "2011",
 title        = "Finding and understanding bugs in C compilers",
 journal      = "SIGPLAN Not.",
 volume       = "46",
 number       = "6",
 pages        = "283--294",
 doi          = "10.1145/1993316.1993532",
)