Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Miraldo, Victor Cacciari"'
We are using the Agda programming language and proof assistant to formally verify the correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / LibraBFT. The Agda implementation is a translation of our Haskell implementat
Externí odkaz:
http://arxiv.org/abs/2205.08718
LibraBFT is a Byzantine Fault Tolerant (BFT) consensus protocol based on HotStuff. We present an abstract model of the protocol underlying HotStuff / LibraBFT, and formal, machine-checked proofs of their core correctness (safety) property and an exte
Externí odkaz:
http://arxiv.org/abs/2203.14711
Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify the entire log, or to trust another party regarding its contents. AAOSLs
Externí odkaz:
http://arxiv.org/abs/2103.04519
The type class system in the Haskell Programming language provides a useful abstraction for a wide range of types, such as those that support comparison, serialization, ordering, between others. This system can be extended by the programmer by provid
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______101::fd00b217684c275a56d7491d27f003be
https://dspace.library.uu.nl/handle/1874/378085
https://dspace.library.uu.nl/handle/1874/378085
Autor:
Miraldo, Victor Cacciari, Dagand, Pierre Evariste, Swierstra, Wouter, Sub Software Technology, Software Technology
Publikováno v:
Proceedings of the Workshop on Type Directed Development, TyDe~'17, Oxford, UK
The Unix diff utility that compares lines of text is used pervasively by version control systems. Yet certain changes to a program may be dicult to describe accurately in terms of modications to individual lines of code. As a result, observing change
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=narcis______::6171b9503df29c2cbfc7c7df760b3617
https://dspace.library.uu.nl/handle/1874/355261
https://dspace.library.uu.nl/handle/1874/355261
Autor:
Miraldo, Victor Cacciari
Publikováno v:
Repositório Científico de Acesso Aberto de Portugal
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
Predicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::e41eb8234e6b6d495eb2b82a80484c71
Autor:
Miraldo, Victor Cacciari
Publikováno v:
Repositório Científico de Acesso Aberto de Portugal
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
SABS is a predicate abstraction laboratory that is beeing developed at University of Minho, Portugal. Our goal is not to produce a industrial software model checker, such as SLAM [BMR01] or SATABS [CKSY05], but to have a tool to study and compare the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::9f037fb2c99ec8b3fecc19807e0aea9d
https://hdl.handle.net/1822/35231
https://hdl.handle.net/1822/35231
Predicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______307::19e43e403c8497c03a0301b2dbe80f2a
https://hdl.handle.net/1822/26360
https://hdl.handle.net/1822/26360
Publikováno v:
ACM / SIGPLAN Notices; Jul2018, Vol. 53 Issue 7, p41-54, 14p
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.