diff --git a/publications/chen-lucanu-rosu-2020-trb.pdf b/publications/chen-lucanu-rosu-2020-trb.pdf index 78c64a4..ca79c88 100644 Binary files a/publications/chen-lucanu-rosu-2020-trb.pdf and b/publications/chen-lucanu-rosu-2020-trb.pdf differ diff --git a/publications/chen-rosu-2020-icfp.pdf b/publications/chen-rosu-2020-icfp.pdf index be30b76..0fed417 100644 Binary files a/publications/chen-rosu-2020-icfp.pdf and b/publications/chen-rosu-2020-icfp.pdf differ diff --git a/publications/hildenbrandt-saxena-zhu-rodrigues-daian-guth-moore-zhang-park-rosu-2018-csf.pdf b/publications/hildenbrandt-saxena-zhu-rodrigues-daian-guth-moore-zhang-park-rosu-2018-csf.pdf index 4e5b372..3c958e9 100644 Binary files a/publications/hildenbrandt-saxena-zhu-rodrigues-daian-guth-moore-zhang-park-rosu-2018-csf.pdf and b/publications/hildenbrandt-saxena-zhu-rodrigues-daian-guth-moore-zhang-park-rosu-2018-csf.pdf differ diff --git a/publications/rodrigues-sebe-chen-rosu-tacas.bib b/publications/rodrigues-sebe-chen-rosu-tacas.bib new file mode 100644 index 0000000..063d136 --- /dev/null +++ b/publications/rodrigues-sebe-chen-rosu-tacas.bib @@ -0,0 +1,35 @@ +@inproceedings{rodrigues-sebe-chen-rosu-tacas, + author = {Nishant Rodrigues and Mircea Sebe and Xiaohong Chen and Grigore Ro\c{s}u}, + title = {A Logical Treatment of Finite Automata}, + abstract = { +We present a sound and complete axiomatization of finite words using +matching logic. A unique feature of our axiomatization is that it gives +a \emph{shallow embedding} of regular expressions into matching logic, +and a \emph{logical} representation of finite automata. The semantics of +both expressions and automata are precisely captured as matching logic +formulae that evaluate to the corresponding language. Regular +expressions are matching logic formulae \emph{as is}, while the +embedding of automata is a \emph{structural analog}---computational +aspects of automata are captured as syntactic features. We demonstrate +that our axiomatization is sound and complete by showing that runs of +Brzozowski's procedure for equivalence checking correspond to matching +logic proofs. We propose this as a general methodology for producing +machine-checkable formal proofs, enabled by capturing structural analogs +of computational artifacts in logic. The proofs produced can be +efficiently checked by the Metamath Zero verifier. Work presented in +this paper contributes to the general scheme of achieving verifiable +computing via logical methods, where computations are reduced to logical +reasoning, encoded as machine-checkable proof objects, and checked by a +trusted proof checker. + }, + author_id = {Nishant Rodrigues and Mircea Sebe and Xiaohong Chen and Grigore Rosu}, + category = {fsl, logics, matching_logic}, + project_url = {https://github.com/formal-systems-laboratory/matching-logic-mm0}, + project_name = {Matching Logic in MM0}, + booktitle_acronym = {TACAS'24}, + booktitle_url = {https://2023.splashcon.org/track/splash-2023-oopsla}, + booktitle = {Proceedings of OOPSLA 2023}, + year = {2024}, + month = {April}, + publisher = {ACM}, +} diff --git a/publications/rodrigues-sebe-chen-rosu-tacas.md b/publications/rodrigues-sebe-chen-rosu-tacas.md new file mode 100644 index 0000000..29697cf --- /dev/null +++ b/publications/rodrigues-sebe-chen-rosu-tacas.md @@ -0,0 +1,63 @@ +--- +bib: + abstract: We present a sound and complete axiomatization of finite words using matching + logic. A unique feature of our axiomatization is that it gives a \emph{shallow + embedding} of regular expressions into matching logic, and a \emph{logical} representation + of finite automata. The semantics of both expressions and automata are precisely + captured as matching logic formulae that evaluate to the corresponding language. + Regular expressions are matching logic formulae \emph{as is}, while the embedding + of automata is a \emph{structural analog}---computational aspects of automata + are captured as syntactic features. We demonstrate that our axiomatization is + sound and complete by showing that runs of Brzozowski's procedure for equivalence + checking correspond to matching logic proofs. We propose this as a general methodology + for producing machine-checkable formal proofs, enabled by capturing structural + analogs of computational artifacts in logic. The proofs produced can be efficiently + checked by the Metamath Zero verifier. Work presented in this paper contributes + to the general scheme of achieving verifiable computing via logical methods, where + computations are reduced to logical reasoning, encoded as machine-checkable proof + objects, and checked by a trusted proof checker. + author: + - first: Nishant + last: Rodrigues + - first: Mircea + last: Sebe + - first: Xiaohong + last: Chen + - first: Grigore + last: Ro\c{s}u + author_id: Nishant Rodrigues and Mircea Sebe and Xiaohong Chen and Grigore Rosu + author_ids: + - nishant-rodrigues + - mircea-sebe + - xiaohong-chen + - grigore-rosu + authors: + - id: nishant-rodrigues + text: Nishant Rodrigues + - id: mircea-sebe + text: Mircea Sebe + - id: xiaohong-chen + text: Xiaohong Chen + - id: grigore-rosu + text: Grigore Rosu + booktitle: Proceedings of OOPSLA 2023 + booktitle_acronym: TACAS'24 + booktitle_url: https://2023.splashcon.org/track/splash-2023-oopsla + category: + - fsl + - logics + - matching_logic + date: 2024-04-01 + id: rodrigues-sebe-chen-rosu-tacas + month: April + project_name: Matching Logic in MM0 + project_url: https://github.com/formal-systems-laboratory/matching-logic-mm0 + publisher: ACM + title: A Logical Treatment of Finite Automata + type: inproceedings + year: '2024' +bib_url: publications/rodrigues-sebe-chen-rosu-tacas.bib +layout: paper +pdf_url: publications/rodrigues-sebe-chen-rosu-tacas.pdf +title: A Logical Treatment of Finite Automata +--- diff --git a/publications/rodrigues-sebe-chen-rosu-tacas.pdf b/publications/rodrigues-sebe-chen-rosu-tacas.pdf new file mode 100644 index 0000000..58c27d1 Binary files /dev/null and b/publications/rodrigues-sebe-chen-rosu-tacas.pdf differ diff --git a/publications/rosu-stefanescu-ciobaca-moore-2013-lics.bib b/publications/rosu-stefanescu-ciobaca-moore-2013-lics.bib index aeef2ca..c5d6eb7 100644 --- a/publications/rosu-stefanescu-ciobaca-moore-2013-lics.bib +++ b/publications/rosu-stefanescu-ciobaca-moore-2013-lics.bib @@ -1,9 +1,14 @@ -@inproceedings{rosu-stefanescu-ciobaca-moore-2013-lics, - author = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu and \c{S}tefan - Ciob\^{a}c\u{a} and Brandon M. Moore}, - title = {One-Path Reachability Logic}, - abstract = { -This paper introduces *reachability logic*, a language-independent proof system +% Encoding: UTF-8 + +@InProceedings{rosu-stefanescu-ciobaca-moore-2013-lics, + author = {Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu and \c{S}tefan Ciob\^{a}c\u{a} and Brandon M. Moore}, + booktitle = {Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13)}, + title = {One-Path Reachability Logic}, + year = {2013}, + month = {June}, + pages = {358-367}, + publisher = {IEEE}, + abstract = {This paper introduces *reachability logic*, a language-independent proof system for program verification, which takes an operational semantics as axioms and derives *reachability rules*, which generalize Hoare triples. This system improves on previous work by allowing operational semantics given @@ -18,23 +23,14 @@ @inproceedings{rosu-stefanescu-ciobaca-moore-2013-lics prove the former sound and complete w.r.t. the latter. The soundness result has also been formalized in Coq, allowing reachability logic derivations to serve as formal proof certificates that rely only on the -operational semantics. - }, - booktitle = {Proceedings of the 28th Symposium on Logic in Computer Science - (LICS'13)}, - pages = {358-367}, - month = {June}, - year = {2013}, - publisher = {IEEE}, - - author_id = {Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and - Brandon Moore}, - category = {fsl, executable_semantics, k, logics, matching_logic, - program_verification, programming_languages}, - project_url = {http://fsl.cs.uiuc.edu/RL}, - project_name = {Reachability Logic}, +operational semantics.}, + author_id = {Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore}, booktitle_acronym = {LICS'13}, booktitle_url = {http://lii.rwth-aachen.de/lics/lics13/}, - doi = {}, - presentation = {2013-06-27-LICS} + category = {fsl, executable_semantics, k, logics, matching_logic, program_verification, programming_languages}, + presentation = {2013-06-27-LICS}, + project_name = {Reachability Logic}, + project_url = {http://fsl.cs.uiuc.edu/RL}, } + +@Comment{jabref-meta: databaseType:bibtex;} diff --git a/publications/rosu-stefanescu-ciobaca-moore-2013-lics.md b/publications/rosu-stefanescu-ciobaca-moore-2013-lics.md index 7039d32..8106f11 100644 --- a/publications/rosu-stefanescu-ciobaca-moore-2013-lics.md +++ b/publications/rosu-stefanescu-ciobaca-moore-2013-lics.md @@ -50,7 +50,6 @@ bib: - program_verification - programming_languages date: 2013-06-01 - doi: '' id: rosu-stefanescu-ciobaca-moore-2013-lics month: June pages: 358-367