Zobrazeno 1 - 10
of 15
pro vyhledávání: '"William Mansky"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 159, Iss Proc. GRAPHITE 2014, Pp 58-70 (2014)
Compiler optimizations, usually expressed as rewrites on program graphs, are a core part of all modern compilers. However, even production compilers have bugs, and these bugs are difficult to detect and resolve. The problem only becomes more complex
Externí odkaz:
https://doaj.org/article/4853e5b6c1414df6ada2d0a2e4ee8ad5
Publikováno v:
Programming Languages and Systems ISBN: 9783030449131
ESOP
ESOP
Separation logic is a useful tool for proving the correctness of programs that manipulate memory, especially when the model of memory includes higher-order state: Step-indexing, predicates in the heap, and higher-order ghost state have been used to r
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ce66f70bb707c1ba9815f976d8469a35
https://doi.org/10.1007/978-3-030-44914-8_16
https://doi.org/10.1007/978-3-030-44914-8_16
Publikováno v:
Proceedings of the ACM on Programming Languages. 1:1-28
We present a concurrent-read exclusive-write buffer system with strong correctness and security properties. Our motivating application for this system is the distribution of sensor values in a multicomponent vehicle-control system, where some compone
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1b53bfb49cd618ea806195bf00c6367d
https://doi.org/10.1145/3133911
https://doi.org/10.1145/3133911
Publikováno v:
Science of Computer Programming. 130:2-23
Optimizations performed by compilers, usually expressed as rewrites on program graphs, are a core part of modern compilers. However, even production compilers have bugs, and these bugs are difficult to detect and resolve. In this paper we present Mor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e30033b41749227f7ccefef1466f98e1
https://doi.org/10.1016/j.scico.2016.06.003
https://doi.org/10.1016/j.scico.2016.06.003
Autor:
Yao Li, Yishuai Li, Li-yao Xia, William Mansky, Benjamin C. Pierce, Nicolas Koh, Wolf Honoré, Lennart Beringer, Steve Zdancewic
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fe885bf3abe5791f0a9d5609ee07a7b1
http://arxiv.org/abs/1811.11911
http://arxiv.org/abs/1811.11911
Publikováno v:
IPDPS
Data races are one of the main culprits behind the complexity of multithreaded programming. Existing data race detectors require large amounts of metadata for each program variable to perform their analyses. The SLIMFAST system exploits the insight t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1a03a6d6aff5c45ba2d185e9cb985b7c
https://doi.org/10.1109/ipdps.2018.00093
https://doi.org/10.1109/ipdps.2018.00093
Publikováno v:
PLDI
GPU programming models enable and encourage massively parallel programming with over a million threads, requiring extreme parallelism to achieve good performance. Massive parallelism brings significant correctness challenges by increasing the possibi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3df876f571d9feab1949e2f3d5cf2ac1
https://doi.org/10.1145/3062341.3062342
https://doi.org/10.1145/3062341.3062342
Autor:
Viktor Vafeiadis, William Mansky, Chung-Kil Hur, Steve Zdancewic, Dmitri Garbuzov, Jeehoon Kang
Publikováno v:
PLDI
The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::89e7c7e6c3be2ddbe26513fa13cb6f88
https://doi.org/10.1145/2737924.2738005
https://doi.org/10.1145/2737924.2738005
Publikováno v:
GRAPHITE
Electronic Proceedings in Theoretical Computer Science, Vol 159, Iss Proc. GRAPHITE 2014, Pp 58-70 (2014)
Electronic Proceedings in Theoretical Computer Science, Vol 159, Iss Proc. GRAPHITE 2014, Pp 58-70 (2014)
Compiler optimizations, usually expressed as rewrites on program graphs, are a core part of all modern compilers. However, even production compilers have bugs, and these bugs are difficult to detect and resolve. The problem only becomes more complex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b84685aca91c13c79b5b136aa92ceab6
http://arxiv.org/abs/1407.7932
http://arxiv.org/abs/1407.7932