Evènement pour le groupe Séminaire Méthodes Formelles


Date 2017-06-27  11:00-12:00
TitreSAT-based Bounded Model Checking for 3-Valued Abstractions 
RésuméIn this talk I will present joint work with Nils Timm (and students) from the University of Pretoria on how to make model-checking of concurrent systems more effective and more efficient. In the first part of the talk, which is based on our SBMF'16 paper, I show how bounded model-checking over a three-valued truth domain {T:true, F:false, U:unknown} can be translated into a classical Boolean satisfiability problem which can then be given to any classical SAT solver. In the second part of the talk, which is based on our recent FSEN'17 paper, I speak about efficiency-increasing heuristics which are based on the availability of structural knowledge about the original system to be model-checked. On the basis of such structural knowledge the SAT solver can be guided into 'promising' search paths, whereby the probability of unnecessarily exploring fruitless paths is considerably diminished. The SBMF'16 paper was acknowledged as the "2nd-best paper of the conference", and the FSEN'17 paper was nominated among the "top three papers of the conference". 
Lieu178 
OrateurStefan GRUNER 
Emailhttp://www.cs.up.ac.za/users/view/sgruner 
UrlUniversity of Pretoria, South Africa 



Aucun document lié à cet événement.

Retour
Retour à l'index