Initiation à la preuve de programme avec Frama-C

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
55
|
Mois de parution
juillet 2011
|
Domaines


Résumé
Avec Frama-c, vérifiez et validez vos programmes C de manière sûre par la preuve de programme.

La suite est réservée aux abonnés. Déjà abonné ? Se connecter

Sur le même sujet

Évolutions récentes de PHP : les nouveautés des 15 dernières années

Magazine
Marque
GNU/Linux Magazine
Numéro
238
|
Mois de parution
juin 2020
|
Domaines
Résumé

PHP est un langage qui, comme la plupart des autres langages, évolue continuellement. Nous traitons dans ces pages régulièrement de ces évolutions, mais entre le moment où vous lisez un article ici et le moment où vous pouvez l'utiliser dans vos projets, il se passe souvent des années... Du coup, de nombreuses nouveautés ne sont que très faiblement utilisées, je vous propose donc de les redécouvrir.

Automatiser les tâches de conception de circuits imprimés : greffons pour KiCAD et FreeCAD

Magazine
Marque
GNU/Linux Magazine
Numéro
238
|
Mois de parution
juin 2020
|
Domaines
Résumé

KiCAD et FreeCAD convergent pour fournir un environnement cohérent de conception électronique et mécanique assistée par ordinateur. Ces deux outils rendent leurs fonctions accessibles depuis Python, langage permettant d’automatiser un certain nombre de tâches répétitives et donc fastidieuses. Nous proposons de rédiger quelques greffons (plugins) pour distribuer des vias [1] le long de lignes de transmissions radiofréquences (KiCAD), puis automatiser la réalisation du boîtier contenant un circuit imprimé avec les ouvertures pour ses connecteurs (FreeCAD).

Y a une panne de secteurs !

Magazine
Marque
GNU/Linux Magazine
Numéro
238
|
Mois de parution
juin 2020
|
Domaines
Résumé

C’est l’histoire réelle d’une traque de secteurs défectueux jusque dans les fichiers concernés, d’une bourde, de la reconstruction en direct d’une table de partitions, et quelques bonus avec ddrescue et nbdkit.

Introduction à QBDI et ses bindings Python

Magazine
Marque
MISC
Numéro
109
|
Mois de parution
mai 2020
|
Domaines
Résumé

Le présent article traite de l'outil d'instrumentation dynamique QBDI. C'est un framework de DBI (Dynamic Binary Instrumentation), comparable à d'autres projets publics tels qu’Intel PIN, Valgrind ou encore DynamoRIO. Avant d'entrer dans le vif du sujet, quelques rappels peuvent s'avérer nécessaires…

Par le même auteur

Spin model checker

Magazine
Marque
Open Silicium
Numéro
9
|
Mois de parution
décembre 2013
|
Domaines
Résumé

Modélisez et vérifiez votre programme multi-threads avec Spin, le model-checker open-source.

Snort & Base

Magazine
Marque
GNU/Linux Magazine
Numéro
149
|
Mois de parution
mai 2012
|
Résumé
Détectez les intrusions réseau avec Snort, l'IDS open source, et analysez-les par l'interface BASE, the Basic Analysis and Security Engine.