Zobrazeno 1 - 10
of 27
pro vyhledávání: '"Traian Florin Şerbănuţă"'
Autor:
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon Moore, Traian Florin Serbanuta, Grigore Rosu
Publikováno v:
Logical Methods in Computer Science, Vol Volume 15, Issue 2 (2019)
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-
Externí odkaz:
https://doaj.org/article/96a8baa5bbcb494daa698a3cb86a7923
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 303, Iss Proc. FROM 2019, Pp 16-31 (2019)
Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two approaches, whic
Externí odkaz:
https://doaj.org/article/43173f457a144c60acc14bb2964720f6
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030290252
TABLEAUX
TABLEAUX
We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for w
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::eed33e3000ebbc7ffefe9e1bcec3e910
https://doi.org/10.1007/978-3-030-29026-9_25
https://doi.org/10.1007/978-3-030-29026-9_25
Publikováno v:
Journal of Logical and Algebraic Methods in Programming. 120:100644
We continue our investigation into hybrid polyadic multi-sorted logic with a focus on expresivity related to the operational and axiomatic semantics of rogramming languages, and relations with first-order logic. We identify a fragment of the full log
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a5805adbdae239581e1cc62bee70b7c8
https://doi.org/10.1016/j.jlamp.2021.100644
https://doi.org/10.1016/j.jlamp.2021.100644
Autor:
Grigore Rosu, Traian Florin Şerbănuţă
Publikováno v:
Electronic Notes in Theoretical Computer Science. 304:3-56
This paper gives an overview of the tool-supported K framework for semantics-based programming language design and formal analysis. K provides a convenient notation for modularly defining the syntax and the semantics of a programming language, togeth
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::003f41c7c14b5aa0e2cd49c0df52f5cd
https://doi.org/10.1016/j.entcs.2014.05.002
https://doi.org/10.1016/j.entcs.2014.05.002
Autor:
Edgar Pek, Manasvi Saxena, Yilong Li, Chris Hathhorn, Dwight Guth, Philip Daian, Grigore Rosu, Traian Florin Şerbănuţă
Publikováno v:
Runtime Verification ISBN: 9783319469812
RV
RV
We present a suite of runtime verification tools developed by Runtime Verification Inc.: RV-Match, RV-Predict, and RV-Monitor. RV-Match is a tool for checking C programs for undefined behavior and other common programmer mistakes. It is extracted fro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::28b3768a41ff7f8ee0e38d8d4a92d451
https://doi.org/10.1007/978-3-319-46982-9_5
https://doi.org/10.1007/978-3-319-46982-9_5
Autor:
Traian Florin Şerbănuţă, Liviu P. Dinu
Publikováno v:
Rewriting Logic and Its Applications ISBN: 9783319448015
WRLA
WRLA
This paper introduces contextual string rewriting as a special kind of parallel string rewriting in which each rule defines a context which is not changed by the application of the rule and can be read (but not modified) by other rules applying concu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e9056ff01b0a63d2c51abcabf5f3be29
https://doi.org/10.1007/978-3-319-44802-2_9
https://doi.org/10.1007/978-3-319-44802-2_9
Publikováno v:
Electronic Notes in Theoretical Computer Science. 192(1):125-141
This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ca27574e5bdacaf1d968c3c5455c1917
Publikováno v:
WRLA
A rewrite logic semantic definitional framework for programming languages is introduced, called K, together with partially automated translations of K language definitions into rewriting logic and into C. The framework is exemplified by defining SILF
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f16ff01cd0118b09564c32e5b142a162
Publikováno v:
Recent Trends in Algebraic Development Techniques ISBN: 9783319281131
WADT
WADT
We advance an institutional formalisation of the logical systems that underlie the $$\mathbb {K}$$K semantic framework and are used to capture both structural properties of program configurations through pattern matching, and changes of configuration
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::325f937399c16a2e1117f59a965028dd
https://doi.org/10.1007/978-3-319-28114-8_2
https://doi.org/10.1007/978-3-319-28114-8_2