Introduction à la vérification logique du premier ordre

9

J'essaie de m'enseigner différentes approches de la vérification logicielle. J'ai lu quelques articles. Pour autant que je sache, la logique propositionnelle avec le temporel utilise généralement la vérification de modèle avec des solveurs SAT (dans les systèmes en cours - réactifs), mais qu'en est-il de la logique du premier ordre avec le temporel? Utilise-t-il des prouveurs de théorèmes? Ou peut-il également utiliser SAT?

Tout pointeur vers des livres ou des articles pour les débutants dans ce domaine est très apprécié.

FELIPE N.
la source
2
Tout d'abord, bienvenue à CS: SE. Bien que je ne sois pas un expert dans ce domaine, vous semblez saisir plusieurs sujets à la fois en laissant beaucoup de trous. Ne vous inquiétez pas; Je le fais tout le temps. Jetez un oeil à la vérification du logiciel puis vérification formelle puis modèle vérification et logiciel de vérification formelle: Modèle Vérification et théorème Proving
Guy Coder

Réponses:

9

La logique du premier ordre est indécidable, donc la résolution SAT n'aide pas vraiment. Cela dit, il existe des techniques de vérification des modèles bornés des formules du premier ordre. Cela signifie que seul un nombre fixe d'objets peut être pris en compte lorsque vous essayez de déterminer si la formule est vraie ou fausse. De toute évidence, ce n'est pas complet, mais si un contre-exemple est trouvé, alors c'est vraiment un contre-exemple.

L'outil Alloy est un outil qui permet de décrire les modèles dans une logique de premier ordre (bien que la syntaxe de surface soit basée sur des modèles décrits de manière relationnelle) et utilise la vérification des modèles bornés pour trouver des solutions. Un solveur SAT est utilisé sous le capot. Une extension d'alliage permet des modèles avec un caractère temporel, bien que techniquement elle ne supporte pas la logique temporelle.

Si vous souhaitez explorer davantage, par exemple, pour vérifier l'exactitude du programme, vous pouvez consulter les outils de vérification du programme. Celles-ci sont généralement basées sur la logique de Hoare (pour le raisonnement sur les pré- et post-conditions), éventuellement étendues avec la logique de séparation (pour le raisonnement sur les tas). Ces logiques sont généralement indécidables, une certaine interaction entre l'humain et l'outil de vérification est donc nécessaire. Voici quelques exemples d'outils:

Dave Clarke
la source
10

Après avoir lu votre question, la seule façon dont je pouvais voir et j'avais suffisamment de connaissances pour relier les sujets était de donner un ensemble d'articles de haut niveau qui descendaient de la vérification logicielle pour finir par essayer d'unir la vérification des modèles et la démonstration des théorèmes. J'espère que mon commentaire l'a fait:

Jetez un oeil à la vérification du logiciel puis vérification formelle puis modèle de vérification et du logiciel de vérification formelle: Modèle Vérification et théorème Proving

Dave a donné une bonne réponse pour laquelle je ne peux pas rendre beaucoup plus justice à la première partie de la question que Dave ne l’avait fait, car je suis également nouveau sur ce point.

Puisque c'est votre première question sur un site SE , la raison pour laquelle je n'ai pas donné de réponse mais un commentaire est parce qu'ici une réponse ne peut pas être juste un ensemble de liens, mais doit donner une réponse écrite et utiliser des liens à l'appui de la réponse; donc un commentaire au lieu d'une réponse.

En ce qui concerne:

Tout pointeur vers des livres ou des articles pour les débutants dans ce domaine est très apprécié.

Les livres que je suggérerais et utiliserais sont:

À l'heure actuelle, je ne peux pas m'étendre davantage sur la démonstration du théorème parce que j'apprends toujours les avantages et les inconvénients de chacun, mais ceux dans lesquels je me concentre sont

  • HOL Light à cause du livre de John Harrison.
  • Coq car il est basé sur le calcul des constructions
  • Isabelle car elle est basée sur une unification d'ordre supérieur.

    Ces assistants de preuve ont également généralement des livres, sont à jour, populaires, open-source, maintenus et ont des communautés de support actives.

Remarque: J'ai utilisé worldcat.org pour référencer les livres, mais vous pouvez les consulter en utilisant la fonction de recherche à l'intérieur d'Amazon.

Guy Coder
la source
Pour éviter beaucoup de modifications à la réponse, je laisserai tomber les informations ajoutées en tant que commentaires, puis à l'avenir les enroulerai dans la réponse. Pour avoir essayé de trier les nombreuses similitudes et différences entre les assistants de preuve. Google pour Freek Wiedijk; Je trouve ses papiers très utiles.
Guy Coder
Merci beaucoup pour votre réponse détaillée et approfondie. Pour ajouter vos commentaires sur les livres et fournir un lien vers le livre gratuit. Encore une fois, je ne vous remercierai jamais assez :-)
FELIPE N.