Formal verification of pipelined processors with precise exceptions. - Krishnamani Kalyanasundaram; R. K. Shyamasundar (MEMOCODE, 2004)

Verification of Clock Synchronization in TTP. - Krishnamani Kalyanasundaram; R. K. Shyamasundar (Formal Models, Languages and Applications, 2007)

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. - Roberto Cavada; Alessandro Cimatti; Anders Franzén; Krishnamani Kalyanasundaram; Marco Roveri; R. K. Shyamasundar (FMCAD, 2007)

Tighter integration of BDDs and SMT for Predicate Abstraction. - Alessandro Cimatti; Anders Franzén; Alberto Griggio; Krishnamani Kalyanasundaram; Marco Roveri (DATE, 2010)