Â鶹´«Ã½

Testing doesn't always reveal every bug in a system, which is why Professor Jhala is interested in all the possible behaviors of programs involved in everything from dispensing cash from automatic teller machines to applets that execute on Java-enabled Web browsers. Increasingly, programs include millions of lines of code. Jhala considers the task of ensuring reliability of such huge programs both a challenging theoretical pursuit and a practical necessity of computer systems.His Ph.D. dissertation was titled Scalable Program Verification by Effective Abstraction. Currently, he is interested in precise but scalable techniques for checking software. He devised a "Lazy Abstraction" method that combines precision and scalability analyses, capitalizing on the insight that precision can be localized.Jhala also is exploring several promising ways to improve checking technology and integrating it with software engineering processes. He has taken steps in this direction by showing how to reuse proofs generated in prior checks to verify programs incrementally -- as they are being developed.

Capsule Bio:

Ranjit Jhala received a bachelor of technology degree in computer science in 1999 from the Indian Institute of Technology in New Delhi, and a Ph.D. in electrical engineering and computer science from UC Berkeley in 2004. While working on his dissertation, Jhala was named the outstanding teaching assistant by Berkeley's EECS Department. He is a member of the Open Source Quality Project, and he has delivered 11 conference papers and has refereed papers for CAV, CONCUR, FSTTCS, LICS, PLDI, and POPL.