NASA Logo, National Aeronautics and Space Administration

I am a research scientist with the Robust Software Engineering Group in the Intelligent Systems Division (Code TI), at NASA Ames Research Center, employed by Carnegie Mellon University.

My research interests are in the fields of automated analysis techniques for complex safety and mission critical systems.


  • 2014-2017: Principal investigator for the NASA funded project: Contract-based compositional verification for outsourced flight-critical systems.


Relevant publications

  • P-L Garoche, A. Gurfinkel, T. Kahsai. Synthesizing modular invariants for synchronous code. HCVS-2014, co-located with CAV-2014. To appear.
  • P-L Garoche, F. Howar, T. Kahsai, X. Thirioux. Testing-Based Compiler Validation for Synchronous Languages. NASA Formal Methods 2014. 246-251. 2014.
  • P-L. Garoche, T. Kahsai, C. Tinelli. Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers. NASA Formal Methods 2013. pp. 139-154. 2013 .
  • A. Gimblett, T. Kahsai, L. O'Reilly, M. Roggenbach On the whereabouts of CSP-CASL - A Survey. In Specification, Transformation, Navigation, Festschrift dedicated to Bernd Krieg-Bruckner, Bremen, 2013.
  • T. Kahsai, P-L. Garoche, Cesare Tinelli, M. Whalen. Incremental Verification with Mode Variable Invariants in State Machines. NASA Formal Methods 2012: pp. 388-402. 2012.
  • P-L. Garoche, T. Kahsai, C. Tinelli. Invariant stream generators using automatic abstract transformers based on a decidable logic. CoRR abs/1205.3758. 2012.
  • T. Kahsai, C. Tinelli. PKind: A parallel k-induction based model checker. PDMC 2011, co-located with CAV-2011. pp. 55-62. 201.
  • T. Kahsai, Y. Ge, C. Tinelli. Instantiation-Based Invariant Discovery. NASA Formal Methods 2011. pp.192-206. 2011.
  • T. Kahsai, G. Holland, M. Roggenbach, H. Schlingloff. Towards formal testing of jet engine Rolls-Royce BR725. In Proc. 18th Int. Conference on Concurrency, Specification and Programming, Krakow, Poland, 2009.
  • T. Kahsai, M. Roggenbach. Property preserving refinement notions for CSP-CASL. In A. Corradini and U. Montanari, editors, Recent Trends in Algebraic Development Techniques. LNCS 5486, Springer, 2009.
  • T. Kahsai, M. Roggenbach, H. Schlingloff. Specification-based testing for Software Product Lines. Proc. 6th IEEE International Conference on Software Engineering and Formal Methods [SEFM'08]. Pag. 149-159, 2008. © IEEE Computer Society. © IEEE Computer Society.
  • T. Kahsai, M. Roggenbach. Refinement notions for CSP-CASL. 19th International Workshop on Algebraic Development Techniques [WADT08]. Preliminary Proceedings, TR-08-15, 2008.
  • T. Kahsai, M.Miculan. Implementing Spi Calculus using Nominal techniques. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Lowe, editors, Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, [CiE'08], Athens, Greece, June 2008, Proceedings. LNCS volume 5028, 2008.
  • T. Kahsai, M. Roggenbach, H. Schlingloff. Specification-based testing for refinement. [SEFM'07]. Proc. 5th IEEE International Conference on Software Engineering and Formal Methods. Pag.237--247. 2007.© IEEE Computer Society.


Bldg 269 Room 294
NASA Ames Research Center
Moffett Field CA 94035

temesghen.kahsaiazene "at"

Links :

+ Linkedin Profile

+ NASA Ames
+ TI Home Page
+ RSE Homepage
+ NASA Home Page

First Gov logo
NASA Logo -