Papers
[GKT13]: Pierre-Loic Garoche, Temesghen Kahsai, Cesare Tinelli. Incremental Invariant Generation using Logic-based Automatic Abstract Transformers. In Proceedings of NASA Formal Methods 2013. LNCS 7871, 2013.
[KGWT12] : Temesghen Kahsai, Pierre-Loic Garoche, Mike Wahlen, Cesare Tinelli. Incremental verification with mode variable invariants in state machines. In Proceedings of NASA Formal Methods NASA 2012.LNCS 7226. 2012
[KT11]: Temesghen Kahsai, Cesare Tinelli. PKind: A parallel k-induction based model checker . In Parallel and Distributed Methods in verification 2011. EPTCS, 2011.
[KYT11]: Temesghen Kahsai, Yeting Ge, Cesare Tinelli. Instantiation-based invariant discovery. In Proceedings of NASA Formal Methods 2011. LNCS 6617. 2011
[HT08]: George Hagen and Cesare Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD'08), Portland, Oregon. IEEE, 2008.
[H08]: George Hagen. Verifying safety properties of Lustre programs: an SMT-based approach. PhD dissertation. Department of Computer Science. The University of Iowa. December 2008.