Search Results

Documents authored by Rosu, Grigore

Found 2 Possible Name Variants:

Rosu, Grigore

Document
DOI: 10.4230/DagRep.11.9.80
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

Authors: Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu

Published in: Dagstuhl Reports, Volume 11, Issue 9 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21431 "Rigorous Methods for Smart Contracts". Blockchain technologies have emerged as an exciting field for both researchers and practitioners focusing on formal guarantees for software. It is arguably a "once in a lifetime" opportunity for rigorous methods to be integrated in audit processes for parties deploying smart contracts, whether for fund raising, securities trading, or supply-chain management. Smart contracts are programs managing cryptocurrency accounts on a blockchain. Research in the area of smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is vibrant development of verification and program-analysis techniques that check the correctness of smart-contract code. Second, there are emerging designs of programming languages and methodologies for writing smart contracts such that they are more robust by construction or more amenable to analysis and verification. Programming-language abstraction layers expose low-level cryptographic primitives enabling developers to design high-level cryptographic protocols. Automated-reasoning mechanisms present a common underlying enabler; and the specific needs of the smart-contract world offer new challenges. This workshop brought together stakeholders in the aforementioned areas related to advancing reliable smart-contract technologies.
Cite as

Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu. Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). In Dagstuhl Reports, Volume 11, Issue 9, pp. 80-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{bjrner_et_al:DagRep.11.9.80,
  author =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  title =	{{Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)}},
  pages =	{80--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{9},
  editor =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.9.80},
  URN =		{urn:nbn:de:0030-drops-159198},
  doi =		{10.4230/DagRep.11.9.80},
  annote =	{Keywords: automated reasoning, cryptographic protocols, program verification, programming languages, smart contracts}
}
Document
Invited Talk
DOI: 10.4230/OASIcs.FMBC.2020.1
Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)

Authors: Grigore Rosu

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

Abstract
The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We will present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal language specification.
Cite as

Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{rosu:OASIcs.FMBC.2020.1,
  author =	{Rosu, Grigore},
  title =	{{Formal Design, Implementation and Verification of Blockchain Languages Using K}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{1:1--1:1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.1},
  URN =		{urn:nbn:de:0030-drops-134141},
  doi =		{10.4230/OASIcs.FMBC.2020.1},
  annote =	{Keywords: Blockchain, K Framework}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.1
Matching mu-Logic: Foundation of K Framework (Invited Paper)

Authors: Xiaohong Chen and Grigore Roşu

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

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

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)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CALCO.2019.1,
  author =	{Chen, Xiaohong and Ro\c{s}u, Grigore},
  title =	{{Matching mu-Logic: Foundation of K Framework}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{1:1--1:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.1},
  URN =		{urn:nbn:de:0030-drops-114296},
  doi =		{10.4230/LIPIcs.CALCO.2019.1},
  annote =	{Keywords: Matching mu-logic, Program verification, Reachability logic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2018.2
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk)

Authors: Grigore Rosu

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
This invited paper describes recent, ongoing and planned work on the use of the rewrite-based semantic framework K to formally design, implement and verify blockchain languages and virtual machines. Both academic and commercial endeavors are discussed, as well as thoughts and directions for future research and development.
Cite as

Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{rosu:LIPIcs.FSCD.2018.2,
  author =	{Rosu, Grigore},
  title =	{{Formal Design, Implementation and Verification of Blockchain Languages}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{2:1--2:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.2},
  URN =		{urn:nbn:de:0030-drops-91722},
  doi =		{10.4230/LIPIcs.FSCD.2018.2},
  annote =	{Keywords: Formal semantics, Program verification, Blockchain}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.RTA.2015.5
Matching Logic - Extended Abstract (Invited Talk)

Authors: Grigore Rosu

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers, but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have a rewrite-based operational semantics.
Cite as

Grigore Rosu. Matching Logic - Extended Abstract (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 5-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{rosu:LIPIcs.RTA.2015.5,
  author =	{Rosu, Grigore},
  title =	{{Matching Logic - Extended Abstract}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{5--21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.5},
  URN =		{urn:nbn:de:0030-drops-51859},
  doi =		{10.4230/LIPIcs.RTA.2015.5},
  annote =	{Keywords: Program logic, First-order logic, Rewriting, Verification}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.151
A Rewriting Logic Semantics Approach to Modular Program Analysis

Authors: Mark Hills and Grigore Rosu

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
The K framework, based on rewriting logic semantics, provides a powerful logic for defining the semantics of programming languages. While most work in this area has focused on defining an evaluation semantics for a language, it is also possible to define an abstract semantics that can be used for program analysis. Using the SILF language (Hills, Serbanuta and Rosu, 2007), this paper describes one technique for defining such a semantics: policy frameworks. In policy frameworks, an analysis-generic, modular framework is first defined for a language. Individual analyses, called policies, are then defined as extensions of this framework, with each policy defining analysis-specific semantic rules and an annotation language which, in combination with support in the language front-end, allows users to annotate program types and functions with information used during program analysis. Standard term rewriting techniques are used to analyze programs by evaluating them in the policy semantics.
Cite as

Mark Hills and Grigore Rosu. A Rewriting Logic Semantics Approach to Modular Program Analysis. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 151-160, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hills_et_al:LIPIcs.RTA.2010.151,
  author =	{Hills, Mark and Rosu, Grigore},
  title =	{{A Rewriting Logic Semantics Approach to Modular Program Analysis}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{151--160},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.151},
  URN =		{urn:nbn:de:0030-drops-26506},
  doi =		{10.4230/LIPIcs.RTA.2010.151},
  annote =	{Keywords: K, rewriting logic semantics, program analysis}
}
Document
DOI: 10.4230/DagSemProc.07011.1
07011 Abstracts Collection – Runtime Verification

Authors: Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky

Published in: Dagstuhl Seminar Proceedings, Volume 7011, Runtime Verification (2008)

Abstract
From January 2--6 2007 the Dagstuhl Seminar 07011 {\em `Runtime Verification'} was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar have been put together in this paper. The first section is an executive summary that describes the seminar topics in general.
Cite as

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Abstracts Collection – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.1,
  author =	{Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg},
  title =	{{07011 Abstracts Collection – Runtime Verification}},
  booktitle =	{Runtime Verification},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.1},
  URN =		{urn:nbn:de:0030-drops-13764},
  doi =		{10.4230/DagSemProc.07011.1},
  annote =	{Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented programming, test oracles, fault protection, dynamic specification learning, combining static and dynamic analysis}
}
Document
DOI: 10.4230/DagSemProc.07011.2
07011 Executive Summary – Runtime Verification

Authors: Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky

Published in: Dagstuhl Seminar Proceedings, Volume 7011, Runtime Verification (2008)

Abstract
From January 2 to January 6, 2007, the Dagstuhl Seminar 07011 "Runtime Verification" was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. Over the past few years, runtime verification has emerged as a focused subject in program analysis that bridges the gap between the complexity-haunted field of fully formal verification methods and the ad-hoc field of testing. Other terms for this subject are: program monitoring, dynamic program analysis, and runtime analysis. Thirty researchers participated in the seminar and discussed their recent work and recent trends in runtime verification.
Cite as

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Executive Summary – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.2,
  author =	{Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg},
  title =	{{07011 Executive Summary – Runtime Verification}},
  booktitle =	{Runtime Verification},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.2},
  URN =		{urn:nbn:de:0030-drops-13699},
  doi =		{10.4230/DagSemProc.07011.2},
  annote =	{Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented program}
}

Roşu, Grigore

Document
DOI: 10.4230/DagRep.11.9.80
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

Authors: Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu

Published in: Dagstuhl Reports, Volume 11, Issue 9 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21431 "Rigorous Methods for Smart Contracts". Blockchain technologies have emerged as an exciting field for both researchers and practitioners focusing on formal guarantees for software. It is arguably a "once in a lifetime" opportunity for rigorous methods to be integrated in audit processes for parties deploying smart contracts, whether for fund raising, securities trading, or supply-chain management. Smart contracts are programs managing cryptocurrency accounts on a blockchain. Research in the area of smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is vibrant development of verification and program-analysis techniques that check the correctness of smart-contract code. Second, there are emerging designs of programming languages and methodologies for writing smart contracts such that they are more robust by construction or more amenable to analysis and verification. Programming-language abstraction layers expose low-level cryptographic primitives enabling developers to design high-level cryptographic protocols. Automated-reasoning mechanisms present a common underlying enabler; and the specific needs of the smart-contract world offer new challenges. This workshop brought together stakeholders in the aforementioned areas related to advancing reliable smart-contract technologies.
Cite as

Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu. Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). In Dagstuhl Reports, Volume 11, Issue 9, pp. 80-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{bjrner_et_al:DagRep.11.9.80,
  author =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  title =	{{Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)}},
  pages =	{80--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{9},
  editor =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.9.80},
  URN =		{urn:nbn:de:0030-drops-159198},
  doi =		{10.4230/DagRep.11.9.80},
  annote =	{Keywords: automated reasoning, cryptographic protocols, program verification, programming languages, smart contracts}
}
Document
Invited Talk
DOI: 10.4230/OASIcs.FMBC.2020.1
Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)

Authors: Grigore Rosu

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

Abstract
The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We will present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal language specification.
Cite as

Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{rosu:OASIcs.FMBC.2020.1,
  author =	{Rosu, Grigore},
  title =	{{Formal Design, Implementation and Verification of Blockchain Languages Using K}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{1:1--1:1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.1},
  URN =		{urn:nbn:de:0030-drops-134141},
  doi =		{10.4230/OASIcs.FMBC.2020.1},
  annote =	{Keywords: Blockchain, K Framework}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.1
Matching mu-Logic: Foundation of K Framework (Invited Paper)

Authors: Xiaohong Chen and Grigore Roşu

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

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

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)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CALCO.2019.1,
  author =	{Chen, Xiaohong and Ro\c{s}u, Grigore},
  title =	{{Matching mu-Logic: Foundation of K Framework}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{1:1--1:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.1},
  URN =		{urn:nbn:de:0030-drops-114296},
  doi =		{10.4230/LIPIcs.CALCO.2019.1},
  annote =	{Keywords: Matching mu-logic, Program verification, Reachability logic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2018.2
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk)

Authors: Grigore Rosu

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
This invited paper describes recent, ongoing and planned work on the use of the rewrite-based semantic framework K to formally design, implement and verify blockchain languages and virtual machines. Both academic and commercial endeavors are discussed, as well as thoughts and directions for future research and development.
Cite as

Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{rosu:LIPIcs.FSCD.2018.2,
  author =	{Rosu, Grigore},
  title =	{{Formal Design, Implementation and Verification of Blockchain Languages}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{2:1--2:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.2},
  URN =		{urn:nbn:de:0030-drops-91722},
  doi =		{10.4230/LIPIcs.FSCD.2018.2},
  annote =	{Keywords: Formal semantics, Program verification, Blockchain}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.RTA.2015.5
Matching Logic - Extended Abstract (Invited Talk)

Authors: Grigore Rosu

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers, but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have a rewrite-based operational semantics.
Cite as

Grigore Rosu. Matching Logic - Extended Abstract (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 5-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{rosu:LIPIcs.RTA.2015.5,
  author =	{Rosu, Grigore},
  title =	{{Matching Logic - Extended Abstract}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{5--21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.5},
  URN =		{urn:nbn:de:0030-drops-51859},
  doi =		{10.4230/LIPIcs.RTA.2015.5},
  annote =	{Keywords: Program logic, First-order logic, Rewriting, Verification}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.151
A Rewriting Logic Semantics Approach to Modular Program Analysis

Authors: Mark Hills and Grigore Rosu

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
The K framework, based on rewriting logic semantics, provides a powerful logic for defining the semantics of programming languages. While most work in this area has focused on defining an evaluation semantics for a language, it is also possible to define an abstract semantics that can be used for program analysis. Using the SILF language (Hills, Serbanuta and Rosu, 2007), this paper describes one technique for defining such a semantics: policy frameworks. In policy frameworks, an analysis-generic, modular framework is first defined for a language. Individual analyses, called policies, are then defined as extensions of this framework, with each policy defining analysis-specific semantic rules and an annotation language which, in combination with support in the language front-end, allows users to annotate program types and functions with information used during program analysis. Standard term rewriting techniques are used to analyze programs by evaluating them in the policy semantics.
Cite as

Mark Hills and Grigore Rosu. A Rewriting Logic Semantics Approach to Modular Program Analysis. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 151-160, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hills_et_al:LIPIcs.RTA.2010.151,
  author =	{Hills, Mark and Rosu, Grigore},
  title =	{{A Rewriting Logic Semantics Approach to Modular Program Analysis}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{151--160},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.151},
  URN =		{urn:nbn:de:0030-drops-26506},
  doi =		{10.4230/LIPIcs.RTA.2010.151},
  annote =	{Keywords: K, rewriting logic semantics, program analysis}
}
Document
DOI: 10.4230/DagSemProc.07011.1
07011 Abstracts Collection – Runtime Verification

Authors: Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky

Published in: Dagstuhl Seminar Proceedings, Volume 7011, Runtime Verification (2008)

Abstract
From January 2--6 2007 the Dagstuhl Seminar 07011 {\em `Runtime Verification'} was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar have been put together in this paper. The first section is an executive summary that describes the seminar topics in general.
Cite as

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Abstracts Collection – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.1,
  author =	{Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg},
  title =	{{07011 Abstracts Collection – Runtime Verification}},
  booktitle =	{Runtime Verification},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.1},
  URN =		{urn:nbn:de:0030-drops-13764},
  doi =		{10.4230/DagSemProc.07011.1},
  annote =	{Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented programming, test oracles, fault protection, dynamic specification learning, combining static and dynamic analysis}
}
Document
DOI: 10.4230/DagSemProc.07011.2
07011 Executive Summary – Runtime Verification

Authors: Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky

Published in: Dagstuhl Seminar Proceedings, Volume 7011, Runtime Verification (2008)

Abstract
From January 2 to January 6, 2007, the Dagstuhl Seminar 07011 "Runtime Verification" was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. Over the past few years, runtime verification has emerged as a focused subject in program analysis that bridges the gap between the complexity-haunted field of fully formal verification methods and the ad-hoc field of testing. Other terms for this subject are: program monitoring, dynamic program analysis, and runtime analysis. Thirty researchers participated in the seminar and discussed their recent work and recent trends in runtime verification.
Cite as

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Executive Summary – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.2,
  author =	{Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg},
  title =	{{07011 Executive Summary – Runtime Verification}},
  booktitle =	{Runtime Verification},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7011},
  editor =	{Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.2},
  URN =		{urn:nbn:de:0030-drops-13699},
  doi =		{10.4230/DagSemProc.07011.2},
  annote =	{Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented program}
}
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact