| The SeaHorn verification framework A Gurfinkel, T Kahsai, A Komuravelli, JA Navas Computer Aided Verification: 27th International Conference, CAV 2015, San …, 2015 | 349 | 2015 |
| PKIND: A parallel k-induction based model checker T Kahsai, C Tinelli Arxiv preprint arXiv:1111.0372, 2011 | 100 | 2011 |
| JayHorn: A Framework for Verifying Java programs T Kahsai, P Rümmer, H Sanchez, M Schäf Computer Aided Verification: 28th International Conference, CAV 2016 …, 2016 | 82 | 2016 |
| JDart: A Dynamic Symbolic Analysis Framework K Luckow, M Dimjašević, D Giannakopoulou, F Howar, M Isberner, ... Tools and Algorithms for the Construction and Analysis of Systems: 22nd …, 2016 | 81 | 2016 |
| 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: 21st …, 2015 | 64 | 2015 |
| Reachability analysis for AWS-based networks J Backes, S Bayless, B Cook, C Dodge, A Gacek, AJ Hu, T Kahsai, ... Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019 | 55 | 2019 |
| CoCoSpec: A mode-aware contract language for reactive systems A Champion, A Gurfinkel, T Kahsai, C Tinelli Software Engineering and Formal Methods: 14th International Conference, SEFM …, 2016 | 45 | 2016 |
| Instantiation-based invariant discovery T Kahsai, Y Ge, C Tinelli NASA Formal Methods, 192-206, 2011 | 44 | 2011 |
| Verifying the safety of a flight-critical system G Brat, D Bushnell, M Davies, D Giannakopoulou, F Howar, T Kahsai FM 2015: Formal Methods: 20th International Symposium, Oslo, Norway, June 24 …, 2015 | 39 | 2015 |
| Synthesizing ranking functions from bits and pieces C Urban, A Gurfinkel, T Kahsai Tools and Algorithms for the Construction and Analysis of Systems: 22nd …, 2016 | 37 | 2016 |
| Incremental invariant generation using logic-based automatic abstract transformers PL Garoche, T Kahsai, C Tinelli NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field …, 2013 | 26 | 2013 |
| Specification-Based Testing for Software Product Lines T Kahsai, M Roggenbach, BH Schlingloff Software Engineering and Formal Methods, 2008. SEFM'08. Sixth IEEE …, 2008 | 24 | 2008 |
| Specification-based testing for refinement T Kahsai, M Roggenbach, BH Schlingloff Fifth IEEE International Conference on Software Engineering and Formal …, 2007 | 23 | 2007 |
| Testing-based compiler validation for synchronous languages PL Garoche, F Howar, T Kahsai, X Thirioux NASA Formal Methods: 6th International Symposium, NFM 2014, Houston, TX, USA …, 2014 | 21 | 2014 |
| Quantified heap invariants for object-oriented programs T Kahsai, R Kersten, P Rümmer, M Schäf LPAR-21, May 7–12, 2017, Maun, Botswana, 368-384, 2017 | 17 | 2017 |
| Incremental verification with mode variable invariants in state machines⋆ T Kahsai, PL Garoche, C Tinelli, M Whalen | 17* | |
| Synthesizing modular invariants for synchronous code PL Garoche, A Gurfinkel, T Kahsai arXiv preprint arXiv:1412.1152, 2014 | 16 | 2014 |
| JayHorn: A Java Model Checker: (Competition Contribution) T Kahsai, P Rümmer, M Schäf Tools and Algorithms for the Construction and Analysis of Systems: 25 Years …, 2019 | 15 | 2019 |
| Compilation of synchronous observers as code contracts A Dieumegard, PL Garoche, T Kahsai, A Taillar, X Thirioux Proceedings of the 30th Annual ACM Symposium on Applied Computing, 1933-1939, 2015 | 14 | 2015 |
| Property preserving refinement for CSP-CASL T Kahsai, M Roggenbach Recent Trends in Algebraic Development Techniques, 206-220, 2009 | 12 | 2009 |
Cesare TinelliProfessor of Computer Science, The University of IowaVerified email at uiowa.edu
