Zobrazeno 1 - 10
of 15
pro vyhledávání: '"Jérémie Koenig"'
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:1-31
Memory models play an important role in verified compilation of imperative programming languages. A representative one is the block-based memory model of CompCert---the state-of-the-art verified C compiler. Despite its success, the abstraction over m
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::68dac266e2f94c2d4471c638e08fca70
https://doi.org/10.1145/3498686
https://doi.org/10.1145/3498686
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2022, ⟨10.1145/3498703⟩
Proceedings of the ACM on Programming Languages, ACM, 2022, ⟨10.1145/3498703⟩
Proceedings of the ACM on Programming Languages, 2022, ⟨10.1145/3498703⟩
Proceedings of the ACM on Programming Languages, ACM, 2022, ⟨10.1145/3498703⟩
Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::08a165a1165f43b75c24df42caed9d38
https://doi.org/10.1145/3498703
https://doi.org/10.1145/3498703
Autor:
Ronghui Gu, Jieung Kim, Vilhelm Sjöberg, David Costanzo, Jérémie Koenig, Xiongnan (Newman) Wu, Hao Chen, Zhong Shao
Publikováno v:
Communications of the ACM. 62:89-99
Operating system (OS) kernels form the backbone of system software. They can have a significant impact on the resilience and security of today's computers. Recent efforts have demonstrated the feasibility of formally verifying simple general-purpose
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::32be2712fb89feb6b5114ed4be49471f
https://doi.org/10.1145/3356903
https://doi.org/10.1145/3356903
Autor:
Jérémie Koenig, Zhong Shao
Publikováno v:
PLDI
Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU designs to network protocols have b
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8f73cb490c3302dcf75079d01e17e0f5
https://doi.org/10.1145/3453483.3454097
https://doi.org/10.1145/3453483.3454097
Autor:
Zhong Shao, Jérémie Koenig
Publikováno v:
LICS
Formal methods have advanced to the point where the functional correctness of various large system components has been mechanically verified. However, the diversity of semantic models used across projects makes it difficult to connect these component
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a2e60fbfa15b09f8c7cbf3ff0db8c110
https://doi.org/10.1145/3373718.3394799
https://doi.org/10.1145/3373718.3394799
Autor:
David Costanzo, Hao Chen, Xiongnan (Newman) Wu, Tahina Ramananandro, Jérémie Koenig, Jieung Kim, Ronghui Gu, Vilhelm Sjöberg, Zhong Shao
Publikováno v:
PLDI
Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronizati
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::af77ea9afb03e9892000063d702dfd34
https://doi.org/10.1145/3296979.3192381
https://doi.org/10.1145/3296979.3192381
Publikováno v:
SOSP
Data center networks evolve as they serve customer traffic. When applying network changes, operators risk impacting customer traffic because the network operates at reduced capacity and is more vulnerable to failures and traffic variations. The impac
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0b5cd0b42dc12b8b2f66735e268c734c
https://doi.org/10.1145/3341301.3359664
https://doi.org/10.1145/3341301.3359664
Autor:
Yu Guo, Shu-Chun Weng, Jérémie Koenig, Zhong Shao, Tahina Ramananandro, Xiongnan (Newman) Wu, Haozhong Zhang, Ronghui Gu
Publikováno v:
POPL
Modern computer systems consist of a multitude of abstraction layers (e.g., OS kernels, hypervisors, device drivers, network protocols), each of which defines an interface that hides the implementation details of a particular set of functionality. Cl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8bc9af853deb44a62fc0b49c7e6474b1
https://doi.org/10.1145/2676726.2676975
https://doi.org/10.1145/2676726.2676975
Publikováno v:
CPP
Recent ground-breaking efforts such as CompCert have made a convincing case that mechanized verification of the compiler correctness for realistic C programs is both viable and practical. Unfortunately, existing verified compilers can only handle who
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c39f9215931770db67c772189847b512
https://doi.org/10.1145/2676724.2693167
https://doi.org/10.1145/2676724.2693167