Foundational Certified Code in a Metalogical Framework. - Karl Crary; Susmit Sarkar (CADE, 2003)

Small Proof Witnesses for LF. - Susmit Sarkar; Brigitte Pientka; Karl Crary (ICLP, 2005)

Foundational certified code in the Twelf metalogical framework. - Karl Crary; Susmit Sarkar (ACM Trans. Comput. Log., 2008)

The semantics of power and ARM multiprocessor machine code. - Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli (DAMP, 2009)

The semantics of x86-CC multiprocessor machine code. - Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli; Scott Owens; Tom Ridge; Thomas Braibant; Magnus O. Myreen; Jade Alglave (POPL, 2009)

A Better x86 Memory Model: x86-TSO. - Scott Owens; Susmit Sarkar; Peter Sewell (TPHOLs, 2009)

Fences in Weak Memory Models. - Jade Alglave; Luc Maranget; Susmit Sarkar; Peter Sewell (CAV, 2010)

x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. - Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (Commun. ACM, 2010)

Ott: Effective tool support for the working semanticist. - Peter Sewell; Francesco Zappa Nardelli; Scott Owens; Gilles Peskine; Thomas Ridge; Susmit Sarkar; Rok Strnisa (J. Funct. Program., 2010)

Understanding POWER multiprocessors. - Susmit Sarkar; Peter Sewell; Jade Alglave; Luc Maranget; Derek Williams (PLDI, 2011)

Mathematizing C++ concurrency. - Mark Batty; Scott Owens; Susmit Sarkar; Peter Sewell; Tjark Weber (POPL, 2011)

Nitpicking C++ concurrency. - Jasmin Christian Blanchette; Tjark Weber; Mark Batty; Scott Owens; Susmit Sarkar (PPDP, 2011)

Litmus: Running Tests against Hardware. - Jade Alglave; Luc Maranget; Susmit Sarkar; Peter Sewell (TACAS, 2011)

An Axiomatic Memory Model for POWER Multiprocessors. - Sela Mador-Haim; Luc Maranget; Susmit Sarkar; Kayvan Memarian; Jade Alglave; Scott Owens; Rajeev Alur; Milo M. K. Martin; Peter Sewell; Derek Williams (CAV, 2012)

Synchronising C/C++ and POWER. - Susmit Sarkar; Kayvan Memarian; Scott Owens; Mark Batty; Peter Sewell; Luc Maranget; Jade Alglave; Derek Williams (PLDI, 2012)

Clarifying and compiling C/C++ concurrency: from C++11 to POWER. - Mark Batty; Kayvan Memarian; Scott Owens; Susmit Sarkar; Peter Sewell (POPL, 2012)

Fences in weak memory models (extended version). - Jade Alglave; Luc Maranget; Susmit Sarkar; Peter Sewell (Formal Methods Syst. Des., 2012)

Fast RMWs for TSO: semantics and implementation. - Bharghava Rajaram; Vijay Nagarajan; Susmit Sarkar; Marco Elver (PLDI, 2013)

Timing Properties and Correctness for Structured Parallel Programs on x86-64 Multicores. - Kevin Hammond; Christopher Brown 002; Susmit Sarkar (FOPARA, 2015)

An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. - Kathryn E. Gray; Gabriel Kerneis; Dominic P. Mulligan; Christopher Pulte; Susmit Sarkar; Peter Sewell (MICRO, 2015)

Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms. - David Castro 006; Kevin Hammond; Susmit Sarkar (ICFP, 2016)

Modelling the ARMv8 architecture, operationally: concurrency and ISA. - Shaked Flur; Kathryn E. Gray; Christopher Pulte; Susmit Sarkar; Ali Sezgin; Luc Maranget; Will Deacon; Peter Sewell (POPL, 2016)

Fence Placement for Legacy Data-Race-Free Programs via Synchronization Read Detection. - Andrew J. McPherson; Vijay Nagarajan; Susmit Sarkar; Marcelo Cintra (ACM Trans. Archit. Code Optim., 2016)

Verification of a lazy cache coherence protocol against a weak memory model. - Christopher J. Banks; Marco Elver; Ruth Hoffmann; Susmit Sarkar; Paul B. Jackson; Vijay Nagarajan (FMCAD, 2017)

Mixed-size concurrency: ARM, POWER, C/C++11, and SC. - Shaked Flur; Susmit Sarkar; Christopher Pulte; Kyndylan Nienhuis; Luc Maranget; Kathryn E. Gray; Ali Sezgin; Mark Batty; Peter Sewell (POPL, 2017)

Memory Consistency Models using Constraints. - Ruth Hoffmann; Özgür Akgün; Susmit Sarkar (CoRR, 2018)

Automatically deriving cost models for structured parallel processes using hylomorphisms. - David Castro 006; Kevin Hammond; Susmit Sarkar; Yasir Alguwaifli (Future Gener. Comput. Syst., 2018)

Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. - Christopher Pulte; Shaked Flur; Will Deacon; Jon French; Susmit Sarkar; Peter Sewell (Proc. ACM Program. Lang., 2018)

Fast and Correct Load-Link/Store-Conditional Instruction Handling in DBT Systems. - Martin Kristien; Tom Spink; Brian Campbell 001; Susmit Sarkar; Ian Stark; Björn Franke; Igor Böhm; Nigel P. Topham (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Compound Memory Models. - Andrés Goens; Soham Chakraborty 001; Susmit Sarkar; Sukarn Agarwal; Nicolai Oswald; Vijay Nagarajan (Proc. ACM Program. Lang., 2023)

Towards Specification-Guarded Refactoring. - Adam D. Barwell; Christopher Brown 002; Susmit Sarkar (LOPSTR, 2024)