Vilhelm Sjöberg

22 papers A* 6B 1Journal 3Unranked 12

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