Zobrazeno 1 - 10
of 68
pro vyhledávání: '"Şerbănuţă, Traian"'
Publikováno v:
EPTCS 389, 2023, pp. 152-166
In this work-in-progress paper we explore using the recently introduced VLSM formalism to define and reason about the dynamics of agent-based systems. To this aim we use VLSMs to formally present several possible approaches to modeling the interactio
Externí odkaz:
http://arxiv.org/abs/2309.13808
Autor:
Zamfir, Vlad, Calancea, Mihai, Diaconescu, Denisa, Kołowski, Wojciech, Moore, Brandon, Palmskog, Karl, Şerbănuţă, Traian Florin, Stay, Michael, Trufaş, Dafina, Tušil, Jan
Modeling and formally reasoning about distributed systems with faults is a challenging task. To address this problem, we propose the theory of Validating Labeled State transition and Message production systems (VLSMs). The theory of VLSMs provides a
Externí odkaz:
http://arxiv.org/abs/2202.12662
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:
http://arxiv.org/abs/2007.01709
Publikováno v:
EPTCS 303, 2019, pp. 16-31
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:
http://arxiv.org/abs/1907.05029
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:
http://arxiv.org/abs/1905.05036
Autor:
Stefanescu, Andrei, Ciobaca, Stefan, Mereuta, Radu, Moore, Brandon, Serbanuta, Traian Florin, Rosu, Grigore
Publikováno v:
Logical Methods in Computer Science, Volume 15, Issue 2 (April 30, 2019) lmcs:4939
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:
http://arxiv.org/abs/1810.10826
This paper presents a many-sorted polyadic modal logic that generalizes some of the existing approaches. The algebraic semantics has led us to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the J\'
Externí odkaz:
http://arxiv.org/abs/1803.09709
Publikováno v:
In Journal of Logical and Algebraic Methods in Programming April 2021 120
Autor:
Şerbănuţă, Traian Florin
Publikováno v:
In Electronic Notes in Theoretical Computer Science 10 June 2014 304:167-182
Publikováno v:
In Electronic Notes in Theoretical Computer Science 10 June 2014 304:3-56