LIPIcs.CALCO.2019.1.pdf
- Filesize: 466 kB
- 4 pages
Document
Matching mu-Logic: Foundation of K Framework (Invited Paper)
Authors
-
Part of:
Volume:
8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-11-25
Cite AsGet BibTex
Xiaohong Chen and Grigore Roşu. Matching mu-Logic: Foundation of K Framework (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CALCO.2019.1
https://doi.org/10.4230/LIPIcs.CALCO.2019.1
Abstract
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic
Keywords
- Matching mu-logic
- Program verification
- Reachability logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
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.
-
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.
-
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.