Merge branch 'publications/add-bibtex-entries' into 'master'

[publications] generate BibTeX entries for phdthesis/manual categories

See merge request !184

_fc-publications/README

@@ -33,29 +33,31 @@ In `_fc-publications/<your-plug-in>`, create a file named as follows:
 
 - <year of publication>-<conference/journal short name>-<initial letter of the name of each author>.md
 
-For example, for a publication, published in 2019 in the "Verification, Model
+For example, for a publication, published in 2017 in the "Verification, Model
 Checking, and Abstract Interpretation" conference, by "Sandrine Blazy, David
 Bühler and Boris Yakobowski", the path to the file is:
 
-- `_fc-publications/eva/2019-vmcai-bby.md`
+- `_fc-publications/eva/2017-vmcai-bby.md`
 
 Note that when a field does not make sense (for example, for a user manual,
 the name of the conference), it can be simply ignored, see for example:
 
-- `_fc-publications/general/user-manual.md`
+- `_fc-publications/general/frama-c-user-manual.md`
 
 Then the file is structured as follows:
 
 ```md
 ---
 plugin: <plug-in identifier>
-authors: "<the authors>"   <-- optional
-title: "<Title of the publication>
+authors: ["<author1>", "<author2>", ...] <-- optional
+title: "<Title of the publication>"
 book: "<Name of the conference/journal>" <-- optional
-place: "<University/School where the teaching takes place>" <-- optional ("teaching" category)
+school: "<University/School where the teaching/thesis takes place>" <-- optional for "teaching" category; mandatory for "phdthesis" category
 link: URL to access to the publication <-- optional
+doi: "<DOI>" <-- optional
 year: year of publication
 category: "<kind of publication>"
+type: "PhD Thesis" or "Habilitation Thesis" (mandatory, but only for "phdthesis" category)
 short: "A short description for the publication." <-- optional
 ---
 Abstract of the publication <-- optional (but highly recommended)
@@ -63,18 +65,18 @@ Abstract of the publication <-- optional (but highly recommended)
 
 In the "General" directory, the category can be:
 
-- manuals
+- manual
 - foundational
 - kernel
-- tutorials
+- tutorial
 - teaching
 
 In other directories, it can be:
 
-- manuals
-- thesis
+- manual
+- phdthesis
 - foundational
-- tutorials
+- tutorial
 - other
 - teaching
 
@@ -88,11 +90,11 @@ Notes:
 
 If your publication includes some content that should be stored on the server,
 add a directory named according to the name of your file in the `download`
-directory. For example for: `_fc-publications/eva/2019-vmcai-bby.md`, we
-should create a directory `download/publications/2019-vmcai-bby`.
+directory. For example for: `_fc-publications/eva/2017-vmcai-bby.md`, we
+should create a directory `download/publications/2017-vmcai-bby`.
 
 If you want to generate specific HTML pages for your publication (for example
 online exercices for a publication in the `teaching` category), proceed as
 above, but in the `html` directory instead of `download`. See for example
 the directory: `html/publications/2010-ensiie-vslg` and its corresponding
-publication file `_fc-publications/general/2010-ensiie-vslg`.
\ No newline at end of file
+publication file `_fc-publications/general/2010-ensiie-vslg`.

_fc-publications/aorai/2009-afadl-gs.md

 ---
 plugin: "aorai"
-authors: "Julien Groslambert and Nicolas Stouls"
+authors: ["Julien Groslambert", "Nicolas Stouls"]
 title: "Vérification de propriétés LTL sur des programmes C par génération d'annotations"
 book: "Proceedings of Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL)"
 link: "http://hal.archives-ouvertes.fr/inria-00568947"

_fc-publications/aorai/user-manual.md → _fc-publications/aorai/aorai-user-manual.md

 ---
 plugin: "aorai"
-authors: "Nicolas Stouls"
+authors: ["Nicolas Stouls"]
 title: "Aoraï Plug-in Tutorial"
 link: "http://frama-c.com/download/aorai/aorai-manual.pdf"
-category: manuals
+category: manual
 short: "The official manual of the Frama-C plug-in Aoraï."
 ---

_fc-publications/c2s/2016-scam-bkll.md

 ---
 plugin: "c2s"
-authors: "Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre and Frédéric Loulergue"
+authors: ["Allan Blanchard", "Nikolai Kosmatov", "Matthieu Lemerre", "Frédéric Loulergue"]
 title: "Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs"
 book: "16th International Working Conference on Source Code Analysis and Manipulation (SCAM)"
 link: "https://hal.archives-ouvertes.fr/hal-01423641/en"

_fc-publications/c2s/2017-lifo-blk.md

 ---
 plugin: "c2s"
-authors: "Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue"
+authors: ["Allan Blanchard", "Nikolai Kosmatov", "Frédéric Loulergue"]
 title: "Concurrent Program Verification by Code Transformation: Correctness"
 book: "LIFO Research Report RR-2017-03"
 link: "https://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2017/RR-2017-03.pdf"

_fc-publications/c2s/2017-vpt-blk.md

 ---
 plugin: "c2s"
-authors: "Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue"
+authors: ["Allan Blanchard", "Nikolai Kosmatov", "Frédéric Loulergue"]
 title: "From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation"
 book: "Fifth International Workshop on Verification and Program Transformation (VPT)"
 link: "https://hal.archives-ouvertes.fr/hal-01495454/en"

_fc-publications/celia/2011-pldi-bdes.md

 ---
 plugin: "celia"
-authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and Mihaela Sighireanu"
+authors: ["Ahmed Bouajjani", "Cezara Drăgoi", "Constantin Enea", "Mihaela Sighireanu"]
 title: "On inter-procedural analysis of programs with lists and data"
 book: "Proceedings of the 32nd Conference on Programming Language Design and Implementation (PLDI)"
 link: "https://www.di.ens.fr/~cezarad/pldi11.pdf"

_fc-publications/celia/2012-vmcai-bdes.md

 ---
 plugin: "celia"
-authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and Mihaela Sighireanu"
+authors: ["Ahmed Bouajjani", "Cezara Drăgoi", "Constantin Enea", "Mihaela Sighireanu"]
 title: "Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data"
 book: "International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI)"
 link: "https://www.irif.fr/~cenea/papers/vmcai2012-lists.pdf"

_fc-publications/cfp/2017-lopstr-as.md

 ---
 plugin: "cfp"
-authors: "Michele Alberti and Julien Signoles"
+authors: ["Michele Alberti", "Julien Signoles"]
 title: "Context Generation from Formal Specifications for C Analysis Tools"
 book: "Logic-based Program Synthesis and Transformation (LOPSTR)"
 link: "http://julien.signoles.free.fr/publis/2017_lopstr.pdf"

_fc-publications/cost/2012-fmics-amarg.md

 ---
 plugin: "cost"
-authors: "Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas"
+authors: ["Nicolas Ayache", "Roberto M. Amadio", "Yann Régis-Gianas"]
 title: "Certifying and reasoning on cost annotations in C programs"
 book: "Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS)"
 link: "http://hal.inria.fr/hal-00702665/en"

_fc-publications/e-acsl/2013-rv-kps.md

 ---
 plugin: "e-acsl"
-authors: "Nikolai Kosmatov, Guillaume Petiot and Julien Signoles"
+authors: ["Nikolai Kosmatov", "Guillaume Petiot", "Julien Signoles"]
 title: "An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs"
 book: "Proceedings of Runtime Verification (RV)"
 link: "https://hal.archives-ouvertes.fr/cea-01834990/en"

_fc-publications/e-acsl/2013-rv-ks.md

 ---
 plugin: "e-acsl"
-authors: "Nikolai Kosmatov and Julien Signoles"
+authors: ["Nikolai Kosmatov", "Julien Signoles"]
 title: "A Lesson on Runtime Assertion Checking with Frama-C"
 book: "International Conference on Runtime Verification (RV)"
 link: "https://julien-signoles.fr/publis/2013_rv.pdf"
 doi: "10.1007/978-3-642-40787-1_29"
 year: 2013
-category: tutorials
+category: tutorial
 short: "A tutorial about the Frama-C plug-in E-ACSL."
 ---
 

_fc-publications/e-acsl/2013-sac-dks.md

 ---
 plugin: "e-acsl"
-authors: "Michaël Delahaye, Nikolai Kosmatov and Julien Signoles"
+authors: ["Michaël Delahaye", "Nikolai Kosmatov", "Julien Signoles"]
 title: "Common Specification Language for Static and Dynamic Analysis of C Programs"
 book: "Proceedings of Symposium on Applied Computing (SAC)"
 link: "https://hal.inria.fr/hal-00853721/en"

_fc-publications/e-acsl/2015-jfla-jks.md

 ---
 plugin: "e-acsl"
-authors: "Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles"
+authors: ["Arvid Jakobsson", "Nikolai Kosmatov", "Julien Signoles"]
 title: "Rester statique pour devenir plus rapide, plus précis et plus mince"
 book: "Journées Francophones des Langages Applicatifs (JFLA)"
 link: "https://julien-signoles.fr/publis/2015_jfla.pdf"

_fc-publications/e-acsl/2017-ismm-vsk.md

 ---
 plugin: "e-acsl"
-authors: "Kostyantyn Vorobyov, Julien Signoles and Nikolai Kosmatov"
+authors: ["Kostyantyn Vorobyov", "Julien Signoles", "Nikolai Kosmatov"]
 title: "Shadow state encoding for efficient monitoring of block-level properties"
 book: "International Symposium on Memory Management (ISMM)"
 link: "https://julien-signoles.fr/publis/2017_ismm.pdf"

_fc-publications/e-acsl/2017-rv-vksa.md

 ---
 plugin: "e-acsl"
-authors: "Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakobsson"
+authors: ["Kostyantyn Vorobyov", "Nikolai Kosmatov", "Julien Signoles", "Arvid Jakobsson"]
 title: "Runtime detection of temporal memory errors."
 book: "International Conference on Runtime Verification (RV)"
 link: "https://julien-signoles.fr/publis/2017_rv.pdf"

_fc-publications/e-acsl/2017-rvcubes-skv.md

 ---
 plugin: "e-acsl"
-authors: "Julien Signoles, Nikolai Kosmatov, and Kostyantyn Vorobyov"
+authors: ["Julien Signoles", "Nikolai Kosmatov", "Kostyantyn Vorobyov"]
 title: "E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs. Tool Paper."
 book: "International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES)"
 link: "https://julien-signoles.fr/publis/2017_rvcubes_tool.pdf"

_fc-publications/e-acsl/2018-hilt-lksl.md

 ---
 plugin: "e-acsl"
-authors: "Dara Ly, Nikolai Kosmatov, Julien Signoles and Frédéric Loulergue"
+authors: ["Dara Ly", "Nikolai Kosmatov", "Julien Signoles", "Frédéric Loulergue"]
 title: "Soundness of a Dataflow Analysis for Memory Monitoring"
 book: "Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT)"
 link: "https://hal.archives-ouvertes.fr/cea-02283406/en"

_fc-publications/e-acsl/2018-tap-vks.md

 ---
 plugin: "e-acsl"
-authors: "Kostyantyn Vorobyov, Nikolai Kosmatov, and Julien Signoles"
+authors: ["Kostyantyn Vorobyov", "Nikolai Kosmatov", "Julien Signoles"]
 title: "Detection of Security Vulnerabilities in C Code using Runtime Verification"
 book: "International Conference on Tests and Proofs (TAP)"
 link: "https://julien-signoles.fr/publis/2018_tap_vorobyov.pdf"

_fc-publications/e-acsl/2018-thesis-signoles.md

 ---
 plugin: "e-acsl"
-authors: "Julien Signoles"
+authors: ["Julien Signoles"]
 title: "From Static Analysis to Runtime Verification with Frama-C and E-ACSL"
-book: "University of Paris Sud, Habilitation Thesis"
+school: "University of Paris Sud"
 year: "2018"
 link: "https://julien-signoles.fr/publis/hdr.pdf"
-category: "thesis"
----
\ No newline at end of file
+category: phdthesis
+type: "Habilitation Thesis"
+---