About me

I obtained my PhD from ETHZ in 2018, at the Secure, Reliable, and Intelligent Systems Lab, supervised by Prof. Martin Vechev. My PhD research focused on static analysis techniques for relaxed memory models and software security. You can find my new web page at andreidan.net.

Conference Papers

2021

Scalable Polyhedral Verification of Recurrent Neural Networks
Wonryong Ryou, Jiayu Chen, Mislav Balunović, Gagandeep Singh, Andrei Dan, Martin Vechev
CAV 2021

2018

Securify: Practical Security Analysis of Smart Contracts
Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, Martin Vechev
ACM CCS 2018
Automatic Verification of RMA Programs via Abstraction Extrapolation
Cedric Baumann, Andrei Marian Dan, Yuri Meshman, Torsten Hoefler, Martin Vechev
VMCAI 2018

2017

Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts
Andrei Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin, Martin Vechev
CAV 2017

2016

Modeling and Analysis of Remote Memory Access Programming
Andrei Dan, Patrick Lam, Torsten Hoefler, Martin Vechev
ACM OOPSLA 2016

2015

Effective Abstractions for Verification under Relaxed Memory Models
Andrei Dan, Yuri Meshman, Martin Vechev, Eran Yahav
VMCAI 2015

2014

Synthesis of Memory Fences via Refinement Propagation
Yuri Meshman, Andrei Dan, Martin Vechev, Eran Yahav
SAS 2014

2013

Predicate Abstraction for Relaxed Memory Models
Andrei Dan, Yuri Meshman, Martin Vechev, Eran Yahav
Static Analysis Symposium (SAS) 2013

Journal Paper

Effective Abstractions for Verification under Relaxed Memory Models
Andrei Marian Dan, Yuri Meshman, Martin Vechev, Eran Yahav
Computer Languages (COMLAN), March 2016. Submitted June 2015. Invited paper.

Education

ETH Zurich, 2012–2018
PhD in Computer Science

EPF Lausanne, 2010–2012
MSc in Computer Science

Ecole Polytechnique Paris, 2008–2010
Engineer Diploma, X07

Polytechnic University of Bucharest, 2005–2009
BSc in Computer Science

Internship

Samsung Research America, Mountain View, 2016.
Finding Fix Locations for CFL-Reachability Analyses via Minimum Cuts. Supervisors: Manu Sridharan and Satish Chandra.

IBM Research, Zurich, 2012.
Master thesis on High-performance Solid-state Enterprise Storage Systems. Supervisor: Roman Pletka.

SRI International, Menlo Park, US, 2010.
Develop a verified SAT trace checker in PVS. Supervisor: Natarajan Shankar.

Awards

Distinguished Paper Award at OOPSLA 2016
ACM SIGPLAN Travel Grant for OOPSLA 2016
EPF Lausanne excellence scholarship - 2010
Eiffel excellence scholarship (French Ministry of Foreign Affairs) - 2008

Service

EASE 2019 - Program Committee Member

OOPSLA 2014 Artifacts Evaluation - Committee Member

Teaching Assistant

Program Analysis - graduate course, 4 ECTS.
Fall 2013, Spring 2015

Big Data - graduate course, 6 ECTS.
Fall 2014

Software Architecture and Engineering - undergraduate course, 8 ECTS.
Spring 2014, Spring 2016, Spring 2017

Seminars and Summer Schools

Dagstuhl Seminar: Concurrency with Weak Memory Models
November 2016, Schloss Dagstuhl, Germany.

NATO International Summer School - Software Systems Safety
August 2013, Marktoberdorf, Germany.

Alpine Verification Meeting (AVM)
May 2013, Trento, Italy.

Verification Technology, Systems & Applications (VTSA)
September 2012, Saarbrücken, Germany.