Showing 1–16 of 16 results for author: Leustean, I

OpenBSD formal driver verification with SeL4

Authors: Adriana Nicolae, Paul Irofti, Ioana Leustean

Abstract: 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 features of an operating system is that it abstracts the handling of devices. This abstraction is represented by device drivers - the software that man… ▽ More 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 features of an operating system is that it abstracts the handling of devices. This abstraction is represented by device drivers - the software that manages the hardware. A proper verification of the software component could ensure that the device would work properly unless there is a hardware failure.In this paper, we choose to model the behavior of a device driver and build the proof that the code implementation matches the expected behavior. The proof was written in Isabelle/HOL, the code translation from C to Isabelle was done automatically by the use of the C-to-Isabelle Parser and AutoCorres tools. We choose Isabelle theorem prover because its efficiency was already shown through the verification of seL4 microkernel. △ Less

Submitted 6 November, 2023; originally announced November 2023.

DELP: Dynamic Epistemic Logic for Security Protocols

Authors: Ioana Leustean, Bogdan Macovei

Abstract: 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 approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few o… ▽ More 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 approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of its properties are verifyied, using the theorem prover Lean. △ Less

Submitted 1 November, 2021; v1 submitted 12 September, 2021; originally announced September 2021.

Many-Sorted Hybrid Modal Languages

Authors: Ioana Leuştean, Natalia Moangă, Traian Florin Şerbănuţă

Abstract: 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 logic, for which we prove sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an un… ▽ More 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 logic, for which we prove sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an uniform way. Although weaker than other hybrid systems previously developed, this system is expected to have better computational properties. Finally, we provide a standard translation from full hybrid many-sorted logic to first-order logic. △ Less

Submitted 2 July, 2020; originally announced July 2020.

Comments: arXiv admin note: text overlap with arXiv:1905.05036, arXiv:1907.05029

From Hybrid Modal Logic to Matching Logic and Back

Authors: Ioana Leuştean, Natalia Moangă, Traian Florin Şerbănuţă

Abstract: 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, which should benefit both systems. 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, which should benefit both systems. △ Less

Submitted 4 September, 2019; v1 submitted 11 July, 2019; originally announced July 2019.

Comments: In Proceedings FROM 2019, arXiv:1909.00584

Journal ref: EPTCS 303, 2019, pp. 16-31

Operational semantics and program verification using many-sorted hybrid modal logic

Authors: Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta

Abstract: 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 which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (… ▽ More 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 which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (1) it is based on operational semantics which allows for a more natural description of the execution than Hoare's style weakest precondition used by dynamic logic; (2) being multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning. △ Less

Submitted 13 May, 2019; originally announced May 2019.

A many-sorted polyadic modal logic

Authors: Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta

Abstract: 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ónsson-Tarski theorem. While the transition from the mono-sorted logic to many-sorted one is a smooth process, we see our system as a step towards deepe… ▽ More 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ónsson-Tarski theorem. While the transition from the mono-sorted logic to many-sorted one is a smooth process, we see our system as a step towards deepening the connection between modal logic and program verification, since our system can be seen as the propositional fragment of Matching logic, a first-order logic for specifying and reasoning about programs. △ Less

Submitted 30 November, 2018; v1 submitted 26 March, 2018; originally announced March 2018.

Infinitary logic and basically disconnected compact Hausdorff spaces

Authors: Antonio Di Nola, Serafina Lapenta, Ioana Leustean

Abstract: We extend Łukasiewicz logic obtaining the infinitary logic $\mathcal{IR}Ł$ whose models are algebras $C(X,[0,1])$, where $X$ is a basically disconnected compact Hausdorff space. Equivalently, our models are unit intervals in $σ$-complete Riesz spaces with strong unit. The Lindenbaum-Tarski algebra of $\mathcal{IR}Ł$ is, up to isomorphism, an algebra of $[0,1]$-valued Borel functions. Finally, our… ▽ More We extend Łukasiewicz logic obtaining the infinitary logic $\mathcal{IR}Ł$ whose models are algebras $C(X,[0,1])$, where $X$ is a basically disconnected compact Hausdorff space. Equivalently, our models are unit intervals in $σ$-complete Riesz spaces with strong unit. The Lindenbaum-Tarski algebra of $\mathcal{IR}Ł$ is, up to isomorphism, an algebra of $[0,1]$-valued Borel functions. Finally, our system enjoys standard completeness with respect to the real interval $[0,1]$. △ Less

Submitted 18 April, 2018; v1 submitted 25 September, 2017; originally announced September 2017.

An analysis of the logic of Riesz Spaces with strong unit

Authors: Antonio Di Nola, Serafina Lapenta, Ioana Leustean

Abstract: We study Ł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 appropriate structure. When only rational scalars are considered, one gets the class of {\em DMV-algebras} and a corresponding logical system. Our research foll… ▽ More We study Ł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 appropriate structure. When only rational scalars are considered, one gets the class of {\em DMV-algebras} and a corresponding logical system. Our research follows two objectives. The first one is to deepen the connections between functional analysis and the logic of Riesz MV-algebras. The second one is to study the finitely presented MV-algebras, DMV-algebras and Riesz MV-algebras, connecting them from logical, algebraic and geometric perspective. △ Less

Submitted 23 September, 2017; v1 submitted 27 July, 2016; originally announced July 2016.

Notes on divisible MV-algebras

Authors: Serafina Lapenta, Ioana Leustean

Abstract: 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 prove a duality between finitely presented algebras and rational polyhedra. 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 prove a duality between finitely presented algebras and rational polyhedra. △ Less

Submitted 2 November, 2016; v1 submitted 4 May, 2016; originally announced May 2016.

Mutually exclusive nuances of truth in Moisil logic

Authors: Denisa Diaconescu, Ioana Leustean

Abstract: Moisil logic, having as algebraic counterpart Łukasiewicz-Moisil algebras, provide an alternative way to reason about vague information based on the following principle: a many-valued event is characterized by a family of Boolean events. However, using the original definition of Łukasiewicz-Moisil algebra, the principle does not apply for subalgebras. In this paper we identify an alternative and e… ▽ More Moisil logic, having as algebraic counterpart Łukasiewicz-Moisil algebras, provide an alternative way to reason about vague information based on the following principle: a many-valued event is characterized by a family of Boolean events. However, using the original definition of Łukasiewicz-Moisil algebra, the principle does not apply for subalgebras. In this paper we identify an alternative and equivalent definition for the $n$-valued Łukasiewicz-Moisil algebras, in which the determination principle is also saved for arbitrary subalgebras, which are characterized by a Boolean algebra and a family of Boolean ideals. As a consequence, we prove a duality result for the $n$-valued Łukasiewicz-Moisil algebras, starting from the dual space of their Boolean center. This leads us to a duality for MV$_n$-algebras, since are equivalent to a subclass of $n$-valued Łukasiewicz-Moisil algebras. △ Less

Submitted 9 December, 2014; originally announced December 2014.

A general view of the algebraic semantics of Łukasiewicz logic with product

Authors: Serafina Lapenta, Ioana Leustean

Abstract: This paper aims at connecting the various classes that provide an algebraic semantics for three different conservative expansions of Lukasiewicz logic, using algebraic and category-theoretical techniques. We connect such classes of algebras by adjunctions, using the tensor product of MV-algebras and defining the tensor PMV-algebra of a semisimple MV-algebra, inspired by the construction of the ten… ▽ More This paper aims at connecting the various classes that provide an algebraic semantics for three different conservative expansions of Lukasiewicz logic, using algebraic and category-theoretical techniques. We connect such classes of algebras by adjunctions, using the tensor product of MV-algebras and defining the tensor PMV-algebra of a semisimple MV-algebra, inspired by the construction of the tensor algebra of a vector space. We further apply the main results to prove amalgamation properties and, via categorical equivalence, we transfer all results to the framework of lattice- ordered groups. △ Less

Submitted 19 September, 2018; v1 submitted 18 November, 2014; originally announced November 2014.

The Riesz hull of a semisimple MV-algebra

Authors: Denisa Diaconescu, Ioana Leustean

Abstract: MV-algebras and Riesz MV-algebras are categorically equivalent to abelian lattice-ordered groups with strong unit and, respectively, with Riesz spaces (vector-lattices) with strong unit. A standard construction in the literature of lattice-ordered groups is the vector-lattice hull of an archimedean lattice-ordered group. Following a similar approach, in this paper we define the Riesz hull of a sem… ▽ More MV-algebras and Riesz MV-algebras are categorically equivalent to abelian lattice-ordered groups with strong unit and, respectively, with Riesz spaces (vector-lattices) with strong unit. A standard construction in the literature of lattice-ordered groups is the vector-lattice hull of an archimedean lattice-ordered group. Following a similar approach, in this paper we define the Riesz hull of a semisimple MV-algebra. △ Less

Submitted 30 October, 2014; originally announced October 2014.

Scalar extensions for algebraic structures of Lukasiewicz logic

Authors: Serafina Lapenta, Ioana Leustean

Abstract: In this paper we study the tensor product for MV-algebras, the algebraic structures of Łukasiewicz $\infty$-valued logic. Our main results are: the proof that the tensor product is preserved by the categorical equivalence between the MV-algebras and abelian lattice-order groups with strong unit and the proof of the scalar extension property for semisimple MV-algebras. We explore consequences of th… ▽ More In this paper we study the tensor product for MV-algebras, the algebraic structures of Łukasiewicz $\infty$-valued logic. Our main results are: the proof that the tensor product is preserved by the categorical equivalence between the MV-algebras and abelian lattice-order groups with strong unit and the proof of the scalar extension property for semisimple MV-algebras. We explore consequences of this results for various classes of MV-algebras and lattice-ordered groups enriched with a product operation. △ Less

Submitted 30 October, 2014; originally announced October 2014.

Journal ref: Journal of Pure and Applied Algebra, 220 (2016) 1538-1553

Stochastic independence for probability MV-algebras

Authors: Serafina Lapenta, Ioana Leustean

Abstract: We prove that any MV-algebra has a faithful state can be embedded in an \em{f}MV-algebra of integrable functions. As consequence, we prove Hölder's inequality and Hausdorff moment problem for MV-algebras with product and we propose a solution for the stochastic independence of probability MV-algebras. We prove that any MV-algebra has a faithful state can be embedded in an \em{f}MV-algebra of integrable functions. As consequence, we prove Hölder's inequality and Hausdorff moment problem for MV-algebras with product and we propose a solution for the stochastic independence of probability MV-algebras. △ Less

Submitted 21 October, 2014; originally announced October 2014.

Journal ref: Fuzzy Sets and Systems 298 (2016) 194-206

Towards understanding the Pierce-Birkhoff conjecture via MV-algebras

Authors: Serafina Lapenta, Ioana Leustean

Abstract: Our main issue was to understand the connection between Łukasiewicz logic with product and the Pierce-Birkhoff conjecture, and to express it in a mathematical way. To do this we define the class of \textit{f}MV-algebras, which are MV-algebras endowed with both an internal binary product and a scalar product with scalars from $[0,1]$. The proper quasi-variety generated by $[0,1]$, with both product… ▽ More Our main issue was to understand the connection between Łukasiewicz logic with product and the Pierce-Birkhoff conjecture, and to express it in a mathematical way. To do this we define the class of \textit{f}MV-algebras, which are MV-algebras endowed with both an internal binary product and a scalar product with scalars from $[0,1]$. The proper quasi-variety generated by $[0,1]$, with both products interpreted as the real product, provides the desired framework: the normal form theorem of its corresponding logical system can be seen as a local version of the Pierce-Birkhoff conjecture. △ Less

Submitted 13 November, 2014; v1 submitted 21 October, 2014; originally announced October 2014.

Journal ref: Fuzzy Sets and Systems 276 (2015) 114-130

Lukasiewicz logic and Riesz spaces

Authors: Antonio Di Nola, Ioana Leustean

Abstract: We initiate a deep study of {\em Riesz MV-algebras} which are MV-algebras endowed with a scalar multiplication with scalars from $[0,1]$. Extending Mundici's equivalence between MV-algebras and $\ell$-groups, we prove that Riesz MV-algebras are categorically equivalent with unit intervals in Riesz spaces with strong unit. Moreover, the subclass of norm-complete Riesz MV-algebras is equivalent with… ▽ More We initiate a deep study of {\em Riesz MV-algebras} which are MV-algebras endowed with a scalar multiplication with scalars from $[0,1]$. Extending Mundici's equivalence between MV-algebras and $\ell$-groups, we prove that Riesz MV-algebras are categorically equivalent with unit intervals in Riesz spaces with strong unit. Moreover, the subclass of norm-complete Riesz MV-algebras is equivalent with the class of commutative unital C$^*$-algebras. The propositional calculus ${\mathbb R}{\cal L}$ that has Riesz MV-algebras as models is a conservative extension of Łukasiewicz $\infty$-valued propositional calculus and it is complete with respect to evaluations in the standard model $[0,1]$. We prove a normal form theorem for this logic, extending McNaughton theorem for Łukasiewicz logic. We define the notions of quasi-linear combination and quasi-linear span for formulas in ${\mathbb R}{\cal L}$ and we relate them with the analogue of de Finetti's coherence criterion for ${\mathbb R}{\cal L}$. △ Less

Submitted 6 September, 2013; originally announced September 2013.

Comments: To appear in Soft Computing

MSC Class: 06D35; 03B50