Sepideh Asadi
PhD Student
- Address:
-
Università della Svizzera italiana (USI Lugano),
Faculty of Informatics, East Campus, Sector D,
Office D4.16, Via la Santa 1, CH-6962 Lugano-Viganello, Switzerland. - Phone:
- +41 58 666 4455 ext. 2306
- Email:
-
asadis take this out< at > usi.ch
- Links:
- ORCiD, GitHub, Google Scholar, DBLP, LinkedIn, CV
About me
I am a final year PhD student in computer science at USI Lugano Formal Verification and Security Lab advised by Prof. Natasha Sharygina. I am broadly interested in software verification with a specific focus on automated symbolic model-checking, incremental verification of C programs, and SAT/SMT solving. I have contributed to developing of UpProver, a bounded model checker for incrementally verifying software revisions. I have also contributed in design of HiFrog, an SMT-based BMC with theory refinement algorithm.
Education
PhD Student in Computer Science
Università della Svizzera italiana (USI Lugano), Lugano, Switzerland, Mar 2016 - presentM.Sc in Information Technology/ Secure Communications
Iran University of Science & Technology (IUST), Tehran, Iran,B.Sc Electrical Engineering/ Electronics
Zanjan University, Zanjan, Iran,Further Education
- Aug 2018
- SAT/SMT/AR Summer School School of Computer Science at the University of Manchester, UK
- 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
Publications
-
Farkas-Based Tree-Interpolation
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina.
In 27th Static Analysis Symposium (SAS), 2020. -
Incremental Verification by SMT-based Summary Repair
S. Asadi, M. Blicha, A. Hyvärinen, G. Fedyukovich, N. Sharygina.
In Formal Methods in Computer-Aided Design (FMCAD), 2020. -
Function Summarization Modulo Theories
S. Asadi, M. Blicha, G. Fedyukovich,A. Hyvärinen, K. Even, N. Sharygina, H. Chockler.
In 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), 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 -
Formal Security Analysis of Authentication in SNMPv3 Protocol by An Automated Tool.
S. Asadi, H. Shahhoseini
In Sixth International Symposium on Telecommunications (IST), 2012. -
HiFrog: Interpolation-based Software Verification using Theory Refinement.
In FMCAD Student Forum, 2017.
Poster
Academic Experience
Teaching Assistant
- Fall21
- Computer Aided Verification Università della Svizzera italiana, Lugano, CH
- Fall18, Fall19, Fall20
- Software Design and Modelling Università della Svizzera italiana, Lugano, CH
- SP19
- Bachelor Projects Università della Svizzera italiana, Lugano, CH
- SP17, SP18, SP20, SP21
- Theory of Computation Università della Svizzera italiana, Lugano, CH
- Fall16, Fall17, Fall21
- Fundamentals of Informatics Università della Svizzera italiana, Lugano, CH
Conference Talks & Invited Talks
- Jun 2021
-
Demo labs for SMT-based approach for bounded model checking,
SRI summer school on formal techniques 2021
Online
[ Lab 1 | Lab 2] - Nov 2020
-
Farkas-Based Tree Interpolation,
SAS 2020
Chicago, USAOnline
[ slide | video] - Sep 2020
-
UpProver: Incremental Verification by SMT-based Summary Repair,
FMCAD 2020
Online
[ slide | short-video | full-video ] - Nov 2018
-
Function Summarization Modulo Theories,
LPAR 2018
Awassa, Ethiopia
[ slide ] - Sep 2017
-
11th Alpine Verification Meeting (AVM)
Visegrád, Hungary
[ slide ] - Apr 2017
- HiFrog: Interpolation-based Software Verification using Theory Refinement, TACAS 2017 Uppsala, Sweden
- 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
Sub-reviewing
-
(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 ('21, '20, '19, '18); TACAS ('21, '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)
Work Experience
Personal
-
Here is a little bit about me ...