| Using Crash Hoare logic for certifying the FSCQ file system H Chen, D Ziegler, T Chajed, A Chlipala, MF Kaashoek, N Zeldovich Proceedings of the 25th Symposium on Operating Systems Principles, 18-37, 2015 | 201 | 2015 |
| Natjam: Design and evaluation of eviction policies for supporting priorities and deadlines in mapreduce clusters B Cho, M Rahman, T Chajed, I Gupta, C Abad, N Roberts, P Lin Proceedings of the 4th annual Symposium on Cloud Computing, 1-17, 2013 | 81 | 2013 |
| Verifying a high-performance crash-safe file system using a tree specification H Chen, T Chajed, A Konradi, S Wang, A İleri, A Chlipala, MF Kaashoek, ... Proceedings of the 26th Symposium on Operating Systems Principles, 270-286, 2017 | 36 | 2017 |
| Amber: Decoupling user data from web applications T Chajed, J Gjengset, J Van Den Hooff, MF Kaashoek, J Mickens, ... 15th Workshop on Hot Topics in Operating Systems (HotOS {XV}), 2015 | 20 | 2015 |
| Verifying concurrent, crash-safe systems with Perennial T Chajed, J Tassarotti, MF Kaashoek, N Zeldovich Proceedings of the 27th ACM Symposium on Operating Systems Principles, 243-258, 2019 | 12 | 2019 |
| Verifying concurrent software using movers in CSPEC T Chajed, MF Kaashoek, B Lampson, N Zeldovich 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2018 | 12 | 2018 |
| Certifying a file system using crash hoare logic: correctness in the presence of crashes T Chajed, H Chen, A Chlipala, MF Kaashoek, N Zeldovich, D Ziegler Communications of the ACM 60 (4), 75-84, 2017 | 10 | 2017 |
| Yodel: strong metadata security for voice calls D Lazar, Y Gilad, N Zeldovich Proceedings of the 27th ACM Symposium on Operating Systems Principles, 211-224, 2019 | 9 | 2019 |
| Everparse: Verified secure zero-copy parsers for authenticated message formats T Ramananandro, A Delignat-Lavaud, C Fournet, N Swamy, T Chajed, ... 28th {USENIX} Security Symposium ({USENIX} Security 19), 1465-1482, 2019 | 9 | 2019 |
| Proving confidentiality in a file system using DiskSec A Ileri, T Chajed, A Chlipala, MF Kaashoek, N Zeldovich 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2018 | 9 | 2018 |
| Argosy: Verifying layered storage systems with recovery refinement T Chajed, J Tassarotti, MF Kaashoek, N Zeldovich Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019 | 5 | 2019 |
| Natjam: Eviction policies for supporting priorities and deadlines in MapReduce clusters I Gupta, B Cho, MR Rahman, T Chajed, CL Abad, N Roberts, P Lin | 5 | 2013 |
| Verifying an I/O-concurrent file system T Chajed Massachusetts Institute of Technology, 2017 | 4 | 2017 |
| Oort: user-centric cloud storage with global queries T Chajed, J Gjengset, MF Kaashoek, J Mickens, R Morris, N Zeldovich | 3 | 2016 |
| Verifying concurrent Go code in coq with Goose T Chajed, J Tassarotti, F Kaashoek, N Zeldovich The Sixth International Workshop on Coq for Programming Languages, CoqPL 2020, 2020 | 1 | 2020 |
| Optimizations for performant multiverse databases JM Bredenberg Massachusetts Institute of Technology, 2020 | | 2020 |
| Characterizing Accuracy and Performance Tradeoffs in Graph Sampling for Graph Property Computations T Chajed, I Gupta | | 2014 |
| Proving Confidentiality in a File System Using DiskSec (Poster# 2) AM İleri, T Chajed, A Chlipala, F Kaashoek, N Zeldovich | | |
| Extending a verified file system with concurrency T Chajed, A Chlipala, MF Kaashoek, N Zeldovich | | |
| Recursively invoking Linnaeus: A Taxonomy for Naming Systems NODF Circumscription | | |
Nickolai ZeldovichVerified email at csail.mit.edu
