Skip to main content

Temesghen Kahsai

Senior Systems Scientist, CyLab and Carnegie Mellon Silicon Valley


Temesghen Kahsai

Research Areas

Trustworthy Computing Platforms and Devices, Mobility

Cross Cutting Thrusts

Formal Methods
Software Security


Temesghen Kahsai is a Research Scientist at NASA Ames employed by CMU, where he has been a member of the Robust Software Engineering group since 2013. 

His research interests are in the automated software analysis for complex safety and mission critical software. From 2012 to 2013, he was a software engineer at Skype (Microsoft), where he worked on the mobile core division. From 2010 to 2012, he was a postdoctoral research scholar at the University of Iowa, where he worked on scaling SMT-based model checking. He is currently leading three research projects funded by NASA and NSF on contract-based verification of outsourced flight critical systems, compositional analysis of heterogeneous software protocol stack and credible auto-coding of embedded systems. He is also a co-investigator in a DARPA-funded research project on ’space/time analysis for cybersecurity’.

Kahsai's professional home page can be accessed at:


PhD, 2011. Computer Science, Swansea University, Wales, UK.
MS, 2006. Computer Science, University of Udine, Italy.
BS, 2003. Computer Science, University of Udine, Italy.


"Verifying the Safety of a Flight-Critical System". G Brat, D Bushnell, M Davies, D Giannakopoulou, F Howar, T Kahsai. FM 2015: Formal Methods, 308-324. 

"Algorithmic logic-based verification". A Gurfinkel, T Kahsai, JA Navas. ACM SIGLOG News 2 (2), 29-38. 2015.

"SeaHorn: A framework for verifying C programs (Competition contribution)". A Gurfinkel, T Kahsai, JA Navas. Tools and Algorithms for the Construction and Analysis of Systems, 447-450 4 2015

"Synthesizing Modular Invariants for Synchronous Code". PL Garoche, A Gurfinkel, T Kahsai. arXiv preprint arXiv:1412.1152 2014

"Testing-Based Compiler Validation for Synchronous Languages". PL Garoche, F Howar, T Kahsai, X Thirioux. NASA Formal Methods, 246-251 2014

"Scalable and Accurate SMT-based Model Checking of Data Flow Systems". C Tinelli, T Kahsai, C Sticksel. IOWA UNIV IOWA CITY 2013

"Incremental invariant generation using logic-based automatic abstract transformers". PL Garoche, T Kahsai, C Tinelli. NASA Formal Methods, 139-154 10 2013