A few days back, Byron Cook, from Microsoft Cambridge came to give a guest lecture in the Formal Methods course. The guy, if you could call him that, talked about SLAM which Microsoft is now using internally for proving correctness of device drivers.
Amongst other things, he showed how, by using their software, the developers of Parallel Port device driver found two invocations of an IO completion API in a particular scenario. He said that a lot of Program Managers within Microsoft have started showing interest in Mathematical Logic and Formal Methods after Bill Gates personally congratulated the team. ;)
Other than increasing my interest further with Formal Methods, he talked about his former company, Prover Technology, which means that people are now building commercial products out of Formal Methods.
The lecture was quite complex keeping in view that we have just started studying this field of computer science. And this is one of the most complex fields within computer science; perhaps, as complex as Analysis of Algorithms. What I have learned uptil now starts from Propositional Logic and ends at First Order Logic. The lectures in this course will also cover Dynamic Logic but I still feel that we know nothing.
I have finally made up my mind to do thesis in formal methods and I have a few more months to start that. Fortunately or unfortunately, the Disrtributed Computing Research Group within Chalmers is not so active.
No comments:
Post a Comment