IC Colloquium : On Synthesis of Verification Tools
Event details
| Date | 11.10.2012 |
| Hour | 16:15 › 17:30 |
| Speaker | Andrey Rybalchenko, TU Munich |
| Location | |
| Category | Conferences - Seminars |
Abstract
Software complexity is growing, so is the demand for software verification. Soon, perhaps within a decade, wide deployment of software verification tools will be indispensable or even mandatory to ensure software reliability in a large number of application domains, including but not restricted to safety and security critical systems. To adequately respond to the demand we need to eliminate tedious aspects of software verifier development, while providing support for the accomplishment of creative aspects. We believe that the next generation of software verifiers will be constructed from logical specifications designed by quality/verification engineers with expertise in the application domain. Give a specification describing a verification method, a corresponding software verifier will be obtained by implementing a frontend that translates software source code into constraints according to the specification and then coupling the frontend with a highly-tuned general-purpose constraint solver, thus eliminating the need for algorithmic implementation efforts from the ground up.
Biography
Andrey's research interests focus on automated methods and tools for formal software verification, ranging from the design of program analysis methods to the development of algorithms for symbolic computation and automated deduction. He is a professor at Technische Universität München. In the past, he was affiliated with Max Planck Institute for Software Systems, EPFL, MSR Cambridge, Max Planck Institute for Informatics, and University of Saarland.
Andrey was selected for MIT TR35 (2010), received an ERC Starting grant (2012), and a Microsoft Research European Fellowship (2006).
Software complexity is growing, so is the demand for software verification. Soon, perhaps within a decade, wide deployment of software verification tools will be indispensable or even mandatory to ensure software reliability in a large number of application domains, including but not restricted to safety and security critical systems. To adequately respond to the demand we need to eliminate tedious aspects of software verifier development, while providing support for the accomplishment of creative aspects. We believe that the next generation of software verifiers will be constructed from logical specifications designed by quality/verification engineers with expertise in the application domain. Give a specification describing a verification method, a corresponding software verifier will be obtained by implementing a frontend that translates software source code into constraints according to the specification and then coupling the frontend with a highly-tuned general-purpose constraint solver, thus eliminating the need for algorithmic implementation efforts from the ground up.
Biography
Andrey's research interests focus on automated methods and tools for formal software verification, ranging from the design of program analysis methods to the development of algorithms for symbolic computation and automated deduction. He is a professor at Technische Universität München. In the past, he was affiliated with Max Planck Institute for Software Systems, EPFL, MSR Cambridge, Max Planck Institute for Informatics, and University of Saarland.
Andrey was selected for MIT TR35 (2010), received an ERC Starting grant (2012), and a Microsoft Research European Fellowship (2006).
Links
Practical information
- Informed public
- Free
- This event is internal
Organizer
- Host : Prof. Viktor Kuncak
Contact
- Christine Moscioni/Simone Muller