Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
SAT-based Bounded Model Checking for 3-Valued Abstractions
du 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