Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Kuppe, Markus A."'
The Confidential Consortium Framework (CCF) is an open-source platform for developing trustworthy and reliable cloud applications. CCF powers Microsoft's Azure Confidential Ledger service and as such it is vital to build confidence in the correctness
Externí odkaz:
http://arxiv.org/abs/2406.17455
TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work we present a framework for relating traces of distributed programs to high-level specifications written
Externí odkaz:
http://arxiv.org/abs/2404.16075
Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages. Se
Externí odkaz:
http://arxiv.org/abs/2404.10362
Autor:
Howard, Heidi, Alder, Fritz, Ashton, Edward, Chamayou, Amaury, Clebsch, Sylvan, Costa, Manuel, Delignat-Lavaud, Antoine, Fournet, Cedric, Jeffery, Andrew, Kerner, Matthew, Kounelis, Fotios, Kuppe, Markus A., Maffre, Julien, Russinovich, Mark, Wintersteiger, Christoph M.
Confidentiality, integrity protection, and high availability, abbreviated to CIA, are essential properties for trustworthy data systems. The rise of cloud computing and the growing demand for multiparty applications however means that building modern
Externí odkaz:
http://arxiv.org/abs/2310.11559
Publikováno v:
Leveraging Applications of Formal Methods, Verification and Validation. 11th International Symposium, ISoLA 2022, 2022, Rhodes, Greece. pp.88-105
Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a workflow that sup
Externí odkaz:
http://arxiv.org/abs/2211.07216
Beyond implementation correctness of a distributed system, it is equally important to understand exactly what users should expect to see from that system. Even if the system itself works as designed, insufficient understanding of its user-visible sem
Externí odkaz:
http://arxiv.org/abs/2210.13661
Publikováno v:
EPTCS 310, 2019, pp. 50-62
We discuss the workflows supported by the TLA+ Toolbox to write and verify specifications. We focus on features that are useful in industry because its users are primarily engineers. Two features are novel in the scope of formal IDEs: CloudTLC connec
Externí odkaz:
http://arxiv.org/abs/1912.10633
Autor:
Freitas, Leo, Hallerstede, Stefan, Hansen, Dominik, Kuppe, Markus, Mejia, Fernando, Merz, Stephan, Vanzetto, Hernán, Winter, Kirsten
Publikováno v:
Freitas, L, Hallerstede, S, Hansen, D, Kuppe, M, Mejia, F, Merz, S, Vanzetto, H & Winter, K 2014, Modeling Dijkstra’s Termination Detection Algorithm in TLA+ . in U Glässer, S Hallerstede, M Leuschel & E Riccobene (eds), Integration of Tools for Rigorous Software Construction and Analysis (Dagstuhl Seminar 13372) . vol. Dagstuhl Reports, Volume 3, Issue 9, Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Integration of Tools for Rigorous Software Construction and Analysis, Leipzig, Germany, 08/09/2013 . https://doi.org/10.4230/DagRep.3.9.74
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=pure_au_____::05f58e6257d0e133114921fed621d1a3
https://pure.au.dk/portal/da/publications/modeling-dijkstras-termination-detection-algorithm-in-tla(f8d97538-936e-48b3-8089-db9d4a88f068).html
https://pure.au.dk/portal/da/publications/modeling-dijkstras-termination-detection-algorithm-in-tla(f8d97538-936e-48b3-8089-db9d4a88f068).html
Publikováno v:
Ausweg Wachstum?; 2007, p139-159, 21p
Publikováno v:
In Computer Aided Geometric Design 1998 15(9):869-877