Verifying Equivalence of Spark Programs. - Shelly Grossman; Sara Cohen; Shachar Itzhaky; Noam Rinetzky; Mooly Sagiv (CAV (2), 2017)

SBFT: a Scalable Decentralized Trust Infrastructure for Blockchains. - Guy Golan-Gueta; Ittai Abraham; Shelly Grossman; Dahlia Malkhi; Benny Pinkas; Michael K. Reiter; Dragos-Adrian Seredinschi; Orr Tamir; Alin Tomescu (CoRR, 2018)

Online detection of effectively callback free objects with applications to smart contracts. - Shelly Grossman; Ittai Abraham; Guy Golan-Gueta; Yan Michalevsky; Noam Rinetzky; Mooly Sagiv; Yoni Zohar (Proc. ACM Program. Lang., 2018)

SBFT: A Scalable and Decentralized Trust Infrastructure. - Guy Golan-Gueta; Ittai Abraham; Shelly Grossman; Dahlia Malkhi; Benny Pinkas; Michael K. Reiter; Dragos-Adrian Seredinschi; Orr Tamir; Alin Tomescu (DSN, 2019)

Taming callbacks for smart contract modularity. - Elvira Albert; Shelly Grossman; Noam Rinetzky; Clara Rodríguez-Núñez; Albert Rubio; Mooly Sagiv (Proc. ACM Program. Lang., 2020)

Phoenix: A Formally Verified Regenerating Vault. - Uri Kirstein; Shelly Grossman; Michael Mirkin; James Wilcox 004; Ittay Eyal; Mooly Sagiv (CoRR, 2021)

Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. - Elvira Albert; Shelly Grossman; Noam Rinetzky; Clara Rodríguez-Núñez; Albert Rubio; Mooly Sagiv (IEEE Trans. Dependable Secur. Comput., 2023)

Practical Verification of Smart Contracts using Memory Splitting. - Shelly Grossman; John Toman; Alexander Bakst; Sameer Arora; Mooly Sagiv; Chandrakana Nandi (Proc. ACM Program. Lang., 2024)