संदीप के. शुक्ला

Sandeep's work on applying formal verification techniques and tools to system design problems is rather unique. He was elected an IEEE fellow for his "contributions to applied probabilistic model-checking for system design". His work on designing reliability-driven nano-computing on defective substrates by novel use of probabilistic model-checking has led to a number of publications in IEEE Transactions on Nanotechnology, and Transactions on Circuits and Systems. It also resulted in a tool called NANOPRISM, and a significant amount of subsequent work on defect-tolerant computing by various research groups. Sandeep's work on creating system level design languages with ability to express distinct models of computations for distinct parts of an embedded hardware/software system led to new kernels of SystemC language. His work on meta-modeling driven component composition pre-dated the standardization effort of the SPIRIT consortium. His reduction of the 'clock calculus' (which lies at the core of the compilation of polychronous languages) to the problem of computing prime implicates in a propositional theory led to a new set of tools for multi-threaded code synthesis. US Air Force funded this work for an industrial implementation at L-3 Communications. Sandeep and his colleagues recently published a constructive operational semantics for combining synchronous programming models within polychronous models which paves the way to combine the strengths of synchronous language based software synthesis and the asynchronous concurrency model of polychronous languages. This work won an US AFOSR international grant to collaborate with INRIA , and University of Kaiserslautern. This is a first attempt to combine these two distinct approaches to synchronous model of computation.