Zobrazeno 1 - 10
of 33
pro vyhledávání: '"David Sanán"'
Publikováno v:
ACM Transactions on Programming Languages and Systems. 43:1-46
To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2ae6c49d4399f577aebf59878ae426e3
https://doi.org/10.1145/3436808
https://doi.org/10.1145/3436808
Publikováno v:
Journal of Automated Reasoning. 65:569-598
The SPARC instruction set architecture (ISA) has been used in various processors in workstations, embedded systems, and in mission-critical industries such as aviation and space engineering. Hence, it is important to provide formal frameworks that fa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8aae50109df0a2eecfa3c363344116dc
https://doi.org/10.1007/s10817-020-09579-4
https://doi.org/10.1007/s10817-020-09579-4
Publikováno v:
IEEE Transactions on Vehicular Technology. 69:7116-7130
The Controller Area Network (CAN) has been widely used in the automotive and industrial automation for over two decades. However, due to the lack of security mechanisms, CAN is vulnerable to attacks. In this paper, we propose a novel protection schem
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e974ce0feea046309bab6b5607fba646
https://doi.org/10.1109/tvt.2020.2990417
https://doi.org/10.1109/tvt.2020.2990417
Publikováno v:
Design Automation for Embedded Systems. 23:123-151
In order to define executable hardware description language while at the same time be fit for formal proofs of properties, a hardware description language VeriFormal, embedded in Isabelle/HOL, was created. VeriFormal, together with a translator and I
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d08e0cf554597c070b48182a19bfa558
https://doi.org/10.1007/s10617-019-09226-1
https://doi.org/10.1007/s10617-019-09226-1
Publikováno v:
ICECCS
Rely-Guarantee is a comprehensive technique that supports compositional reasoning for concurrent programs. However, specifications of the Rely condition - environment interference, and Guarantee condition - local transformation of thread state - are
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a9214fd40f532f469f3f27fdfc30de8f
https://doi.org/10.1109/iceccs51672.2020.00013
https://doi.org/10.1109/iceccs51672.2020.00013
Publikováno v:
IEEE Symposium on Security and Privacy
Bitcoin has been a popular research topic recently. Ethereum (ETH), a second generation of cryptocurrency, extends Bitcoin’s design by offering a Turing-complete programming language called Solidity to develop smart contracts. Smart contracts allow
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2677156092f037ad65ec259778d870e2
https://doi.org/10.1109/sp40000.2020.00066
https://doi.org/10.1109/sp40000.2020.00066
Publikováno v:
ICECCS
Buddy memory allocation algorithms are widely adopted by various memory management systems for managing memory layouts. Rigorous mathematical proofs provide strong assurance to improve the confidence on the reliability of a memory management system.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f2c29e356da0d6dfa4590fa35b139a64
https://doi.org/10.1109/iceccs.2019.00023
https://doi.org/10.1109/iceccs.2019.00023
Autor:
David Sanán, Yongwang Zhao
Publikováno v:
Computer Aided Verification ISBN: 9783030255428
CAV (2)
CAV (2)
Formal verification of concurrent operating systems (OSs) is challenging, and in particular the verification of the dynamic memory management due to its complex data structures and allocation algorithm. Up to our knowledge, this paper presents the fi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9affd2dec2e2d298eb6936bab81833b3
https://doi.org/10.1007/978-3-030-25543-5_29
https://doi.org/10.1007/978-3-030-25543-5_29
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030309411
FM
FM
Reactive systems are composed of a well defined set of event handlers by which the system responds to environment stimulus. In concurrent environments, event handlers can interact with the execution of other handlers such as hardware interruptions in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f716f4e89562315965b909079f752f0c
https://doi.org/10.1007/978-3-030-30942-8_11
https://doi.org/10.1007/978-3-030-30942-8_11
Publikováno v:
Dependable Software Engineering. Theories, Tools, and Applications ISBN: 9783030355395
SETTA
SETTA
Formal verification of real-time services is important because they are usually associated with safety-critical systems. In this paper, we present a verified Two-Level Segregated Fit (TLSF) memory management model. TLSF is a dynamic memory allocator
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3c8aefae51b770b5b7b4ec0109632906
https://doi.org/10.1007/978-3-030-35540-1_8
https://doi.org/10.1007/978-3-030-35540-1_8