Zobrazeno 1 - 9
of 9
pro vyhledávání: '"Daniel Matichuk"'
Autor:
Daniel Matichuk
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 102, Iss Proc. SSV 2012, Pp 46-56 (2012)
In systems verification we are often concerned with multiple, inter-dependent properties that a program must satisfy. To prove that a program satisfies a given property, the correctness of intermediate states of the program must be characterized. How
Externí odkaz:
https://doaj.org/article/ab1e81de37c04727ae8ecd253508fc03
Publikováno v:
Journal of Automated Reasoning. 56:261-282
Machine-checked proofs are becoming ever-larger, presenting an increasing maintenance challenge. Isabelle's most popular language interface, Isar, is attractive for new users, and powerful in the hands of experts, but has previously lacked a means to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::60937f4ba02e2a83d4ea3b5e3883a25c
https://doi.org/10.1007/s10817-015-9360-2
https://doi.org/10.1007/s10817-015-9360-2
Autor:
Daniel Matichuk, K. Rustan M. Leino
Publikováno v:
Principled Software Development ISBN: 9783319980461
Principled Software Development
Principled Software Development
Following software engineering best practices, programs are divided into modules to facilitate information hiding. A variety of programming-language constructs provide ways to define a module and to classify which of its declarations are private to t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::36c3e5bfdb93b41fa6da78c69143a558
https://doi.org/10.1007/978-3-319-98047-8_12
https://doi.org/10.1007/978-3-319-98047-8_12
Publikováno v:
Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375(2104). The Royal Society
We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microke
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9f7106cd61507bc20cbde7737e73f78c
https://pubmed.ncbi.nlm.nih.gov/28871053
https://pubmed.ncbi.nlm.nih.gov/28871053
Publikováno v:
Interactive Theorem Proving ISBN: 9783319431437
ITP
ITP
We present a simple yet scalable framework for formal reasoning and machine-assisted proof of interrupt-driven concurrency in operating-system code, and use it to prove the principal scheduling property of the embedded, real-time eChronos OS: that th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c2112319dbeba1862596fadbf296573d
https://doi.org/10.1007/978-3-319-43144-4_4
https://doi.org/10.1007/978-3-319-43144-4_4
Publikováno v:
2015 IEEE/ACM 37th IEEE International Conference on Software Engineering.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c0e431450caa664257e5f01f89b13227
https://doi.org/10.1109/icse.2015.85
https://doi.org/10.1109/icse.2015.85
Publikováno v:
Interactive Theorem Proving ISBN: 9783319089690
ITP
ITP
Machine-checked proofs are becoming ever-larger, presenting an increasing maintenance challenge. Isabelle’s most popular language interface, Isar, is attractive for new users, and powerful in the hands of experts, but has previously lacked a means
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7fda599201d45c1815c5c2e5f207ea0e
https://doi.org/10.1007/978-3-319-08970-6_25
https://doi.org/10.1007/978-3-319-08970-6_25
Autor:
Xin Gao, Sean Seefried, M. Brassil, Corey Lewis, Gerwin Klein, Daniel Matichuk, Peter Gammie, Timothy Bourke, Toby Murray
Publikováno v:
IEEE Symposium on Security and Privacy
In contrast to testing, mathematical reasoning and formal verification can show the absence of whole classes of security vulnerabilities. We present the, to our knowledge, first complete, formal, machine-checked verification of information flow secur
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8ec686feb3511fe961d3ec1002a3e9dc
https://doi.org/10.1109/sp.2013.35
https://doi.org/10.1109/sp.2013.35
Autor:
Daniel Matichuk, Toby Murray
Publikováno v:
Software Engineering and Formal Methods ISBN: 9783642338250
SEFM
SEFM
One way to reduce the cost of formally verifying a large program is to perform proofs over a specification of its behaviour, which its implementation refines. However, interesting programs must often satisfy multiple properties. Ideally, each propert
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::172a21569c974e109dde807bc35c5a94
https://doi.org/10.1007/978-3-642-33826-7_23
https://doi.org/10.1007/978-3-642-33826-7_23