Et tout d'abord, Pourquoi vérifier les programmes ?
et aussi : Tony Hoare's "grand challenge" concept (and many Position Papers)
Bibliographie
Quelques sources pour rechercher des papiers : Doc INRIA-Sophia,
Un début de rangement de ma biblio sur
Conférences
- POPL : Symposium on Principles of Programming Languages : 2008, 2007,
- SAS : International Static Analysis Symposium : 2007, 2006, 2005,
- SCAM : IEEE International Working Conference on Source Code Analysis and Manipulation : 2007, 2006, 2005,
- FLoC : Federated Logic Conference : 2006,
- CAV (part of FLoC) : 2006, 2005,
- FM :International Symposium On Formal Methods : 2008, 2006, 2005,
- ETAPS : European Joint Conferences on Theory and Practice of Software : 2008, 2007,
- TACAS (part of ETAPS) : Tools and Algorithms for the Construction and Analysis of Systems : 2008, 2007, 2006, 2005,
- WRS : Workshop on Reduction Strategies in Rewriting and Programming
Quelques personnes
- Tony Hoare,
- Edsger W. Dijkstra,
- ThomasReps,
- BarbaraG.Ryder,
- FrankTip,
- Susan B. Horwitz,
- George Necula (CIL, PCC, ...),
- PatrickCousot, RadhiaCousot,
- John Hatcliff,
- Edmund M. Clarke (Model Checking)
- Leslie Lamport,
- Donald E. Knuth,
- Dawson Engler (Stanford, outil Coverity)
- Jean-Yves Girard (logiques, démonstration... quelques articles de 'relative' vulgarisation très bien)
- Roberto Di Cosmo (impliqué dans les enjeux technologiques et stratégiques dans la société de l'information, mais aussi les isomorphismes de types),
- EricGoubault,
- OlivierTardieu,
Outils
- CEA : CAVEAT, TAO, Claire, Fluctuat,
- LRI : Why, Caduceus,
- JACK : Java Applet Correctness Kit, outil de preuve de propriétés JML) (Java Modeling Language),
- Coq : système de manipulation de preuves mathématiques formelles,
- PVS : Specification and Verification System, langage de spécification + outil de preuve,
- simplify (ne semble plus distribué seul, inclus dans ESC/Java),
- ESC/JAVA : The Compaq Extended Static Checker for Java (ESC/Java2),
- Assent : vérification de règles de programmation C du secteur de l'automobile (Misra)) + autres vérif. C + Java, commercial, version démo (Windows),
- Splint Annotation-Assisted Lightweight Static Checking (un genre de lint, mais statique)
- Coverity outil commercial, vérification de systèmes et logiciels libres, (model checking ?),
- MAGIC : Modular Analysis of proGrams In C (Clarke, model checking)
- Polyspace outil commercial, interprétation abstraite,
- Astrée, interprétation abstraite,
- AbsInt, interprétation abstraite,
- CIL, analyseur C en CAML,
- AtelierB : outil de mise en oeuvre de la méthode B, commercialisé par ClearSy,
- SMV : Symbolic Model Verifier, OpenSource,
- Splint : Annotation-Assisted Lightweight Static Checking, OpenSource,
- FlawFinder : recherche de menaces sur C/C++ (syntaxique ?), OpenSource,
- SecureSoftware : commercial, Java, orienté sécurité, peu d'info techniques,
- MOPS : MOdelchecking Programs for Security properties, langage C, OpenSource,
- KIV : a tool for formal systems development. WP, logique temporelle, outil de preuve, logique d'ordre supérieur, machines à état, 250 pages de cours (!), licence non commercial gratuite pour un an.
- Maxima (autre site en français) : logiciel de calcul formel (style Mapple ou Mathematica) distribué sous la licence GPL.
Slicing
- Literature survey on program slicing, Jeff Russell,
- plein de liens relatifs au slicing,
- Aristitle Reseach Group : Program Analysis Based Software Engineering,
- Michael D. Ernst,
- Daniel Weise,
- ProgramTransformation,
- Mark Harman's Publications (dont papiers sur le "Pre/Post conditioned slicing" et le Amorphous Slicing), (Nouvelle adresse),
- VASTT,
- GUSTT : GUided Slicing and Targeted Transformation,
- Outil en ligne (Amorphous Slicing),
- Dave Binkley
- GoldsmithsUniversity,
- SebastienDanicic,
- ThomasReps,
- CodeSurfer,
- Ghinsu,
- John Hatcliff et l'outil Indus
Autres liens
- FormalMethods, FormalMethodsEurope,
- ModelChecking (liens),
- Parallélisme (cours d'Eric) : voir surtout son poly,
- ProofCarryingCode,
- ProgramTransformation,
- IntroPreuveFormelle,
- LambdaTheUltimate,
- ProofsAndTypes,
- Structure and Interpretation of Computer Programs,
- Pi-Calcul,
- Separation Logic : Short Courses, Intro & links,
- PlanetMath.org : Lattice,...
- Qiang Wu : bon résumé sur l'analyse d'alias,
