CSolve: Verifying C with Liquid Types. - Patrick Maxim Rondon; Alexander Bakst; Ming Kawaguchi; Ranjit Jhala (CAV, 2012)

Deterministic parallelism via liquid effects. - Ming Kawaguchi; Patrick Maxim Rondon; Alexander Bakst; Ranjit Jhala (PLDI, 2012)

Bounded refinement types. - Niki Vazou; Alexander Bakst; Ranjit Jhala (ICFP, 2015)

Predicate Abstraction for Linked Data Structures. - Alexander Bakst; Ranjit Jhala (VMCAI, 2016)

Verifying distributed programs via canonical sequentialization. - Alexander Bakst; Klaus von Gleissenthall; Rami Gökhan Kici; Ranjit Jhala (Proc. ACM Program. Lang., 2017)

Sequentialization and Synchronization for Distributed Programs. - Alexander Bakst (2017)

Weird Machines as Insecure Compilation. - Jennifer Paykin; Eric Mertens; Mark Tullsen; Luke Maurer; Benoît Razet; Alexander Bakst; Scott Moore 001 (CoRR, 2019)

Pretend synchrony: synchronous verification of asynchronous distributed programs. - Klaus von Gleissenthall; Rami Gökhan Kici; Alexander Bakst; Deian Stefan; Ranjit Jhala (Proc. ACM Program. Lang., 2019)

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)