IC Colloquium: Developing Provably Correct and Efficient Programs Using the Ciao Model
Cancelled
Event details
| Date | 29.10.2018 |
| Hour | 16:15 › 17:30 |
| Location | |
| Category | Conferences - Seminars |
By: Manuel Hermenegildo - IMDEA Software Institute and UPM
Abstract:
The demand for software that is provably correct and efficient has moved from niche application areas to truly pervading the software industry. Avoiding the consequences of those errors, such as private information leakage, has become of paramount importance. However, developing such provably correct and efficient code in a cost-effective way is still challenging. The Ciao program development model addresses this issue through a best-effort approach that
combines performing static analyses during program editing and compilation in order to detect bugs or certify as much as possible of the code, with run-time checks and testing for properties or parts of the program that cannot be verified statically --an approach that is now behind many current efforts in the area. We will present a number of results achieved with this model verifying conditions ranging from classical safety properties to non-functional properties such as time, memory, energy, or user-defined resources. We will also discuss the biggest challenges involved, and present some of our recent work in areas such as verifying energy consumption, reducing the cost of run-time checks and analyzing them statically, or combining incremental and modular analysis for scalability.
Bio:
Manuel Hermenegildo has a Ph.D. in Computer Science and Engineering from UT Austin (1986) and a Masters from T.U. Madrid (UPM). He is Distinguished Professor at the IMDEA Software Institute (of which he was the founding director) and Full Prof. at T.U. Madrid. Previously, he held an Endowed Chair at the U. of New Mexico and was Project Leader at MCC and faculty at UT Austin. He has received the National Prize for Mathematics and Information Science and Technology, a 10-year most influential paper award from the Association of Logic Programming, and several best paper awards. He is a member of the
Academia Europaea, president of the INRIA Scientific Board, and member of the Dagstuhl Advisory Board, and has been vice-President of Informatics Europe and President of the Association for Logic Programming. His interests include energy-aware computing, program analysis and verification, abstract interpretation, partial evaluation, parallelizing compilers, and constraint and logic programming language design and implementation.
More information
Abstract:
The demand for software that is provably correct and efficient has moved from niche application areas to truly pervading the software industry. Avoiding the consequences of those errors, such as private information leakage, has become of paramount importance. However, developing such provably correct and efficient code in a cost-effective way is still challenging. The Ciao program development model addresses this issue through a best-effort approach that
combines performing static analyses during program editing and compilation in order to detect bugs or certify as much as possible of the code, with run-time checks and testing for properties or parts of the program that cannot be verified statically --an approach that is now behind many current efforts in the area. We will present a number of results achieved with this model verifying conditions ranging from classical safety properties to non-functional properties such as time, memory, energy, or user-defined resources. We will also discuss the biggest challenges involved, and present some of our recent work in areas such as verifying energy consumption, reducing the cost of run-time checks and analyzing them statically, or combining incremental and modular analysis for scalability.
Bio:
Manuel Hermenegildo has a Ph.D. in Computer Science and Engineering from UT Austin (1986) and a Masters from T.U. Madrid (UPM). He is Distinguished Professor at the IMDEA Software Institute (of which he was the founding director) and Full Prof. at T.U. Madrid. Previously, he held an Endowed Chair at the U. of New Mexico and was Project Leader at MCC and faculty at UT Austin. He has received the National Prize for Mathematics and Information Science and Technology, a 10-year most influential paper award from the Association of Logic Programming, and several best paper awards. He is a member of the
Academia Europaea, president of the INRIA Scientific Board, and member of the Dagstuhl Advisory Board, and has been vice-President of Informatics Europe and President of the Association for Logic Programming. His interests include energy-aware computing, program analysis and verification, abstract interpretation, partial evaluation, parallelizing compilers, and constraint and logic programming language design and implementation.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host: Viktor Kuncak