Výsledky vyhledávání - "Marijana Lazić"

Akademický článek

Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker

Autor: Igor Konnov, Marijana Lazić, Ilina Stoilkovska, Josef Widder

Publikováno v: Logical Methods in Computer Science, Vol Volume 19, Issue 1 (2023)

Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems in distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain

Externí odkaz: https://doaj.org/article/108d81d8efd84c74b43f1fa7438e852f

Zobrazit plný text záznamu

Tutorial: Parameterized Verification with Byzantine Model Checker

Autor: Ilina Stoilkovska, Josef Widder, Igor Konnov, Marijana Lazić

Publikováno v: Formal Techniques for Distributed Objects, Components, and Systems
Lecture Notes in Computer Science
40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2020, Valletta, Malta. pp.189-207, ⟨10.1007/978-3-030-50086-3_11⟩
Lecture Notes in Computer Science-Formal Techniques for Distributed Objects, Components, and Systems
Formal Techniques for Distributed Objects, Components, and Systems-FORTE 2020
Formal Techniques for Distributed Objects, Components, and Systems ISBN: 9783030500856
FORTE

Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems of distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::38de7bae2c1fc24e3117277040576c3d
http://europepmc.org/articles/PMC7281874

Zobrazit plný text záznamu

A Reduction Theorem for Randomized Distributed Algorithms Under Weak Adversaries

Autor: Marijana Lazić, Josef Widder, Nathalie Bertrand

Publikováno v: VMCAI 2021-22nd International Conference on Verification, Model Checking, and Abstract Interpretation
VMCAI 2021-22nd International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2021, Copenhagen, Denmark. pp.219-239, ⟨10.1007/978-3-030-67067-2_11⟩
Lecture Notes in Computer Science ISBN: 9783030670665
VMCAI
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Verification, Model Checking, and Abstract Interpretation
Verification, Model Checking, and Abstract Interpretation

International audience; Weak adversaries are a way to model the uncertainty due to asynchrony in randomized distributed algorithms. They are a standard notion in correctness proofs for distributed algorithms, and express the property that the adversa

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7436db3e6a99de82137b752c4bc47cf4
https://hal.inria.fr/hal-03150397

Zobrazit plný text záznamu

A dynamic epistemic logic analysis of equality negation and other epistemic covering tasks

Autor: Jérémy Ledent, Hans van Ditmarsch, Marijana Lazić, Eric Goubault, Sergio Rajsbaum

Publikováno v: Journal of Logical and Algebraic Methods in Programming

In this paper we study the solvability of the equality negation task in a simple wait-free model where two processes communicate by reading and writing shared variables or exchanging messages. In this task, the two processes start with a private inpu

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f0c1a912eb454b84b72967df23c27b82

Zobrazit plný text záznamu

Para $$^2$$ 2 : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms

Autor: Marijana Lazić, Helmut Veith, Josef Widder, Igor Konnov

Publikováno v: Formal Methods in System Design. 51:270-307

Automatic verification of threshold-based fault-tolerant distributed algorithms (FTDA) is challenging: FTDAs have multiple parameters that are restricted by arithmetic conditions, the number of processes and faults is parameterized, and the algorithm

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::db0745c8d812eb2b476f503a9dacf2b5
https://doi.org/10.1007/s10703-017-0297-4

Zobrazit plný text záznamu

Correction to: Verification of randomized consensus algorithms under round-rigid adversaries

Autor: Nathalie Bertrand, Marijana Lazić, Igor Konnov, Josef Widder

Publikováno v: International Journal on Software Tools for Technology Transfer. 23:823-823

A correction to this paper has been published: https://doi.org/10.1007/s10009-021-00612-4

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::c4288d7c8b531bb16cf057bb5584fe81
https://doi.org/10.1007/s10009-021-00612-4

Zobrazit plný text záznamu

Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries

Autor: Nathalie Bertrand, Igor Konnov, Marijana Lazić, Josef Widder

Publikováno v: CONCUR 2019-30th International Conference on Concurrency Theory
CONCUR 2019-30th International Conference on Concurrency Theory, Aug 2019, Amsterdam, Netherlands. pp.1-16, ⟨10.4230/LIPIcs.CONCUR.2019.33⟩
International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, Springer Verlag, 2021, 23, pp.797-821. ⟨10.1007/s10009-020-00603-x⟩
International Journal on Software Tools for Technology Transfer, 2021, 23, pp.797-821. ⟨10.1007/s10009-020-00603-x⟩
30th International Conference on Concurrency Theory (CONCUR 2019)

International audience; Randomized fault-tolerant distributed algorithms pose a number of challenges for automated verification: (i) parameterization in the number of processes and faults, (ii) randomized choices and probabilistic properties, and (ii

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8fccafbdf2ff7912fb73bd9d3c483908

Zobrazit plný text záznamu

Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics

Autor: Idan Berkovits, Sharon Shoham, Oded Padon, Marijana Lazić, Giuliano Losa

Publikováno v: Computer Aided Verification-31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II
Computer Aided Verification ISBN: 9783030255428
CAV (2)
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Computer Aided Verification

Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code and in its correctness proof, e.g., a process can perform an action only

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::118c5dd2cfb1838b3e66819f355165c9

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání