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 - present

M.Sc in Information Technology/ Secure Communications

Iran University of Science & Technology (IUST), Tehran, Iran, Jan 2013

B.Sc Electrical Engineering/ Electronics

Zanjan University, Zanjan, Iran, Oct 2008

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, Saarbrü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. Hyvärinen, G. Fedyukovich, N. Sharygina.
In 27th Static Analysis Symposium (SAS), 2020.
Incremental Verification by SMT-based Summary Repair
S. Asadi, M. Blicha, A. Hyvä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. Hyvä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. Hyvä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. Hyvärinen, S. Asadi, N. Sharygina.
In International Symposium on Leveraging Applications of Formal Methods (ISoLA), Industrial Practice, 2018.
Theory Refinement for Program Verification
A. Hyvä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. Hyvä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. Hyvä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.

Poster

HiFrog: Interpolation-based Software Verification using Theory Refinement.
In FMCAD Student Forum, 2017.

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, USA~~ Online
[ 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

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

(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

Personal

Here