I am currently a PhD candidate in computer science at Formal Verification and Security Lab under supervision of Prof. Natasha Sharygina. My research interests are in automated symbolic model-checking, incremental verification of large-scale programs, and SAT/SMT solving. Recently I've been working on developing a bounded model checker designed to incrementally verify software while it is being gradually changed.
PhD Candidate in Computer ScienceUniversità della Svizzera italiana (USI Lugano), Lugano, Switzerland, Mar 2016 - present
M.Sc in Information Technology/ Secure CommunicationsIran University of Science & Technology (IUST), Tehran, Iran,
B.Sc Electrical Engineering/ ElectronicsZanjan University, Zanjan, Iran,
- Aug 2017
- SAT/SMT & Symbolic Computation Summer School · MPI Informatics, Saarbrücken, Germany
- Aug 2016
- Dependable Software Systems Engineering · Marktoberdorf Summer School, Germany
- Oct 2016
- Workshop on Software Correctness and Reliability · ETH Zürich
- Jun 2016
- SAT/SMT & Automated Reasoning Summer School · Lisbon, Portugal
- Spring 2016
- Computer Aided Verification · Università della Svizzera italiana, Lugano, CH
Incremental Verification by SMT-based Summary Repair
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina.
Function Summarization Modulo Theories
S. Asadi, M. Blicha, G. Fedyukovich,A. Hyvärinen, K. Even, N. Sharygina, H. Chockler.
1In the 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), 2018.
Lattice-Based Refinement in Bounded Model Checking
K. Even, S. Asadi, A. Hyvärinen, H. Chockler, N. Sharygina
In 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2018.
Computing Exact Worst-Case Gas Consumption for Smart Contracts.
M. Marescotti, M. Blicha, A. Hyvärinen, S. Asadi, N. Sharygina.
In International Symposium on Leveraging Applications of Formal Methods ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018.
Theory Refinement for Program Verification
A. Hyvärinen S. Asadi, K. Even, G. Fedyukovich, H. Chockler, N. Sharygina.
In 20th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2017.
HiFrog: SMT-based Function Summarization for Software Verification.
L. Alt, S. Asadi, H. Chockler, K. Even, G. Fedyukovich, A. Hyvärinen, N. Sharygina
In 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017.
Duality-based interpolation for quantifier-free equalities and uninterpreted functions.
L. Alt, A. Hyvärinen, S. Asadi, N. Sharygina.
In Formal Methods in Computer-Aided Design (FMCAD), 2017
HiFrog: Interpolation-based Software Verification using Theory Refinement.
In FMCAD Student Forum, 2017.
Formal Security Analysis of Authentication in SNMPv3 Protocol by An Automated Tool.
S. Asadi, H. Shahhoseini
In Sixth International Symposium on Telecommunications (IST), 2012.
- Bachelor Projects · Università della Svizzera italiana, Lugano, CH
- Fall'18, Fall'19
- Software Design and Modelling · Università della Svizzera italiana, Lugano, CH
- SP'17, SP'18, SP'20
- Theory of Computation · Università della Svizzera italiana, Lugano, CH
- Fall'16, Fall'17
- Fundamentals of Informatics · Università della Svizzera italiana, Lugano, CH
Conference Talks & Invited Talks
- Aug 2018
- HiFrog: Interpolation-based Software Verification using Theory Refinement TACAS 2017 · Uppsala, Sweden
- Nov 2018
- Function Summarization Modulo Theories LPAR 2018 · Awassa, Ethiopia
- Sep 2017
- 11th Alpine Verification Meeting (AVM) · Visegrád, Hungary
- Jan 2013
- A survey on formal methods · Security Study Group (SSG) of IT organization of Iran
- Jan 2012
- Formal verification of security protocols · Iran Telecommunication Research Center (ITRC), Tehran, Iran
(Feb 2014 — May 2015) R&D Engineer at MAT IT-Solutions Tehran, Iran.
Applied Public Key Infrastructure solutions for digitalizing the existing travel documents
(Jan 2013 — Dec 2013) Researcher at Iran Telecommunication Research Center (ITRC) Tehran, Iran.
Our team offered road maps towards designing and implementing National Information Network
(Jul 2012 — Dec 2012) Intern at ICT Research Institute Tehran, Iran.
Contributed to formal evaluation and security assurance of network management protocols
Sub-reviewing ACM Journal of Computing Surveys (CSUR),
Sub-reviewing papers on international Conferences: CAV ('20, '19, '18); TACAS ('20, '18, '17); VMCAI ('20); SAT ('20,'19); FM ('19, '18, '16); AAAI ('19); FMCAD (20', '19, '18, '17); HVC ('17).
Sub-reviewing papers on international workshops: SMT('20), MARS('20)