CSL professor Mitra publishes textbook

Reflecting on his father’s habit of regularly penning newspaper articles, plays, and stories, CSL professor Sayan Mitra ascribes his writing to, perhaps, a familial trait. Also inspired by the work of some of his fellow ECE faculty, and taking a detour from his usual research productivity, Mitra used 2019-2020 to finish writing his textbook.

“As a researcher, I have found the company of textbooks reassuring in exploring new areas,” says Mitra. “I aspired to contribute my little piece in that tradition. The final decision to write the book was really a miscalculation in estimating the work required to make a book out of course notes.”

Mitra’s textbook covers “verification”. He describes this as the art and the science of determining whether a system meets its requirements. It is a core technology for designing safe autonomous systems like driverless cars, urban air mobility, and embedded medical devices. His book is an introduction to verification techniques for such cyber-physical systems.

“The textbook is designed for graduate students and researchers interested in modeling, verification, cyber-physical systems, robotics, autonomous systems, design automation, and related areas,” says Mitra. “I am hopeful that the book will also be accessible to motivated undergraduate students.”

Mitra says that current methods of teaching mathematics for computer science – automata, logic, etc. – makes the math look much different from calculus (math for physics).

“This siloed view makes a typical CS student uncomfortable in dealing with differential equations, and an EE student nervous about automata, induction, and logic,” says Mitra. “One of the things that the book tries to do is to bridge this gap. It introduces a unified viewpoint for talking about both programs and differential equations.”

The book is designed for a semester-long course. Mitra specifically allowed for a number of different tracks for students to choose from and includes plenty of examples, exercises, and programming assignments. He says that the most difficult part of writing the textbook was deciding what to exclude.

“I have been doing research in this area for more than a decade and have my biases and favorites,” says Mitra. “There is a tension between all the material that I care about and making the book too prolonged for newcomers. I also had to cope with the procrastination games that became quite baroque with this longer time-scale project.”

The textbook is now available through MIT Press.