I am a PhD student at the Faculty of Informatics, University of Lugano (Universita' della Svizzera Italiana). I am a member of Formal Verification and Security Lab of Prof. Natasha Sharygina.

Research interests: formal methods, software verification, model checking, decision procedures, static analysis, information security and application of verification techniques to software security.

Projects: As part of my Ph.D. research I am involved with the several projects. 1) "Detection of Security Flaws and Vulnerabilities by Guided Model Checking". In this project we apply bounded model checking to abstract models, obtained by the localized abstract-interpretation-based summarization of the program. SAT solvers are heavily used both in the summarization and model-checking steps. To improve the scalability of this approach I am interested in substituting SAT with SMT. For that I am also working in the 2) Formal Verification via Boolean and Theory Reasoning (SMT) project. Besides I participate in 3) The Synergy of Precise and Fast Abstractions project, where new abstraction/refinement techniques for the CEGAR framework are developed.

The tools I work on:
• Loopfrog — a static analyzer for ANSI-C programs
• OpenSMT — a compact and open-source SMT-solver

Publications:

• Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D: Loop Summarization and Termination Analysis. In: TACAS 2011 proceedings.
• Sharygina, N., Tonetta, S., Tsitovich, A.: An abstraction refinement approach combining precise and approximated techniques. International Journal on Software Tools for Technology Transfer (STTT), Springer, 2011 (in press).
• Bruttomesso, R.; Rollini, S.F.; Sharygina, N.; Tsitovich, A.: Flexible Interpolation with Local Proof Transformations. In: ICCAD 2010 proceedings.
• Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination Analysis with Compositional Transition Invariants. In: CAV 2010 proceedings.
• Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: TACAS 2010 proceedings.
• Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loopfrog: A Static Analyzer for ANSI-C Programs. In: ASE 2009 proceedings.
• Sharygina, N., Tonetta, S., Tsitovich, A.: The Synergy of Precise and Fast Abstractions for Program Verification. In: ACM SAC 2009 proceedings.
• Tsitovich, A.: Detection of Security Vulnerabilities using Guided Model Checking (extended abstract). In: Proceedings of ICLP 2008.
• Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop Summarization Using Abstract Transformers. In: Proceedings of ATVA 2008.
• Tsitovich A.: Control-flow Obfuscation Complexity Metrics Based on Graph Cyclomatic Complexity. In: Belarusian Engineering Academy Proceedings, 2005 #2(20)/1, pp.40-42 (in Russian).
• Tsitovich A.: Methods of Software Protection Based on Modern Obfuscation Technologies. In: Collection of materials of 61^st student scientific workshop of BSU, 17-20 of May 2004, in 3 parts, part 1, p. 212 (in Russian).

More details are available at the Lab's publications repository.

Teaching Activities

Teaching Assistant:
• Computer Aided Verification, Fall 2009
• Validation and Verification, Spring 2009
• Information Security and Privacy, Spring 2009
• Validation and Verification, Fall 2007 - Spring 2008
• Software Verification and Security, Fall 2007
• Automata and Formal Languages, Spring 2007
• Theory of Computation, Fall 2006

Also, I have several project for Master/Bachelor students willing to work with static anaylysis of the programs or with SMT-based decision procedures.

• Visualizing the jumps of LoopFrog
• Paralleling OpenSMT Towards Cloud Computing