Modularity for decidability of deductive verification with applications to distributed systems. - Marcelo Taube; Giuliano Losa; Kenneth L. McMillan; Oded Padon; Mooly Sagiv; Sharon Shoham; James R. Wilcox; Doug Woos (PLDI, 2018)

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. - Orr Tamir; Marcelo Taube; Kenneth L. McMillan; Sharon Shoham; Jon Howell; Guy Gueta; Mooly Sagiv (Proc. ACM Program. Lang., 2023)