Zobrazeno 1 - 10
of 43
pro vyhledávání: '"Leustean, Ioana"'
The seL4 microkernel is currently the only kernel that has been fully formally verified. In general, the increased interest in ensuring the security of a kernel's code results from its important role in the entire operating system. One of the basic f
Externí odkaz:
http://arxiv.org/abs/2311.03585
Autor:
Leustean, Ioana, Macovei, Bogdan
The formal analysis of security protocols is a challenging field, with various approaches being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to validate security protocols. Combining ideas from previous
Externí odkaz:
http://arxiv.org/abs/2109.05599
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
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
We extend \L ukasiewicz logic obtaining the infinitary logic $\mathcal{IR}\L$ whose models are algebras $C(X,[0,1])$, where $X$ is a basically disconnected compact Hausdorff space. Equivalently, our models are unit intervals in $\sigma$-complete Ries
Externí odkaz:
http://arxiv.org/abs/1709.08397
We study \L ukasiewicz logic enriched with a scalar multiplication with scalars taken in $[0,1]$. Its algebraic models, called {\em Riesz MV-algebras}, are, up to isomorphism, unit intervals of Riesz spaces with a strong unit endowed with an appropri
Externí odkaz:
http://arxiv.org/abs/1607.08030
Autor:
Lapenta, Serafina, Leustean, Ioana
In these notes we study the class of divisible MV-algebras inside the algebraic hierarchy of MV-algebras with product. We connect divisible MV-algebras with $\mathbb Q$-vector lattices, we present the divisible hull as a categorical adjunction and we
Externí odkaz:
http://arxiv.org/abs/1605.01230
Publikováno v:
In Journal of Logical and Algebraic Methods in Programming April 2021 120
