Amir(hossein) Vakili's homepage

My name is Amir Vakili, and I'm a Postdoctoral Fellow at Electrical & Computer Engineering department, University of Waterloo, under supervision of Prof. Mark Aagaard and Prof. Guang Gong. Currently, I'm working on applications of formal methods in security and cryptography.

I'm interested in applying formal methods, advanced mathematical techniques based on logic, to discover security and safety flaws in systems. These technologies are applicable to both software and hardware systems. The techniques that I develop utilize automatic verification technologies, such as model checkers and SMT solvers, to provide fast and accurate feedback to designers. For more information about my research, please check out my publications, or contact me via email.

Last Update: 15 Nov 2016

Profiles

• Google Scholar
• DBLP

PhD Thesis

Amirhossein Vakili, Temporal Logic Model Checking as Automated Theorem Proving, Cheriton School of Computer Science, University of Waterloo, Jan 2016.

Refereed

• Amirhossein Vakili and Nancy A. Day, Finite Model Finding Using the Logic of Equality with Uninterpreted Functions, FM'16, Nov 2016.


• Nancy A. Day and Amirhossein Vakili, Representing Behavioural Models with Rich Control Structures in SMT-LIB, MiSE'16, May 2016, ICSE'16 workshop on Modelling in Software Engineering.


• Amirhossein Vakili and Nancy A. Day, Verifying CTL-Live Properties of Infinite State Models using an SMT Solver, FSE'14, Nov 2014.


• Amirhossein Vakili and Nancy A. Day, Reducing CTL-Live Model Checking to First-Order Logic Validity Checking, FMCAD'14, Oct 2014, short paper.


• Amirhossein Vakili and Nancy A. Day, Temporal Logic Model Checking in Alloy, ABZ'12, Jun 2012, 3rd conference on ASM, Alloy, B and Z.


• Amirhossein Vakili and Nancy A. Day, Avestan: A Declarative Modeling Language Based on SMT-LIB, MiSE'12, Jun 2012, ICSE'12 workshop on Modelling in Software Engineering.


• Amirhossein Vakili and Nancy A. Day, Using Model Checking to Analyze Static Properties of Declarative Models, ASE'11, Nov 2011, short paper.


• Amirhossein Vakili, Analyzing Temporal Properties of Abstract Models, ASE'11, Nov 2011, Doctoral Symposium.

Non-refereed

• Nancy A. Day and Amirhossein Vakili, Representing Behavioural Models with Rich Control Structures in SMT-LIB, Cheriton School of Computer Science, University of Waterloo, Technical Report CS-2015-14, 2015.


• Amirhossein Vakili and Nancy A. Day, Verifying CTL-live Properties of Infinite State Models using an SMT solver (Version 1), Cheriton School of Computer Science, University of Waterloo, Technical Report CS-2014-10, 2014.


• Amirhossein Vakili and Nancy A. Day, Reducing CTL-Live Model Checking to Semantic Entailment in First-Order Logic (Version 1), Cheriton School of Computer Science, University of Waterloo, Technical Report CS-2014-05, 2014.


• Amirhossein Vakili and Nancy A. Day, Using Model Checking to Analyze Static Properties of Declarative Models: Extended Version, Cheriton School of Computer Science, University of Waterloo, Technical Report CS-2011-22, 2011.

Coming soon!

Instructor

- SE212: Logic and Computation (Fall 2014)

Guest Lecturer

- CS365 (15 and 17 Feb 2011)

Instructional Apprentice (IA)

- CS245/SE212 (Fall 2011, Winter 2012, Fall 2012 - Fall 2013)

Teaching Assistant (TA)

- CS365 (Winter 2011)

- CS360 (Winter 2010-Fall 2010, Spring 2011)

- CS135 (Fall 2009, Winter 2011)

Amirhossein Vakili, PhD

Electrical & Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada, N2L 3G1

office: EIT 4139
phone: +1 519 888 4567 x37471
email: ........@uwaterloo.ca