IC Colloquium: Algorithmic Foundations for Systems Certification
By: Rupak Majumdar - Max Planck Institute for Software Systems
Abstract
Our ability to design, implement, and generate new systems outpaces our ability to ensure that they work as they should.Systems certification studies how we can convince ourselves and others that a system works as it is specified; typically, but not always, this involves building a rigorous proof of correctness that can be independently checked.
In this talk, we will explore the theoretical and practical landscape of systems certification from an algorithmic perspective. We focus on three threads of work. First, we describe new decidability and tractability results for verification of infinite-state models of software.Second, we describe correct-by-construction techniques for controller synthesis for cyber-physical systems. Finally, we consider rigorous certification techniques that give up absolute certainty. Here, we show how randomized algorithms can form the basis for rigorous certification with probabilistic guarantees.
We conclude with strategic considerations in certification, where the provider of a certificate may have incentives different from the consumer.
Bio
Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. His research interests are in the verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, logic, and automata theory. Dr. Majumdar received the President's Gold Medal from IIT Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, a Sloan Foundation Fellowship, an ERC Synergy award, a Distinguished Alumnus Award from IIT Kanpur, "Most Influential Paper" awards from PLDI, POPL, and CONCUR, and several best paper awards. He received the B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur and the Ph.D. degree in Computer Science from the University of California at Berkeley.
More information
Abstract
Our ability to design, implement, and generate new systems outpaces our ability to ensure that they work as they should.Systems certification studies how we can convince ourselves and others that a system works as it is specified; typically, but not always, this involves building a rigorous proof of correctness that can be independently checked.
In this talk, we will explore the theoretical and practical landscape of systems certification from an algorithmic perspective. We focus on three threads of work. First, we describe new decidability and tractability results for verification of infinite-state models of software.Second, we describe correct-by-construction techniques for controller synthesis for cyber-physical systems. Finally, we consider rigorous certification techniques that give up absolute certainty. Here, we show how randomized algorithms can form the basis for rigorous certification with probabilistic guarantees.
We conclude with strategic considerations in certification, where the provider of a certificate may have incentives different from the consumer.
Bio
Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. His research interests are in the verification and control of reactive, real-time, hybrid, and probabilistic systems, software verification and programming languages, logic, and automata theory. Dr. Majumdar received the President's Gold Medal from IIT Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, a Sloan Foundation Fellowship, an ERC Synergy award, a Distinguished Alumnus Award from IIT Kanpur, "Most Influential Paper" awards from PLDI, POPL, and CONCUR, and several best paper awards. He received the B.Tech. degree in Computer Science from the Indian Institute of Technology at Kanpur and the Ph.D. degree in Computer Science from the University of California at Berkeley.
More information
Practical information
- General public
- Free
Contact
- Host: Viktor Kuncak