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

Comments and questions to:
For website issues: