Matching mu-Logic: Foundation of K Framework (Invited Paper)
K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching mu-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, and reachability logic.
Matching mu-logic
Program verification
Reachability logic
Theory of computation~Logic
1:1-1:4
Invited Paper
Xiaohong
Chen
Xiaohong Chen
University of Illinois at Urbana-Champaign, USA
http://fsl.cs.illinois.edu/~xchen
Grigore
Roşu
Grigore Roşu
University of Illinois at Urbana-Champaign, USA
http://fsl.cs.illinois.edu/~grosu
10.4230/LIPIcs.CALCO.2019.1
Denis Bogdănaş and Grigore Roşu. K-Java: A complete semantics of Java. In Proceedings of the 42superscriptnd Symposium on Principles of Programming Languages (POPL'15), pages 445-456. ACM, 2015.
Xiaohong Chen and Grigore Roşu. Matching μ-logic. In Proceedings of the 34superscriptth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'19), 2019.
Xiaohong Chen and Grigore Roşu. Matching μ-logic. Technical report, University of Illinois at Urbana-Champaign, 2019. URL: http://hdl.handle.net/2142/102281.
http://hdl.handle.net/2142/102281
Andrei Ştefănescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Roşu. Semantics-based program verifiers for all languages. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'16), pages 74-91. ACM, 2016.
Chris Hathhorn, Chucky Ellison, and Grigore Roşu. Defining the undefinedness of C. In Proceedings of the 36superscriptth annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), pages 336-345. ACM, 2015.
Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, Brandon Moore, Yi Zhang, Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KEVM: A complete semantics of the Ethereum virtual machine. In Proceedings of the 2018 IEEE Computer Security Foundations Symposium (CSF'18). IEEE, 2018. URL: http://jellopaper.org.
http://jellopaper.org
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969.
Dexter Kozen. Results on the propositional μ-calculus. In Proceedings of the 9superscriptth International Colloquium on Automata, Languages and Programming (ICALP'82), pages 348-359. Springer, 1982.
Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KJS: A complete formal semantics of JavaScript. In Proceedings of the 36superscriptth annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), pages 346-356. ACM, 2015.
Grigore Roşu. Matching logic. Logical Methods in Computer Science, 13(4):1-61, 2017.
Grigore Roşu, Andrei Ştefănescu, Ştefan Ciobâcă, and Brandon M. Moore. One-path reachability logic. In Proceedings of the 28superscriptth Symposium on Logic in Computer Science (LICS'13), pages 358-367. IEEE, 2013.
Xiaohong Chen and Grigore Roşu
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode