diff --git a/_fc-publications/aorai/2009-afadl-gs.md b/_fc-publications/aorai/2009-afadl-gs.md index 147c1077fc203f75c635387b58ae5c04e60bcd58..3dad3d2cab025fa7ab8b02f72d326a0506e67bd0 100644 --- a/_fc-publications/aorai/2009-afadl-gs.md +++ b/_fc-publications/aorai/2009-afadl-gs.md @@ -3,7 +3,7 @@ plugin: "aorai" authors: "Julien Groslambert and 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 +link: "http://hal.archives-ouvertes.fr/inria-00568947" year: 2009 category: foundational short: "In French." diff --git a/_fc-publications/c2s/2016-scam-bkll.md b/_fc-publications/c2s/2016-scam-bkll.md index 9bde06f47f7b0ce8716175b258d902e95225b9ab..77e836ee84fe734d6e4442e666febe94311a3266 100644 --- a/_fc-publications/c2s/2016-scam-bkll.md +++ b/_fc-publications/c2s/2016-scam-bkll.md @@ -3,7 +3,7 @@ plugin: "c2s" authors: "Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre and 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 +link: "https://hal.archives-ouvertes.fr/hal-01423641/en" doi: "10.1109/SCAM.2016.18" year: 2016 category: foundational diff --git a/_fc-publications/c2s/2017-lifo-blk.md b/_fc-publications/c2s/2017-lifo-blk.md index 41bf1721e8d1f2436415f5f048e53ae62c3d850a..b3b23ac11471e7b8f768cb4eaf1f4cdfbe5cf814 100644 --- a/_fc-publications/c2s/2017-lifo-blk.md +++ b/_fc-publications/c2s/2017-lifo-blk.md @@ -3,7 +3,7 @@ plugin: "c2s" authors: "Allan Blanchard, Nikolai Kosmatov and 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 +link: "https://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2017/RR-2017-03.pdf" year: 2017 category: other short: "Complete version of \"From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation\"" diff --git a/_fc-publications/c2s/2017-vpt-blk.md b/_fc-publications/c2s/2017-vpt-blk.md index ef9b4783953a5d7c7d7dbd5ad96a3bfd6a0061c8..b9c5fb4dc5e669e6698392d006af85fedfad957b 100644 --- a/_fc-publications/c2s/2017-vpt-blk.md +++ b/_fc-publications/c2s/2017-vpt-blk.md @@ -3,7 +3,7 @@ plugin: "c2s" authors: "Allan Blanchard, Nikolai Kosmatov and 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 +link: "https://hal.archives-ouvertes.fr/hal-01495454/en" doi: "10.4204/EPTCS.253.9" year: 2017 category: foundational diff --git a/_fc-publications/celia/2011-pldi-bdes.md b/_fc-publications/celia/2011-pldi-bdes.md index 670ee21b6039fcfd0401aa2ed90bda5335342722..899dd37110a5b4152b2ec6cc5d001d4cc44cbb95 100644 --- a/_fc-publications/celia/2011-pldi-bdes.md +++ b/_fc-publications/celia/2011-pldi-bdes.md @@ -3,7 +3,7 @@ plugin: "celia" authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and 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 +link: "https://www.di.ens.fr/~cezarad/pldi11.pdf" doi: "10.1145/1993498.1993566" year: 2011 category: foundational diff --git a/_fc-publications/celia/2012-vmcai-bdes.md b/_fc-publications/celia/2012-vmcai-bdes.md index b629cd83ac2c5ec73840befec20c33399e088406..ea60ee11a7a41ecfb7254643d62953187e04cf45 100644 --- a/_fc-publications/celia/2012-vmcai-bdes.md +++ b/_fc-publications/celia/2012-vmcai-bdes.md @@ -3,7 +3,7 @@ plugin: "celia" authors: "Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and 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 +link: "https://www.irif.fr/~cenea/papers/vmcai2012-lists.pdf" doi: "10.1007/978-3-642-27940-9_1" year: 2012 category: foundational diff --git a/_fc-publications/cfp/2017-lopstr-as.md b/_fc-publications/cfp/2017-lopstr-as.md index a4b31a5944ba92c3279b3f5a6a1ee184cce5a612..1ec47b520acc8096f21d2f918a7bea89438fb3e7 100644 --- a/_fc-publications/cfp/2017-lopstr-as.md +++ b/_fc-publications/cfp/2017-lopstr-as.md @@ -3,7 +3,7 @@ plugin: "cfp" authors: "Michele Alberti and 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 +link: "http://julien.signoles.free.fr/publis/2017_lopstr.pdf" doi: "10.1007/978-3-319-94460-9_6" year: 2017 category: foundational diff --git a/_fc-publications/cost/2012-fmics-amarg.md b/_fc-publications/cost/2012-fmics-amarg.md index c22ea8fe189dd3aa84fd3e7c6e1579711d642a04..24db559554c87fd906ae0b1af5229e0092fb99f6 100644 --- a/_fc-publications/cost/2012-fmics-amarg.md +++ b/_fc-publications/cost/2012-fmics-amarg.md @@ -3,7 +3,7 @@ plugin: "cost" authors: "Nicolas Ayache, Roberto M. Amadio and 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 +link: "http://hal.inria.fr/hal-00702665/en" doi: "10.1007/978-3-642-32469-7_3" year: 2012 category: foundational diff --git a/_fc-publications/e-acsl/2013-rv-kps.md b/_fc-publications/e-acsl/2013-rv-kps.md index 711621d7b99262b038b8907547fd07879fcc89cf..569df651067ef2f4cfe3fb083b0e079d2aeb6a2b 100644 --- a/_fc-publications/e-acsl/2013-rv-kps.md +++ b/_fc-publications/e-acsl/2013-rv-kps.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Nikolai Kosmatov, Guillaume Petiot and 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 +link: "https://hal.archives-ouvertes.fr/cea-01834990/en" doi: "10.1007/978-3-642-40787-1_10" year: 2013 category: other diff --git a/_fc-publications/e-acsl/2013-sac-dks.md b/_fc-publications/e-acsl/2013-sac-dks.md index 679083e84a45d460da03ddaa269b9d57b5043cd6..0f5a86c2b6814118453d604232d868fc1cda4943 100644 --- a/_fc-publications/e-acsl/2013-sac-dks.md +++ b/_fc-publications/e-acsl/2013-sac-dks.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Michaël Delahaye, Nikolai Kosmatov and 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 +link: "https://hal.inria.fr/hal-00853721/en" doi: "10.1145/2480362.2480593" year: 2013 category: foundational diff --git a/_fc-publications/e-acsl/2015-jfla-jks.md b/_fc-publications/e-acsl/2015-jfla-jks.md index e29f688ff99731ea28c3dbf8f95d262cc24db12c..1c1e0a102972ea07bab32d7698af913efa0ab0d7 100644 --- a/_fc-publications/e-acsl/2015-jfla-jks.md +++ b/_fc-publications/e-acsl/2015-jfla-jks.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Arvid Jakobsson, Nikolai Kosmatov and 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 +link: "https://julien-signoles.fr/publis/2015_jfla.pdf" year: 2015 category: other short: "In French" diff --git a/_fc-publications/e-acsl/2017-ismm-vsk.md b/_fc-publications/e-acsl/2017-ismm-vsk.md index 68298e9cb8dac10017b8f7bf5c2015bb3a4b6145..57a5d4b18bf343c1f78a07242ebafd4536423033 100644 --- a/_fc-publications/e-acsl/2017-ismm-vsk.md +++ b/_fc-publications/e-acsl/2017-ismm-vsk.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Kostyantyn Vorobyov, Julien Signoles and 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 +link: "https://julien-signoles.fr/publis/2017_ismm.pdf" doi: "10.1145/3092255.3092269" year: 2017 category: foundational diff --git a/_fc-publications/e-acsl/2017-rvcubes-skv.md b/_fc-publications/e-acsl/2017-rvcubes-skv.md index f854a1278dbf4eca97e6e5e6d33ed5729ac48b74..c257dd12b448ada964268f39e4538cc06730b5bf 100644 --- a/_fc-publications/e-acsl/2017-rvcubes-skv.md +++ b/_fc-publications/e-acsl/2017-rvcubes-skv.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Julien Signoles, Nikolai Kosmatov, and 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 +link: "https://julien-signoles.fr/publis/2017_rvcubes_tool.pdf" doi: "10.29007/fpdh" year: 2017 category: foundational diff --git a/_fc-publications/e-acsl/2018-hilt-lksl.md b/_fc-publications/e-acsl/2018-hilt-lksl.md index f8d5df9fe33b9036e0972cfc9bf2c8243fb4a193..bbf1bcfec81781d4fdabe265828c8753765e2492 100644 --- a/_fc-publications/e-acsl/2018-hilt-lksl.md +++ b/_fc-publications/e-acsl/2018-hilt-lksl.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Dara Ly, Nikolai Kosmatov, Julien Signoles and 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 +link: "https://hal.archives-ouvertes.fr/cea-02283406/en" doi: "10.1145/3375408.3375416" year: 2018 category: other diff --git a/_fc-publications/e-acsl/2018-tap-vks.md b/_fc-publications/e-acsl/2018-tap-vks.md index 7442508f6571ff634b5e2a7d19e366f2aa369577..e13626a7e92946c4ac9616460f846ca747abafa6 100644 --- a/_fc-publications/e-acsl/2018-tap-vks.md +++ b/_fc-publications/e-acsl/2018-tap-vks.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Kostyantyn Vorobyov, Nikolai Kosmatov, and 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 +link: "https://julien-signoles.fr/publis/2018_tap_vorobyov.pdf" doi: "10.1007/978-3-319-92994-1_8" year: 2018 category: other diff --git a/_fc-publications/e-acsl/2020-rv-kms.md b/_fc-publications/e-acsl/2020-rv-kms.md index 29bdffc494624eab39c571238c59c83f520be9a2..e242ad7b7940da2166c1d877f41e02e747b2de2d 100644 --- a/_fc-publications/e-acsl/2020-rv-kms.md +++ b/_fc-publications/e-acsl/2020-rv-kms.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Nikolai Kosmatov, Fonenantsoa Maurica and Julien Signoles" title: "Efficient Runtime Assertion Checking for Properties over Mathematical Numbers" book: "International Conference on Runtime Verification (RV)" -link: https://julien-signoles.fr/publis/2020_rv.pdf +link: "https://julien-signoles.fr/publis/2020_rv.pdf" doi: "10.1007/978-3-030-60508-7_17" year: 2020 category: foundational diff --git a/_fc-publications/e-acsl/2020-tap-lkls.md b/_fc-publications/e-acsl/2020-tap-lkls.md index 5da825aebb3fb6441258aa6ec74b5f83278f322f..da97e560394fcf5250a7c85630d45b0958eca93d 100644 --- a/_fc-publications/e-acsl/2020-tap-lkls.md +++ b/_fc-publications/e-acsl/2020-tap-lkls.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Dara Ly, Nikolai Kosmatov, Frédéric Loulergue and Julien Signoles" title: "Verified Runtime Assertion Checking for Memory Properties" book: "International Conference on Tests and Proofs (TAP)" -link: https://hal-cea.archives-ouvertes.fr/cea-02879211/en +link: "https://hal-cea.archives-ouvertes.fr/cea-02879211/en" doi: "10.1007/978-3-030-50995-8_6" year: 2020 category: other diff --git a/_fc-publications/e-acsl/2021-vmcai-vjks.md b/_fc-publications/e-acsl/2021-vmcai-vjks.md index b87a3f5ebc7078b2070f370551bf1b7ccb19a30e..c9e0b7e2aa88c6797c2bfe82940396f448a4219d 100644 --- a/_fc-publications/e-acsl/2021-vmcai-vjks.md +++ b/_fc-publications/e-acsl/2021-vmcai-vjks.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, and Julien Signoles" title: "Runtime abstract interpretation for numerical accuracy and robustness." book: "International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)" -link: https://julien-signoles.fr/publis/2021_vmcai.pdf +link: "https://julien-signoles.fr/publis/2021_vmcai.pdf" doi: "10.1007/978-3-030-67067-2_12" year: 2021 category: other diff --git a/_fc-publications/e-acsl/2021-vortex-s.md b/_fc-publications/e-acsl/2021-vortex-s.md index 655c5e975fb9191acb7457235ca73eb3343aef12..1d861883427dd5424c1ab8d8f02d39563735d84b 100644 --- a/_fc-publications/e-acsl/2021-vortex-s.md +++ b/_fc-publications/e-acsl/2021-vortex-s.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Julien Signoles" title: "The E-ACSL Perspective on Runtime Assertion Checking" book: "International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX)" -link: https://julien-signoles.fr/publis/2021_vortex.pdf +link: "https://julien-signoles.fr/publis/2021_vortex.pdf" doi: "10.1145/3464974.3468451" year: 2021 category: other diff --git a/_fc-publications/e-acsl/2022-jfla-brs.md b/_fc-publications/e-acsl/2022-jfla-brs.md index 294670f70920e40ae47925e9360d4ace1e4b7abc..b59140d37d222c46bd81386175188f29b63c30d6 100644 --- a/_fc-publications/e-acsl/2022-jfla-brs.md +++ b/_fc-publications/e-acsl/2022-jfla-brs.md @@ -3,7 +3,7 @@ plugin: "e-acsl" authors: "Thibaut Benjamin, Felix Ridoux and Julien Signoles" title: "Formalisation d'un vérificateur efficace d'assertions arithmétiques à l'exécution" book: "Journées Francophones des Langages Applicatifs (JFLA)" -link: https://julien-signoles.fr/publis/2022_jfla.pdf +link: "https://julien-signoles.fr/publis/2022_jfla.pdf" year: 2022 category: other short: "In French" diff --git a/_fc-publications/eva/2017-vmcai-bby.md b/_fc-publications/eva/2017-vmcai-bby.md index 94a2019882746ed46de8feaeb16cf3f290c7c93f..7a2a60a03d33342354561a8ed639cbb9585bb962 100644 --- a/_fc-publications/eva/2017-vmcai-bby.md +++ b/_fc-publications/eva/2017-vmcai-bby.md @@ -3,7 +3,7 @@ plugin: "eva" authors: "Sandrine Blazy, David Bühler and Boris Yakobowski" title: "Structuring Abstract Interpreters Through State and Value Abstractions" book: "Verification, Model Checking, and Abstract Interpretation (VMCAI)" -link: https://hal-cea.archives-ouvertes.fr/cea-01808886/en +link: "https://hal-cea.archives-ouvertes.fr/cea-01808886/en" doi: "10.1007/978-3-319-52234-0_7" year: 2017 category: foundational diff --git a/_fc-publications/fanc/2012-erts-cddml.md b/_fc-publications/fanc/2012-erts-cddml.md index f2450f0b9bfc938cb3dd4b196c743d98c8b21998..6fc1429c81118ea6d5b9f490aca90e414b503a8e 100644 --- a/_fc-publications/fanc/2012-erts-cddml.md +++ b/_fc-publications/fanc/2012-erts-cddml.md @@ -3,7 +3,7 @@ plugin: "fanc" authors: "Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya Lamiel" title: "Fan-C, a Frama-C plug-in for data flow verification" book: "Proceedings of Embedded Real Time Software and Systems (ERTS²)" -link: https://hal.archives-ouvertes.fr/hal-02263407/en +link: "https://hal.archives-ouvertes.fr/hal-02263407/en" year: 2012 category: foundational --- diff --git a/_fc-publications/general/2007-minho-obbcjssp.md b/_fc-publications/general/2007-minho-obbcjssp.md index 1cd9788b1b5a93c88e9a0847d5026958ea9b17be..50069803ced3d51e75c9cec6044d7a14cb4d0399 100644 --- a/_fc-publications/general/2007-minho-obbcjssp.md +++ b/_fc-publications/general/2007-minho-obbcjssp.md @@ -3,7 +3,7 @@ plugin: general authors: "José N. Oliveira, LuÃs S. Barbosa, José B. Barros, Alcino Cunha, Maria João Frade and Jorge Sousa Pinto" title: "Formal Methods in Software Engineering" place: "University of Minho" -link: https://mei.di.uminho.pt/?q=en/1112/mfes-uk +link: "https://mei.di.uminho.pt/?q=en/1112/mfes-uk" year: 2007-2012 category: teaching --- diff --git a/_fc-publications/general/2012-moscow-k.md b/_fc-publications/general/2012-moscow-k.md index 734bd50a8cfe4464b03f074c921cf40c82748146..b99f91979be851984097768aa4454932a7674d65 100644 --- a/_fc-publications/general/2012-moscow-k.md +++ b/_fc-publications/general/2012-moscow-k.md @@ -4,7 +4,7 @@ authors: Eugene Kornykhin title: "Formal Specification and Verification" place: "Moscow State University" year: 2012-2013 -link: https://sed.ispras.ru/fmprac +link: "https://sed.ispras.ru/fmprac" category: teaching short: In Russian. --- diff --git a/_fc-publications/general/2014-college-london-pl.md b/_fc-publications/general/2014-college-london-pl.md index 5860692022bd895db910e3cac4d2a3abb597c253..ca7710cb1b83da42077f09ce95accd3abd647c8b 100644 --- a/_fc-publications/general/2014-college-london-pl.md +++ b/_fc-publications/general/2014-college-london-pl.md @@ -3,7 +3,7 @@ plugin: general authors: "Martin Peres and Steve D. Lazaro" title: "Language-based security" place: "University College London" -link: http://www.mupuf.org/blog/2014/02/10/a_return_into_the_world_of_frama-c +link: "http://www.mupuf.org/blog/2014/02/10/a_return_into_the_world_of_frama-c" year: 2014 category: teaching --- \ No newline at end of file diff --git a/_fc-publications/general/2018-hpcs-bkl.md b/_fc-publications/general/2018-hpcs-bkl.md index ea81b326341c103d2edb9a36e5ef973cf44b5818..dfe6ab04bd75ceeccc265774494dcd1270623daf 100644 --- a/_fc-publications/general/2018-hpcs-bkl.md +++ b/_fc-publications/general/2018-hpcs-bkl.md @@ -3,7 +3,7 @@ plugin: "general" authors: "Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue" title: "A Lesson on Verification of IoT Software with Frama-C" book: "International Conference on High Performance Computing & Simulation (HPCS)" -link: https://hal.inria.fr/hal-02317078/en +link: "https://hal.inria.fr/hal-02317078/en" doi: "10.1109/HPCS.2018.00018" year: 2019 category: tutorials diff --git a/_fc-publications/jessie/2007-ccv-m.md b/_fc-publications/jessie/2007-ccv-m.md index a5dacdb6d0a9e4872f79a10e2cdd994f6aec5af4..c7a58e25005cb33797b3ead7a7d6cd95ee3eb35f 100644 --- a/_fc-publications/jessie/2007-ccv-m.md +++ b/_fc-publications/jessie/2007-ccv-m.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Yannick Moy" title: "Union and Cast in Deductive Verification" book: "Proceedings of the C/C++ Verification Workshop (CCV)" -link: https://pdfs.semanticscholar.org/1fce/15dc2c6e8a42c5da1dd7e56fdb224f1e9ed1.pdf +link: "https://pdfs.semanticscholar.org/1fce/15dc2c6e8a42c5da1dd7e56fdb224f1e9ed1.pdf" year: 2007 category: foundational --- diff --git a/_fc-publications/jessie/2007-hav-hm.md b/_fc-publications/jessie/2007-hav-hm.md index 8961b812cb4480a9b1a8d91798925d3e40cfed2a..93453521cf08fad79c4b4876673de57ad2186023 100644 --- a/_fc-publications/jessie/2007-hav-hm.md +++ b/_fc-publications/jessie/2007-hav-hm.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Thierry Hubert and Claude Marché" title: "Separation analysis for deductive verification" book: "Proceedings of Heap Analysis and Verification (HAV)" -link: http://www.lri.fr/~marche/hubert07hav.pdf +link: "http://www.lri.fr/~marche/hubert07hav.pdf" year: 2007 category: foundational --- diff --git a/_fc-publications/jessie/2007-hav-mm.md b/_fc-publications/jessie/2007-hav-mm.md index 758cb3b3deb7ad7137adef1abe5c0d55beb177a3..12f6ea423a8dab8ffb66c9311e42e66c8de58769 100644 --- a/_fc-publications/jessie/2007-hav-mm.md +++ b/_fc-publications/jessie/2007-hav-mm.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Yannick Moy and Claude Marché" title: "Inferring local (non-)aliasing and strings for memory safety" book: "Proceedings of Heap Analysis and Verification (HAV)" -link: https://www.researchgate.net/publication/250763933_Inferring_Local_NonAliasing_and_Strings_for_Memory_Safety_1 +link: "https://www.researchgate.net/publication/250763933_Inferring_Local_NonAliasing_and_Strings_for_Memory_Safety_1" year: 2007 category: foundational --- diff --git a/_fc-publications/jessie/2007-inria-m.md b/_fc-publications/jessie/2007-inria-m.md index f269c1e0def1bae168e458d49dc06b3afda041c6..b4f221855ef2a40c120870149e67a4a123facf9f 100644 --- a/_fc-publications/jessie/2007-inria-m.md +++ b/_fc-publications/jessie/2007-inria-m.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Yannick Moy" title: "Checking C Pointer Programs for Memory Safety" book: "INRIA Research Report n°6334" -link: https://hal.inria.fr/inria-00181950/en +link: "https://hal.inria.fr/inria-00181950/en" year: 2007 category: foundational --- diff --git a/_fc-publications/jessie/2008-vmcai-m.md b/_fc-publications/jessie/2008-vmcai-m.md index c34e1eaa860a5d1da930cd42da2518ea49b069c9..b2b5acf6a482b078c6dbe29f0a7f8202fd353242 100644 --- a/_fc-publications/jessie/2008-vmcai-m.md +++ b/_fc-publications/jessie/2008-vmcai-m.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Yannick Moy" title: "Sufficient Preconditions for Modular Assertion Checking" book: "Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)" -link: https://link.springer.com/chapter/10.1007/978-3-540-78163-9_18 +link: "https://link.springer.com/chapter/10.1007/978-3-540-78163-9_18" doi: "10.1007/978-3-540-78163-9_18" year: 2008 category: foundational diff --git a/_fc-publications/jessie/2009-inria-a.md b/_fc-publications/jessie/2009-inria-a.md index c5445c07db69a54341af145cf591ead2f666e892..e9c193c1763757dae797146bddd8c1c6603cf59d 100644 --- a/_fc-publications/jessie/2009-inria-a.md +++ b/_fc-publications/jessie/2009-inria-a.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Ali Ayad" title: "On formal methods for certifying floating-point C programs" book: "Research Report RR-6927, INRIA" -link: http://hal.inria.fr/inria-00383793/en/ +link: "http://hal.inria.fr/inria-00383793/en/" year: 2009 category: foundational --- diff --git a/_fc-publications/jessie/2010-calculemus-bhmt.md b/_fc-publications/jessie/2010-calculemus-bhmt.md index b186bebb8cdc501da4064a31c6b94b5a57c63670..b29287f220bb9da0cedf47db12ae10c92bc90e19 100644 --- a/_fc-publications/jessie/2010-calculemus-bhmt.md +++ b/_fc-publications/jessie/2010-calculemus-bhmt.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Franck Butelle, Florent Hivert, Micaela Mayero and Frédéric Toumazet" title: "Formal Proof of SCHUR Conjugate Function" book: "Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (CALCULEMUS)" -link: http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf +link: "http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf" doi: "10.1007/978-3-642-14128-7_15" year: 2010 category: other diff --git a/_fc-publications/jessie/2010-erts-dgmlp.md b/_fc-publications/jessie/2010-erts-dgmlp.md index 7c227d9317ad8f6bc328697980ea2439b546bdae..ecf6ad558ad31bdba6db1d9204f29edfa9fa4380 100644 --- a/_fc-publications/jessie/2010-erts-dgmlp.md +++ b/_fc-publications/jessie/2010-erts-dgmlp.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Stéphane Duprat, Pierre Gaufillet, Victoria Moya Lamiel and Frédéric Passarello" title: "Formal verification of SAM state machine implementation" book: "Proceedings of Embedded Real Time Software and Systems (ERTS²)" -link: https://www.researchgate.net/publication/265141424_Formal_verification_of_SAM_state_machine_implementation +link: "https://www.researchgate.net/publication/265141424_Formal_verification_of_SAM_state_machine_implementation" year: 2010 category: other --- diff --git a/_fc-publications/jessie/2010-jsc-mm.md b/_fc-publications/jessie/2010-jsc-mm.md index 2b8d8da82853d653568a194fbdf072c1e968e8aa..35e37b7a9c342b364d1fd4a2988543205f5c6a36 100644 --- a/_fc-publications/jessie/2010-jsc-mm.md +++ b/_fc-publications/jessie/2010-jsc-mm.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Yannick Moy and Claude Marché" title: "Modular inference of subprogram contracts for safety checking" book: "Journal of Symbolic Computation" -link: http://hal.inria.fr/inria-00534331/en +link: "http://hal.inria.fr/inria-00534331/en" doi: "10.1016/j.jsc.2010.06.004" year: 2010 category: foundational diff --git a/_fc-publications/jessie/2010-nfm-bn.md b/_fc-publications/jessie/2010-nfm-bn.md index 0aeb6bb62911fad82b8d4a4265a2692131216546..c856eefc35f5ed4ad0fad5e4e3479c4bc145e19c 100644 --- a/_fc-publications/jessie/2010-nfm-bn.md +++ b/_fc-publications/jessie/2010-nfm-bn.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Sylvie Boldo and Thi Minh Tuyen Nguyen" title: "Proofs of numerical programs when the compiler optimizes" book: "Innovations in Systems and Software Engineering" -link: https://hal.inria.fr/hal-00777639/document +link: "https://hal.inria.fr/hal-00777639/document" doi: "10.1007/s11334-011-0151-6" year: 2011 category: foundational diff --git a/_fc-publications/jessie/2013-nfm-gmkc.md b/_fc-publications/jessie/2013-nfm-gmkc.md index 8ac749ee3e66d3ecc2f08fc7d5c3fccb59b1de8e..8b0ecdb8d6d3ce148abf5f95acf2308045f41b66 100644 --- a/_fc-publications/jessie/2013-nfm-gmkc.md +++ b/_fc-publications/jessie/2013-nfm-gmkc.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Alwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson" title: "Verification of Numerical Programs: From Real Numbers to Floating Point Numbers" book: "NASA Formal Methods (NFM)" -link: https://shemesh.larc.nasa.gov/people/cam/publications/nfm2013-draft.pdf +link: "https://shemesh.larc.nasa.gov/people/cam/publications/nfm2013-draft.pdf" doi: "10.1007/978-3-642-38088-4_31" year: 2013 category: other diff --git a/_fc-publications/jessie/2013-sac-kps.md b/_fc-publications/jessie/2013-sac-kps.md index 8987e43f855403455b7aa2276625624c44840dbf..d999d90692bd4cbc969f7fc1c656a9b07baf9d5c 100644 --- a/_fc-publications/jessie/2013-sac-kps.md +++ b/_fc-publications/jessie/2013-sac-kps.md @@ -3,7 +3,7 @@ plugin: "jessie" authors: "Nikolai Kosmatov, Virgile Prevosto and Julien Signoles" title: "Specification and Proof of Programs with Frama-C" book: "28th Symposium on Applied Computing (SAC)" -link: http://www.sigapp.org/sac/sac2013/T4.pdf +link: "http://www.sigapp.org/sac/sac2013/T4.pdf" year: 2013 category: tutorials --- diff --git a/_fc-publications/ltest/2014-tap-bcdk.md b/_fc-publications/ltest/2014-tap-bcdk.md index e6201289fb1138831c33bb5189ccdf4c17dfa3f9..0543a9ce42d582f53a7a87f7a0abe92467afcf7c 100644 --- a/_fc-publications/ltest/2014-tap-bcdk.md +++ b/_fc-publications/ltest/2014-tap-bcdk.md @@ -3,7 +3,7 @@ plugin: "ltest" authors: "Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, and Nikolai Kosmatov" title: "An All-in-One Toolkit for Automated White-Box Testing" book: "International Conference on Tests and Proofs (TAP)" -link: https://hal-cea.archives-ouvertes.fr/cea-01834983v1 +link: "https://hal-cea.archives-ouvertes.fr/cea-01834983v1" doi: "10.1007/978-3-319-09099-3_4" year: 2014 category: foundational diff --git a/_fc-publications/ltest/2017-icst-mbdkv.md b/_fc-publications/ltest/2017-icst-mbdkv.md index 9d496052e79ef820ee4e8207d8a4578ae34e3caf..2870411a46785efda9a995108ae21f1f57a4ce83 100644 --- a/_fc-publications/ltest/2017-icst-mbdkv.md +++ b/_fc-publications/ltest/2017-icst-mbdkv.md @@ -3,7 +3,7 @@ plugin: "ltest" authors: "Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, and Virgile Prevosto" title: "Taming Coverage Criteria Heterogeneity with LTest" book: "International Conference on Software Testing, Verification and Validation (ICST)" -link: https://hal-cea.archives-ouvertes.fr/cea-01808788v1 +link: "https://hal-cea.archives-ouvertes.fr/cea-01808788v1" doi: "10.1109/ICST.2017.57" year: 2017 category: foundational diff --git a/_fc-publications/ltest/2018-icse-mpbkpc.md b/_fc-publications/ltest/2018-icse-mpbkpc.md index f88f179b8993af2b481af8e25caa163c8e9c88cb..5260160cbebfc8a9155f2a3ef657992d9b7116da 100644 --- a/_fc-publications/ltest/2018-icse-mpbkpc.md +++ b/_fc-publications/ltest/2018-icse-mpbkpc.md @@ -3,7 +3,7 @@ plugin: "ltest" authors: "Michaël Marcozzi, Mike Papadakis, Sébastien Bardin, Nikolai Kosmatov, Virgile Prévosto, and Loic Correnson" title: "Time to Clean Your Test Objectives" book: "International Conference On Software Engineering (ICSE)" -link: https://hal-cea.archives-ouvertes.fr/cea-01835503 +link: "https://hal-cea.archives-ouvertes.fr/cea-01835503" doi: "10.1145/3180155.3180191" year: 2018 category: other diff --git a/_fc-publications/ltest/2020-ifm-mkpl.md b/_fc-publications/ltest/2020-ifm-mkpl.md index 8726480e6d065427803b8492e4ee47bd7bb2bc65..ce192dab791aa923461ca66f901699cbf51e5631 100644 --- a/_fc-publications/ltest/2020-ifm-mkpl.md +++ b/_fc-publications/ltest/2020-ifm-mkpl.md @@ -3,7 +3,7 @@ plugin: "ltest" authors: "Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, and Matthieu Lemerre" title: "Detection of Polluting Test Objectives for Dataflow Criteria" book: "International Conference on Integrated Formal Methods (IFM)" -link: https://hal-cea.archives-ouvertes.fr/cea-02974228 +link: "https://hal-cea.archives-ouvertes.fr/cea-02974228" doi: "10.1007/978-3-030-63461-2_18" year: 2020 category: foundational diff --git a/_fc-publications/metacsl/2019-tacas-rkprlg.md b/_fc-publications/metacsl/2019-tacas-rkprlg.md index 855394ed33fc9a624fddbfe3c29c5dae563144b3..b175330782f0d36b976aa4176f37ec30332054a9 100644 --- a/_fc-publications/metacsl/2019-tacas-rkprlg.md +++ b/_fc-publications/metacsl/2019-tacas-rkprlg.md @@ -3,7 +3,7 @@ plugin: "metacsl" authors: "Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall" title: "MetAcsl: Specification and Verification of High-Level Properties" book: "International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)" -link: https://hal-cea.archives-ouvertes.fr/cea-02019790/en +link: "https://hal-cea.archives-ouvertes.fr/cea-02019790/en" doi: "10.1007/978-3-030-17462-0_22" year: 2019 category: foundational diff --git a/_fc-publications/metacsl/2019-tap-rkvrlg.md b/_fc-publications/metacsl/2019-tap-rkvrlg.md index e71953680257b9a8d9c070e6f8b36590b90f0837..2d723e8cadd62d830c16058ae6f348def3aa5dbf 100644 --- a/_fc-publications/metacsl/2019-tap-rkvrlg.md +++ b/_fc-publications/metacsl/2019-tap-rkvrlg.md @@ -3,7 +3,7 @@ plugin: "metacsl" authors: "Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall" title: "Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties" book: "Tests and Proofs (TAP)" -link: https://hal.archives-ouvertes.fr/cea-02301892/en +link: "https://hal.archives-ouvertes.fr/cea-02301892/en" doi: "10.1007/978-3-030-31157-5_11" year: 2019 category: foundational diff --git a/_fc-publications/pathcrawler/2004-ase-wmm.md b/_fc-publications/pathcrawler/2004-ase-wmm.md index 1a79f01f6ab43b294904cd6d067e7d6afde09138..064e71e2b766a6feeea71eeb6a4969fafb3a0b79 100644 --- a/_fc-publications/pathcrawler/2004-ase-wmm.md +++ b/_fc-publications/pathcrawler/2004-ase-wmm.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nicky Williams, Bruno Marre and Patricia Mouy" title: "On-the-fly generation of k-paths tests for C functions: towards the automation of grey-box testing" book: "International Conference on Automated Software Engineering (ASE)" -link: https://hal.archives-ouvertes.fr/hal-01810203/en +link: "https://hal.archives-ouvertes.fr/hal-01810203/en" year: 2004 category: foundational --- diff --git a/_fc-publications/pathcrawler/2005-edcc-wmmr.md b/_fc-publications/pathcrawler/2005-edcc-wmmr.md index 255c8007fcd7a32e19d0258fd70fb5be8112c78a..3cd70256003a945a7eeb8c7752c4c7eab4f26791 100644 --- a/_fc-publications/pathcrawler/2005-edcc-wmmr.md +++ b/_fc-publications/pathcrawler/2005-edcc-wmmr.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nicky Williams, Bruno Marre, Patricia Mouy and Muriel Roger" title: "PathCrawler: automatic generation of path tests by combining static and dynamic analysis" book: "European Dependable Computing Conference (EDCC)" -link: https://hal.archives-ouvertes.fr/hal-01810201/en +link: "https://hal.archives-ouvertes.fr/hal-01810201/en" doi: "10.1007/11408901_21" year: 2005 category: foundational diff --git a/_fc-publications/pathcrawler/2005-wcet-w.md b/_fc-publications/pathcrawler/2005-wcet-w.md index cd18e05435d338f7b2b6bbbeedff648c3e9a5221..16f3b03401bcffd7cc3b6e0ecaf406cf4d372f7c 100644 --- a/_fc-publications/pathcrawler/2005-wcet-w.md +++ b/_fc-publications/pathcrawler/2005-wcet-w.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nicky Williams" title: "WCET measurement using modified path testing" book: "International Workshop on Worst-Case Execution Time Analysis (WCET)" -link: https://hal.archives-ouvertes.fr/hal-01810200/en +link: "https://hal.archives-ouvertes.fr/hal-01810200/en" doi: "10.4230/OASIcs.WCET.2005.809" year: 2005 category: other diff --git a/_fc-publications/pathcrawler/2008-icst-mmwlg.md b/_fc-publications/pathcrawler/2008-icst-mmwlg.md index 345c7c6362f0b08bd1ca1cb461f09e415292f23e..ae8fe70074cfff1b55f3e85d6a3d8cc343d6dfc2 100644 --- a/_fc-publications/pathcrawler/2008-icst-mmwlg.md +++ b/_fc-publications/pathcrawler/2008-icst-mmwlg.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Patricia Mouy, Bruno Marre, Nicky Williams and Pascale Le Gall" title: "Generation of all-paths unit test with function calls" book: "International Conference on Software Testing, Verification, and Validation (ICST)" -link: https://hal.archives-ouvertes.fr/hal-01810199/en +link: "https://hal.archives-ouvertes.fr/hal-01810199/en" doi: "10.1109/ICST.2008.35" year: 2008 category: other diff --git a/_fc-publications/pathcrawler/2008-issre-k.md b/_fc-publications/pathcrawler/2008-issre-k.md index ab7f370a9c3325ac7ccfc865738e3dd97c0347de..935872fbde98c88127052fa3d2015afb9e17f45e 100644 --- a/_fc-publications/pathcrawler/2008-issre-k.md +++ b/_fc-publications/pathcrawler/2008-issre-k.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nikolai Kosmatov" title: "All-paths test generation for programs with internal aliases" book: "International Symposium on Software Reliability Engineering (ISSRE)" -link: http://nikolai.kosmatov.free.fr/publications/kosmatov_issre_2008.pdf +link: "http://nikolai.kosmatov.free.fr/publications/kosmatov_issre_2008.pdf" doi: "10.1109/ISSRE.2008.25" year: 2008 category: other diff --git a/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md b/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md index d20d9fe0fb3f8753943bdacc73675231fd8d5f19..04a193a028218e09ae3d927dd775467667a77ac5 100644 --- a/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md +++ b/_fc-publications/pathcrawler/2009-ast-bdhthkmrw.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger and Nicky Williams" title: "Automating Structural Testing of C Programs: Experience with PathCrawler" book: "International Workshop on Automation of Software Test (AST)" -link: https://ieeexplore.ieee.org/document/5069043 +link: "https://ieeexplore.ieee.org/document/5069043" doi: "10.1109/IWAST.2009.5069043" year: 2009 category: other diff --git a/_fc-publications/pathcrawler/2009-ast-wr.md b/_fc-publications/pathcrawler/2009-ast-wr.md index 1d2f74b9bef84eb87e502b8d8c252d4caa069b66..c1103bed2054e42c0d21527ede0ad62246267f89 100644 --- a/_fc-publications/pathcrawler/2009-ast-wr.md +++ b/_fc-publications/pathcrawler/2009-ast-wr.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nicky Williams and Muriel Roger" title: "Test Generation Strategies to Measure Worst-Case Execution Time" book: "International Workshop on Automation of Software Test (AST)" -link: https://ieeexplore.ieee.org/document/5069045 +link: "https://ieeexplore.ieee.org/document/5069045" doi: "10.1109/IWAST.2009.5069045" year: 2009 category: other diff --git a/_fc-publications/pathcrawler/2009-taic-part-k.md b/_fc-publications/pathcrawler/2009-taic-part-k.md index 3c98390629b3835ad1def133fc7eb68b89be2c67..ee244b6be9410ec6f570b4ecf4b67542708c5fb8 100644 --- a/_fc-publications/pathcrawler/2009-taic-part-k.md +++ b/_fc-publications/pathcrawler/2009-taic-part-k.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nikolai Kosmatov" title: "On Complexity of All-Paths Test Generation. From Practice to Theory" book: "Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART)" -link: https://ieeexplore.ieee.org/document/5381631 +link: "https://ieeexplore.ieee.org/document/5381631" doi: "10.1109/TAICPART.2009.26" year: 2009 category: other diff --git a/_fc-publications/pathcrawler/2010-ast-w.md b/_fc-publications/pathcrawler/2010-ast-w.md index 5d9aa2c868d1e3d82d327924c62e304c12e5cd4b..a909923094ae9e88880c4a2941ac377c4dd63964 100644 --- a/_fc-publications/pathcrawler/2010-ast-w.md +++ b/_fc-publications/pathcrawler/2010-ast-w.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nicky Williams" title: "Abstract path testing with PathCrawler" book: "International Workshop on Automation of Software Test (AST)" -link: https://hal.archives-ouvertes.fr/hal-01810297/en +link: "https://hal.archives-ouvertes.fr/hal-01810297/en" doi: "10.1145/1808266.1808272" year: 2010 category: other diff --git a/_fc-publications/pathcrawler/2011-cstva-kbrw.md b/_fc-publications/pathcrawler/2011-cstva-kbrw.md index afe0967d4b06f2f3d29ac948c24f6adfe2f8a91b..5b0930e729ee66ab4db25ffa15a15a0bce51df08 100644 --- a/_fc-publications/pathcrawler/2011-cstva-kbrw.md +++ b/_fc-publications/pathcrawler/2011-cstva-kbrw.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nikolai Kosmatov, Bernard Botella, Muriel Roger and Nicky Williams" title: "Online Test Generation with PathCrawler. Tool demo." book: "International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA)" -link: https://nikolai-kosmatov.eu/publications/kosmatov_brw_cstva_2011.pdf +link: "https://nikolai-kosmatov.eu/publications/kosmatov_brw_cstva_2011.pdf" doi: "10.1109/ICSTW.2011.85" year: 2011 category: other diff --git a/_fc-publications/pathcrawler/2012-qsic-wk.md b/_fc-publications/pathcrawler/2012-qsic-wk.md index 2b29b433f4042cc056b5636800c3f6360949ed96..5289d8758b41293fd7d1a9a0b4459e053b89a77b 100644 --- a/_fc-publications/pathcrawler/2012-qsic-wk.md +++ b/_fc-publications/pathcrawler/2012-qsic-wk.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nicky Williams and Nikolai Kosmatov" title: "Structural Testing with PathCrawler. Tutorial Synopsis" book: "International Conference on Quality Software (QSIC)" -link: https://hal.archives-ouvertes.fr/hal-01810295/ +link: "https://hal.archives-ouvertes.fr/hal-01810295/" doi: "10.1109/QSIC.2012.24" year: 2012 category: tutorials diff --git a/_fc-publications/pathcrawler/2012-tap-kwbrc.md b/_fc-publications/pathcrawler/2012-tap-kwbrc.md index 294c880c929abac4aa93d384d7264537aabb4977..de71dc72058da2baadfa7df6be38a74765765e03 100644 --- a/_fc-publications/pathcrawler/2012-tap-kwbrc.md +++ b/_fc-publications/pathcrawler/2012-tap-kwbrc.md @@ -3,7 +3,7 @@ plugin: "pathcrawler" authors: "Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro" title: "A Lesson on Structural Testing with PathCrawler-online.com" book: "International Conference on Tests and Proofs (TAP)" -link: https://hal.archives-ouvertes.fr/hal-01810295/en +link: "https://hal.archives-ouvertes.fr/hal-01810295/en" doi: "10.1007/978-3-642-30473-6_15" year: 2012 category: tutorials diff --git a/_fc-publications/rpp/2017-tacas-bklgp.md b/_fc-publications/rpp/2017-tacas-bklgp.md index 6a7006c24301b222b82dacef1e246708c87dbbd3..8c46be7237f8ebfe09ffdc8dc200a5bb7cfeffc4 100644 --- a/_fc-publications/rpp/2017-tacas-bklgp.md +++ b/_fc-publications/rpp/2017-tacas-bklgp.md @@ -3,7 +3,7 @@ plugin: "rpp" authors: "Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall and Virgile Prevosto" title: "RPP: Automatic Proof of Relational Properties by Self-composition" book: "Tools and Algorithms for the Construction and Analysis of Systems23rd International Conference, TACAS" -link: https://hal-cea.archives-ouvertes.fr/cea-01808885/en +link: "https://hal-cea.archives-ouvertes.fr/cea-01808885/en" doi: "10.1007/978-3-662-54577-5_22" year: 2017 category: foundational diff --git a/_fc-publications/rpp/2018-tap-bklgpp.md b/_fc-publications/rpp/2018-tap-bklgpp.md index dc1abb8a2affe357135a359cf4376d2f8b3e8e3e..5f2be4e14c1fb649365198dc819a5be87670624e 100644 --- a/_fc-publications/rpp/2018-tap-bklgpp.md +++ b/_fc-publications/rpp/2018-tap-bklgpp.md @@ -3,7 +3,7 @@ plugin: "rpp" authors: "Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto and Guillaume Petiot" title: "Static and Dynamic Verification of Relational Properties on Self-composed C Code" book: "In Tests and Proofs - 12th International Conference (TAP)" -link: https://hal-cea.archives-ouvertes.fr/cea-01835470/en +link: "https://hal-cea.archives-ouvertes.fr/cea-01835470/en" doi: "10.1007/978-3-319-92994-1_3" year: 2018 category: foundational diff --git a/_fc-publications/sante/2010-tap-ckgj.md b/_fc-publications/sante/2010-tap-ckgj.md index 05746b3d399cbf97825377718a69dc6154793676..4096d592991f18b186f523742021617a7f6f9cfa 100644 --- a/_fc-publications/sante/2010-tap-ckgj.md +++ b/_fc-publications/sante/2010-tap-ckgj.md @@ -3,7 +3,7 @@ plugin: "sante" authors: "Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand" title: "Combining static analysis and test generation for C program debugging" book: "Proceedings of the 4th International Conference on Tests & Proofs (TAP)" -link: https://hal.archives-ouvertes.fr/hal-00563308/en +link: "https://hal.archives-ouvertes.fr/hal-00563308/en" doi: "10.1007/978-3-642-13977-2_9" year: 2010 category: foundational diff --git a/_fc-publications/sante/2011-tap-ckgj.md b/_fc-publications/sante/2011-tap-ckgj.md index e5cc3085f52a51da9bd11f399005ffe5ee202b66..e904b311bcf3dc4dc1a90bdac19ca02beacb9174 100644 --- a/_fc-publications/sante/2011-tap-ckgj.md +++ b/_fc-publications/sante/2011-tap-ckgj.md @@ -3,7 +3,7 @@ plugin: "sante" authors: "Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand" title: "The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging" book: "Proceedings of the 5th International Conference on Tests & Proofs (TAP)" -link: https://hal.inria.fr/inria-00622904/en +link: "https://hal.inria.fr/inria-00622904/en" doi: "10.1007/978-3-642-21768-5_7" year: 2011 category: foundational diff --git a/_fc-publications/sante/2012-sac-ckgj.md b/_fc-publications/sante/2012-sac-ckgj.md index f5e220807cd1e9dfba868f0ca1b9feb7591ae7e2..cf0d045560f304b0817249f7f7987214f5979dc4 100644 --- a/_fc-publications/sante/2012-sac-ckgj.md +++ b/_fc-publications/sante/2012-sac-ckgj.md @@ -3,7 +3,7 @@ plugin: "sante" authors: "Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand" title: "Program slicing enhances a verification technique combining static and dynamic analysis" book: "Proceedings of the 27th Symposium On Applied Computing (SAC)" -link: https://hal.inria.fr/hal-00746814/en +link: "https://hal.inria.fr/hal-00746814/en" doi: "10.1145/2245276.2231980" year: 2012 category: foundational diff --git a/_fc-publications/secureflow/2013-sec-astt.md b/_fc-publications/secureflow/2013-sec-astt.md index 8e94eb054f4e53696ea841f4a5aba2a61c801ddf..71baf12934b23e8c02371cd2a24c97566aec81d8 100644 --- a/_fc-publications/secureflow/2013-sec-astt.md +++ b/_fc-publications/secureflow/2013-sec-astt.md @@ -3,7 +3,7 @@ plugin: "secureflow" authors: "Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel" title: "Program transformation for non-interference verification on programs with pointers" book: "International Information Security and Privacy Conference (SEC)" -link: http://julien.signoles.free.fr/publis/2013_sec.pdf +link: "http://julien.signoles.free.fr/publis/2013_sec.pdf" doi: "10.1007/978-3-642-39218-4_18" year: 2013 category: foundational diff --git a/_fc-publications/secureflow/2017-tap-bs.md b/_fc-publications/secureflow/2017-tap-bs.md index 707dfe5b46123ca083e9eb58caad9f79a4de5340..3635c38d333879f130b0d5f27115a9d34f1756dd 100644 --- a/_fc-publications/secureflow/2017-tap-bs.md +++ b/_fc-publications/secureflow/2017-tap-bs.md @@ -3,7 +3,7 @@ plugin: "secureflow" authors: "Gergö Barany and Julien Signoles" title: "Hybrid Information Flow Analysis for Real-World C Code" book: "International Conference on Tests and Proofs (TAP)" -link: http://julien.signoles.free.fr/publis/2017_tap.pdf +link: "http://julien.signoles.free.fr/publis/2017_tap.pdf" doi: "10.1007/978-3-319-61467-0_2" year: 2017 category: foundational diff --git a/_fc-publications/sidan/2009-crisis-dtt.md b/_fc-publications/sidan/2009-crisis-dtt.md index a3bc09dec389338a2d06f52a2b40483caed72286..174effab99bc972785146c27bcb2eb7b67f67600 100644 --- a/_fc-publications/sidan/2009-crisis-dtt.md +++ b/_fc-publications/sidan/2009-crisis-dtt.md @@ -3,7 +3,7 @@ plugin: "sidan" authors: "Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel" title: "SIDAN: a tool dedicated to Software Instrumentation for Detecting Attacks on Non-control-data" book: "4th International Conference on Risks and Security of Internet and Systems (CRISIS)" -link: https://hal.archives-ouvertes.fr/hal-00424574/en +link: "https://hal.archives-ouvertes.fr/hal-00424574/en" doi: "10.1109/CRISIS.2009.5411977" year: 2009 category: foundational diff --git a/_fc-publications/slicing/2008-trust-ms.md b/_fc-publications/slicing/2008-trust-ms.md index 390e80574930501354babf29c4ae6fa1ad6eb5d2..e4e8f9f64174b8da5d32f1aa2faa2128d1090821 100644 --- a/_fc-publications/slicing/2008-trust-ms.md +++ b/_fc-publications/slicing/2008-trust-ms.md @@ -3,7 +3,7 @@ plugin: "slicing" authors: "Benjamin Monate and Julien Signoles" title: "Slicing for Security of Code" book: "Proceedings of the 1st international conference on Trusted Computing and Trust in Information Technologies (TRUST)" -link: http://julien.signoles.free.fr/publis/2008_trust.pdf +link: "http://julien.signoles.free.fr/publis/2008_trust.pdf" doi: "10.1007/978-3-540-68979-9_10" year: 2008 category: foundational diff --git a/_fc-publications/stac/2010-mdv-cmp.md b/_fc-publications/stac/2010-mdv-cmp.md index b3a875e9bbda6f6b10de46a8ae55a682ad6b8633..242e585e8436026651329a8cdcd748180385fe03 100644 --- a/_fc-publications/stac/2010-mdv-cmp.md +++ b/_fc-publications/stac/2010-mdv-cmp.md @@ -3,7 +3,7 @@ plugin: "stac" authors: "Dumitru Ceara, Laurent Mounier and Marie-Laure Potet" title: "Taint Dependency Sequences: a characterization of insecure execution paths based on input-sensitive cause sequences" book: "Modeling and Detecting Vulnerabilities workshop (MDV)" -link: http://www-verimag.imag.fr/PEOPLE/mounier/Papers/mdv10.pdf +link: "http://www-verimag.imag.fr/PEOPLE/mounier/Papers/mdv10.pdf" doi: "10.1109/ICSTW.2010.28" year: 2010 category: foundational diff --git a/_fc-publications/stady/2014-scam-pkbgj.md b/_fc-publications/stady/2014-scam-pkbgj.md index 24647b20d16b66b9e72c1e340d55740c14a355f3..3f586d112d1e092ab547548ab5474cc744b0f76a 100644 --- a/_fc-publications/stady/2014-scam-pkbgj.md +++ b/_fc-publications/stady/2014-scam-pkbgj.md @@ -3,7 +3,7 @@ plugin: "stady" authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti and Jacques Julliand" title: "Instrumentation of Annotated C Programs for Test Generation" book: "14th International Working Conference on Source Code Analysis and Manipulation (SCAM)" -link: https://hal.archives-ouvertes.fr/cea-01836306/en +link: "https://hal.archives-ouvertes.fr/cea-01836306/en" doi: "10.1109/SCAM.2014.19" year: 2014 category: foundational diff --git a/_fc-publications/stady/2014-tap-pkgj.md b/_fc-publications/stady/2014-tap-pkgj.md index 10e49197abc5f6f1e35d9042ea8f7b6c803bc83a..d47d773e44c24a555ba737a427c53e6b2c118efc 100644 --- a/_fc-publications/stady/2014-tap-pkgj.md +++ b/_fc-publications/stady/2014-tap-pkgj.md @@ -3,7 +3,7 @@ plugin: "stady" authors: "Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti and Jacques Julliand" title: "How Test Generation Helps Software Specification and Deductive Verification in Frama-C" book: "International Conference on Tests and Proofs (TAP)" -link: https://hal.inria.fr/hal-01108553/en +link: "https://hal.inria.fr/hal-01108553/en" doi: "10.1007/978-3-319-09099-3_16" year: 2014 category: foundational diff --git a/_fc-publications/stady/2016-tap-pkbgj.md b/_fc-publications/stady/2016-tap-pkbgj.md index d7328d2c56e4b50560472b5eee31cda1fece558f..0d7cc6c5d408fe374c83a60a1f08e977cedff38c 100644 --- a/_fc-publications/stady/2016-tap-pkbgj.md +++ b/_fc-publications/stady/2016-tap-pkbgj.md @@ -3,7 +3,7 @@ plugin: "stady" authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti and Jacques Julliand" title: "Your Proof Fails? Testing Helps to Find the Reason" book: "International Conference on Tests and Proofs (TAP)" -link: https://arxiv.org/abs/1508.01691 +link: "https://arxiv.org/abs/1508.01691" doi: "10.1007/978-3-319-41135-4_8" year: 2016 category: foundational diff --git a/_fc-publications/stady/2018-fac-pkbgj.md b/_fc-publications/stady/2018-fac-pkbgj.md index c0a94cb819a9c1ee2084672a056d8c0ef78d6102..985e10867ef2b2b727227ca92f8dc039e2e13c10 100644 --- a/_fc-publications/stady/2018-fac-pkbgj.md +++ b/_fc-publications/stady/2018-fac-pkbgj.md @@ -3,7 +3,7 @@ plugin: "stady" authors: "Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti and Jacques Julliand" title: "How testing helps to diagnose proof failures" book: "Formal Aspects of Computing, vol. 30 issue 6" -link: https://hal.archives-ouvertes.fr/hal-01948799/en +link: "https://hal.archives-ouvertes.fr/hal-01948799/en" doi: "10.1007/s00165-018-0456-4" year: 2018 category: foundational diff --git a/_fc-publications/taster/2010-erts-ddmls.md b/_fc-publications/taster/2010-erts-ddmls.md index f0ab85fc8b14e5565535489813e8aef0dd7261de..9c136a3f7af625a953cd8ee7465092d3c2cc781e 100644 --- a/_fc-publications/taster/2010-erts-ddmls.md +++ b/_fc-publications/taster/2010-erts-ddmls.md @@ -3,7 +3,7 @@ plugin: "taster" authors: "David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien Signoles" title: "Taster, a Frama-C plug-in to enforce Coding Standards" book: "Proceedings of Embedded Real Time Software and Systems (ERTS²)" -link: https://www.di.ens.fr/~delmas/papers/erts10.pdf +link: "https://www.di.ens.fr/~delmas/papers/erts10.pdf" year: 2010 category: foundational --- diff --git a/_fc-publications/wp/2012-nfm-c.md b/_fc-publications/wp/2012-nfm-c.md index 3c44ea533dbb6c2f321ba8c8ba6951e34ec501af..f56bcffcdf19316ea74b4df86383bf688bb9fb4c 100644 --- a/_fc-publications/wp/2012-nfm-c.md +++ b/_fc-publications/wp/2012-nfm-c.md @@ -3,7 +3,7 @@ plugin: "wp" authors: "Loïc Correnson" title: "Qed. Computing What Remains to Be Proved." book: "NASA Formal Methods (NFM)" -link: http://dx.doi.org/10.1007/978-3-319-06200-6_17 +link: "http://dx.doi.org/10.1007/978-3-319-06200-6_17" year: 2012 category: foundational short: "Presentation of Qed, a core library of WP that simplifies proof obligations before sending them to provers."