Predicate Abstraction for Relaxed Memory Models. - Andrei Marian Dan; Yuri Meshman; Martin T. Vechev; Eran Yahav (SAS, 2013)

Synthesis of Memory Fences via Refinement Propagation. - Yuri Meshman; Andrei Marian Dan; Martin T. Vechev; Eran Yahav (SAS, 2014)

Modeling and analysis of remote memory access programming. - Andrei Marian Dan; Patrick Lam 001; Torsten Hoefler; Martin T. Vechev (OOPSLA, 2016)

Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts. - Andrei Marian Dan; Manu Sridharan; Satish Chandra 001; Jean-Baptiste Jeannin; Martin T. Vechev (CAV (2), 2017)

Effective abstractions for verification under relaxed memory models. - Andrei Marian Dan; Yuri Meshman; Martin T. Vechev; Eran Yahav (Comput. Lang. Syst. Struct., 2017)

Securify: Practical Security Analysis of Smart Contracts. - Petar Tsankov; Andrei Marian Dan; Dana Drachsler-Cohen; Arthur Gervais; Florian Bünzli; Martin T. Vechev (CCS, 2018)

Automatic Verification of RMA Programs via Abstraction Extrapolation. - Cedric Baumann; Andrei Marian Dan; Yuri Meshman; Torsten Hoefler; Martin T. Vechev (VMCAI, 2018)

Fast and Effective Robustness Certification for Recurrent Neural Networks. - Wonryong Ryou; Jiayu Chen; Mislav Balunovic; Gagandeep Singh 001; Andrei Marian Dan; Martin T. Vechev (CoRR, 2020)

Scalable Polyhedral Verification of Recurrent Neural Networks. - Wonryong Ryou; Jiayu Chen; Mislav Balunovic; Gagandeep Singh 001; Andrei Marian Dan; Martin T. Vechev (CAV (1), 2021)