Seminar 2019-10-10

Date: 2019-10-10​
Time: 11:00-12:00
Speaker: ​​Mauricio Chimento, KTH
Title: Combined Static and Dynamic Verification of Object Oriented Software Through Partial Proofs

Abstract
When verifying software one can make use of several verification techniques. These techniques mostly fall in one of two categories: static verification and dynamic verification. Static verification deals with the analysis of either concrete source code, or a model of it. These kinds of techniques can verify properties over all possible runs of a program. Dynamic verification is concerned with the monitoring of software, providing guarantees that observed runs comply with specified properties. It is strong in analysing systems of a complexity that is difficult to address by static verification, e.g., systems with numerous interacting sub-units, concrete (as opposed to abstract) data, etc. On the other hand, its major drawbacks are the impossibility to extrapolate correct observations to all possible runs, and that the monitoring of a property introduces runtime overheads.

It is quite clear that static and dynamic verification have largely disjoint strengths. Therefore, their combination can allow the verification process to deal with richer properties, with a greater ease. In this talk I will present the main contributions of the work which I have developed during my PhD studies regarding the combination of static and dynamic verification. The main novelty of this work is that it considers the use of the partial proofs in the verification process as a means to accomplish the combination of verification techniques, whereas, in general, other verification approaches discard these kind of proofs right away

Bio
My name is Jesus Mauricio Chimento. I have recently got my PhD degree at Chalmers University of Technology. There I worked under the supervision of Wolfgang Ahrendt (in the rol of supervisor), and Gerardo Schneider (in the rol of co-supervisor). The work developed during my PhD was focused on the combination of static verification and dynamic verification. Now, I am part of the Software and Computer Systems department, where I am doing a PostDoc working with David Broman in a project regarding the verification of cyber-physical systems. In general, my research interests focus on studying Formal Methods, and Certified Programming. Regarding Formal Methods, I am keen on studying Program Specification and Program Verification, in particular Theorem Proving and Runtime Verification.