Kalyan

Kalyan is a post-doctoral researcher with the ProVal team at INRIA Saclay - Île-de-France .

He works on software verification, more specifically on loop invariant generation for the Frama-C software verification platform. Recently, he also did some effort on a distributed computing library for functional programming called "Functory" - inspired by Google's Map/Reduce.

Previously, he graduated with a PhD in Computer Science, focussing his research on scalable, efficient and effective formal verification techniques. It also resulted in NuSMT - a formal verification tool that combines the efficiency of model-checkers with the effectiveness of SMT solvers and scales up the verification process to industrial-size designs using abstraction techniques as in the CEGAR framework.

During his free time, he reads articles on current affairs, learns about startups and business technology, sketches cartoons - more recently in digital form, and continuously ponders about the application of innovative technologies for societal development - health-care and energy being his particular favourites. Besides these, he enjoys coffee, running, photography and debate.

He is an alumnus of the Birla Institute of Technology and Science (BITS, Pilani), Pilani, India, as well as the Tata Institute of Fundamental Research (TIFR), Mumbai, India.

His old (but cool..) web-page could still be found here.

Academic Research

• Safety-critical software verification: Software verification has always posed various challenges for computer scientists. A recent approach for software verification is deductive verification of annotated programs. Frama-C is a framework that combines program analyzers and static verification techniques. It works on an annotated C programs and generates verification conditions that are automatically discharged by a bunch of provers. I am trying to generate some of these annotations, in particular loop invariants automatically, using techniques of predicate abstraction. This reduces the burden on the verification engineer, thereby improving the productivity



• Functory: Functory is a distributed computing library for functional programming. It helps in distributing parallelizable tasks to different cores within the same machine, or different machines on a network. It also offers API implementations corresponding to different contexts of deployment - depending on the version of Ocaml used in the different machines, the architecture of the different machines and the ability to pass closures. It is polymorphic and also boasts of a robust fault-tolerant mechanism. It is implemented in OCaml, but the techniques are rather straight forward to implement in other languages.



• NuSMT: NuSMT is a verification tool that combines the strengths of BDDs (Binary Decision Diagrams) and SMT (Satisfiability Modulo Theory) solvers. The name 'NuSMT' is derived from the verification engines it is composed of: NuSMV model checker and MathSAT SMT solver. BDD based quantification is known to be efficient and it forms the heart of many modern model checking engines. NuSMT is an extension to the most widely used open-source model checker NuSMV. The newer verification engines - SMT solvers quite aptly referred to as a "disruptive technology" enables us to handle richer theories. NuSMT uses MathSAT SMT solver.

Mailing address:

Kalyan KRISHNAMANI
#70, PCRI (Pôle Commun de Recherche en Informatique)
INRIA - Saclay Île-de-France
Rue Noetzlin, 91190 Gif-sur-Yvette
France