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.
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.
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.
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.
Jens Krinke (2003):
Context-sensitive slicing of concurrent programs.
SIGSOFT Softw. Eng. Notes 28(5),
pp. 178–187,
doi:10.1145/949952.940096.
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.
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.
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.
Xavier Leroy (2009):
A Formally Verified Compiler Back-end.
J. Autom. Reason. 43(4),
pp. 363–446,
doi:10.1007/s10817-009-9155-4.
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.
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.
Lawrence C. Paulson (1993):
Isabelle: The Next 700 Theorem Provers.
CoRR cs.LO/9301106.
Available at http://arxiv.org/abs/cs.LO/9301106.
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.
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.
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.
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.
eptcs@eptcs.org