Vilhelm Sjöberg

Publication Activity (10 Years)

Years Active: 2009-2024
Publications (10 Years): 11

Top Topics

Provably Correct

Declarative Programming

Top Venues

Proc. ACM Program. Lang.

Publications

Zhenyang Dai, Shuang Liu, Vilhelm Sjöberg, Xupeng Li, Yu Chen, Wenhao Wang, Yuekai Jia, Sean Noble Anderson, Laila Elbeheiry, Shubham Sondhi, Yu Zhang, Zhaozhong Ni, Shoumeng Yan, Ronghui Gu, Zhengyu He
Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor. ASPLOS (2) (2024)
Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao
Foundational Verification of Smart Contracts through Verified Compilation. CoRR (2024)
Daniel Britten, Vilhelm Sjöberg, Steve Reeves
Provably Correct Smart Contracts: An Approach using DeepSEA. SPLASH Companion (2022)
Kinnari Dave, Vilhelm Sjöberg, Xinyuan Sun
Towards Verified Price Oracles for Decentralized Exchange Protocols. FMBC@CAV (2021)
Xinyuan Sun, Shaokai Lin, Vilhelm Sjöberg, Jay Jie
How to Exploit a DeFi Project. Financial Cryptography Workshops (2021)
Daniel Britten, Vilhelm Sjöberg, Steve Reeves
Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper). FMBC@CAV (2021)
Vilhelm Sjöberg, Yuyang Sang, Shu-Chun Weng, Zhong Shao
DeepSEA: a language for certified system software. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, David Costanzo
Building certified concurrent OS kernels. Commun. ACM 62 (10) (2019)
Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro
Certified concurrent abstraction layers. PLDI (2018)
Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao
Safety and Liveness of MCS Lock - Layer by Layer. APLAS (2017)
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, David Costanzo
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. OSDI (2016)
Vilhelm Sjöberg, Stephanie Weirich
Programming up to Congruence. POPL (2015)
Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
Combining proofs and programs in a dependently typed language. POPL (2014)
Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn
Equational reasoning about programs with general recursion and call-by-value semantics. PLPV (2012)
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems MSFP (2012)
Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
Step-Indexed Normalization for a Language with General Recursion MSFP (2012)
Peter-Michael Osera, Vilhelm Sjöberg, Steve Zdancewic
Dependent interoperability. PLPV (2012)
Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich
Dependent types and program equivalence. POPL (2010)
Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
Termination Casts: A Flexible Approach to Termination with General Recursion PAR (2010)
Vilhelm Sjöberg, Aaron Stump
Equality, Quasi-Implicit Products, and Large Eliminations ITRS (2010)
Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
Termination Casts: A Flexible Approach to Termination with General Recursion. PAR@ITP (2010)
Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, Steve Zdancewic
Reactive noninterference. CCS (2009)