Proving correctness of compiler optimizations by temporal logic

DOI10.1145/503272.503299zbMath1323.68380OpenAlexW2065635796MaRDI QIDQ5178913

Carl Christian Frederiksen, Neil D. Jones, Eric Van Wyk, David Lacey

Publication date: 17 March 2015

Published in: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11299/217345

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Silver: an extensible attribute grammar system, Generalising the array split obfuscation, A formally verified compiler back-end, Imperative-program transformation by instrumented-interpreter specialization, Internal and External Logics of Abstract Interpretations, Inter-program Properties