In 2019, I joined the digital health startup BrightInsight in a quest to make the leading regulated cloud platform.

Between 2011 and 2019, I was helping R&D team at Sonova to create a stellar digital patient journey ‐ from "no calibration required" online hearing test to realtime remote hearing instrument fitting.

Industrial interests: digital health, software as a medical device (SaMD), cloud architectures.

Prior to joining R&D team at Sonova, I did a Ph.D. 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 have worked on:
• Loopfrog — a static analyzer for ANSI-C programs
• OpenSMT — a compact and open-source SMT-solver

Publications:

• Rollini, S.F.; Bruttomesso, R.; Sharygina, N.; Tsitovich, A.: Resolution proof transformation for compression and interpolation. Formal Methods in System Design (FMSD), Journal, Volume 45, issue 1, Springer, 2014.
• Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop Summarization using State and Transition Invariants. Formal Methods in System Design (FMSD), Journal, Volume 42, issue 3, Springer, 2013.
• 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, 2012.
• Tsitovich, A.: Scalable Abstractions for Efficient Security Checks, Ph.D. Thesis. Faculty of Informatics, University of Lugano, 2011.
• Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D: Loop Summarization and Termination Analysis. In: TACAS 2011 proceedings.
• 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:
• Software Atelier IV (Scala/Lift), Spring 2011
• 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