Konstantinos Mamouras designs programming abstractions for processing data streams. The CS assistant professor also taught Verified Programming to graduate students during his first year at Rice University. Students learned the mathematical foundations required to build reliable software.
“I use interactive proof assistants that allow one to program as well as prove the correctness of the software they are creating in a single environment,” Mamouras said.
“Along the way, students learn about logic, functional programming, and deductive verification. At a very high level, I hope they learned the skills necessary to reason formally about the software that they create. I hope they got the skills that are necessary to rigorously prove the correctness of their software,” he said.
Mamouras’ research focuses on creating programming languages and tools for the processing of streaming data. Several real-time decision-making applications rely on the computation of quantitative summaries of very large streams of data.
Mamouras proposed StreamQRE, a declarative query language that combines regular expressions, quantitative aggregation, and relational features.
“Stream processing is the processing of data that is generated continuously in real time such as sensor measurements, activity logs such as user activity on the web, credit card transactions and so on. StreamQRE is an example of a language for data stream processing which provides strong guarantees of performance,” he said.
A conversation with a friend who does research on medical devices sparked the idea for using StreamQRE in the medical domain. Mamouras was a postdoctoral researcher at the time. He was advised by Rajeev Alur at the University of Pennsylvania. The friend needed a language for stream processing to apply to his research. Soon a collaboration was born.
“We have used StreamQRE in a health care application, namely for the detection of potentially fatal arrhythmias,” he said.
Mamouras wants to bring the techniques used in the classroom to his research in the future.
“I want to use the technology of proof assistants to model the languages that I design. I also want to verify the correctness of the algorithms and tools that I create. I believe this line of work has the potential to make an impact in safety-critical applications such as the monitoring algorithms that are used in medical devices,” he said.
Cintia Listenbee, Communications and Marketing Specialist in Computer Science