I did my PhD in software static analysis at the Faculty of Informatics, University of Lugano (Universita' della Svizzera Italiana). I was a member of Formal Verification and Security Lab.

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

Projects

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