|
![](images/spacer.gif) |
Jeudi 23 Mars
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
CARET Model Checking For Pushdown Systems |
Description: |
Huu-Vu Nguyen CARET (A temporal logic of calls and returns) was introduced by Alur et al. This logic allows to write linear temporal logic formulas while taking into account matching of calls and returns. However, CARET model checking for Pushdown Systems (PDSs) was never considered in the literature. Previous works only dealt with the model checking problem for Recursive State Machine (RSMs). While RSMs are a good formalism to model sequential programs written in structured programming languages like C or Java, they become non suitable for modeling binary or assembly programs, since, in these programs, explicit push and pop of the stack can occur. Thus, it is very important to have a CARET model checking algorithm for PDSs. We tackle this problem in this paper. We also consider CARET model checking with regular valuations, where the set of configurations in which an atomic proposition holds is a regular language. We reduce these problems to the emptiness problem of Büchi Pushdown Systems. We implemented our technique in a tool, and we applied it to different case studies. Our results are encouraging. In particular, we were able to apply our tool to detect several malwares.
This is a joint work with Tayssir Touili. |
|
|