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 | 336 | 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 | 104 | 2013 |
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 | 94 | 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 | 87 | 2019 |
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 | 87 | 2017 |
GoJournal: a verified, concurrent, crash-safe journaling system T Chajed, J Tassarotti, M Theng, R Jung, MF Kaashoek, N Zeldovich 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2021 | 45 | 2021 |
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 | 42 | 2015 |
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 | 34 | 2018 |
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 | 28 | 2018 |
Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning T Chajed, J Tassarotti, M Theng, MF Kaashoek, N Zeldovich 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2022 | 24 | 2022 |
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 | 20 | 2019 |
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 | 17 | 2017 |
Anvil: Verifying liveness of cluster management controllers X Sun, W Ma, JT Gu, Z Ma, T Chajed, J Howell, A Lattuada, O Padon, ... 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2024 | 15 | 2024 |
Verifying concurrent Go code in Coq with Goose T Chajed, J Tassarotti, MF Kaashoek, N Zeldovich Proceedings of the 6th International Workshop on Coq for Programming …, 2020 | 11 | 2020 |
Verus: A practical foundation for systems verification A Lattuada, T Hance, J Bosamiya, M Brun, C Cho, H LeBlanc, ... Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles …, 2024 | 8 | 2024 |
Oort: User-centric cloud storage with global queries T Chajed, J Gjengset, MF Kaashoek, J Mickens, R Morris, N Zeldovich | 7 | 2016 |
Verifying a concurrent, crash-safe filesystem with sequential reasoning (Research Statement) T Chajed | 5* | 2021 |
Beyond isolation: OS verification as a foundation for correct applications M Brun, R Achermann, T Chajed, J Howell, G Zellweger, A Lattuada Proceedings of the 19th Workshop on Hot Topics in Operating Systems, 158-165, 2023 | 4 | 2023 |
Verifying an I/O-concurrent file system T Chajed Massachusetts Institute of Technology, 2017 | 4 | 2017 |
Shadow filesystems: Recovering from filesystem runtime errors via robust alternative execution J Liu, X Hao, A Arpaci-Dusseau, R Arpaci-Dusseau, T Chajed Proceedings of the 16th ACM Workshop on Hot Topics in Storage and File …, 2024 | 2 | 2024 |