Follow
Tej Chajed
Title
Cited by
Cited by
Year
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
3402015
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
1032013
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
972019
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
892017
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
872019
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
472015
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
462021
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
352018
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
282018
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
232022
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
202019
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
182017
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
142024
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
102020
Oort: User-centric cloud storage with global queries
T Chajed, J Gjengset, MF Kaashoek, J Mickens, R Morris, N Zeldovich
82016
Verifying a concurrent, crash-safe filesystem with sequential reasoning (Research Statement)
T Chajed
5*2021
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
42024
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
42023
Verifying an I/O-concurrent file system
T Chajed
Massachusetts Institute of Technology, 2017
42017
Inductive invariants that spark joy: using invariant taxonomies to streamline distributed protocol proofs
TN Zhang, T Hance, T Chajed, M Kapritsos, B Parno
Proceedings of the 18th USENIX Conference on Operating Systems Design and …, 2024
12024
The system can't perform the operation now. Try again later.
Articles 1–20