Tej Chajed
Tej Chajed
MIT CSAIL
Verified email at mit.edu - Homepage
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
2012015
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
812013
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
362017
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
202015
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
122019
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
122018
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
102017
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
92019
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
92019
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
92018
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
52019
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
52013
Verifying an I/O-concurrent file system
T Chajed
Massachusetts Institute of Technology, 2017
42017
Oort: user-centric cloud storage with global queries
T Chajed, J Gjengset, MF Kaashoek, J Mickens, R Morris, N Zeldovich
32016
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
12020
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
The system can't perform the operation now. Try again later.
Articles 1–20