Document Open Access Logo

Matching mu-Logic: Foundation of K Framework (Invited Paper)

Authors Xiaohong Chen, Grigore Roşu

PDF

File

Thumbnail PDF
PDF
LIPIcs.CALCO.2019.1.pdf
  • Filesize: 466 kB
  • 4 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Xiaohong Chen
  • University of Illinois at Urbana-Champaign, USA
Grigore Roşu
  • University of Illinois at Urbana-Champaign, USA

References

  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. Google Scholar
  2. 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. Google Scholar
  3. Xiaohong Chen and Grigore Roşu. Matching μ-logic. Technical report, University of Illinois at Urbana-Champaign, 2019. URL: http://hdl.handle.net/2142/102281.
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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.
  7. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. Grigore Roşu. Matching logic. Logical Methods in Computer Science, 13(4):1-61, 2017. Google Scholar
  11. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact