# CIR academic 2021

Articles:
- Murdoch Gabbay, Arvid Jakobsson and Kristina Sojakova. *Money Grows on (Proof-)Trees: Formalisation and Correctness of the FA1.2 Ledger Standard*. In FMBC'21. (https://arxiv.org/pdf/2109.09451.pdf)
- Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, Alain Mebsout. *Formally Documenting Tenderbake*. In FMBC'21. (https://hal.archives-ouvertes.fr/hal-03398884/document)
- Lacramioara Astefanoaei, Pierre Chambart, Antonella Del Pozzo, Thibault Rieutord, Sara Tucci, Eugen Zălinescu. *Tenderbake - A Solution to Dynamic Repeated Consensus for Blockchains*. In FAB'21. (https://arxiv.org/pdf/2001.11965.pdf)
- Valentin Chaboche, Zaynah Dargaye et Arvid Jakobsson. In JFLA'22.
*Soyez prudent : prenez des photos pour l'assurance avec Osnap.*
- J. Todd McDonald, Ramya Manikyam, Sébastien Bardin, Richard Bonichon and Todd R. Andel. *Program Protection Through Software-Based Hardware Abstraction*. In SECRYPT'21 (http://sebastien.bardin.free.fr/final-SECRYPT-2021.pdf)
- Grégoire Menguy , Sébastien Bardin , Richard Bonichon and Cauim de Souza Lima. *Search-based Approaches for Local Blackbox Deobfuscation: Understand, Improve and Mitigate*. In CCS'21. (https://binsec.github.io/assets/publications/papers/2021-ccs.pdf)
- Frédéric Recoules , Sébastien Bardin , Richard Bonichon , Matthieu Lemerre , Laurent Mounier and Marie-Laure Potet. *Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine*. In ICSE'21. *Distinguished Paper Award* (https://binsec.github.io/assets/publications/papers/2021-icse.pdf)
- Farka, F., Nanevski, A., Banerjee, A., Delbianco, G. A., and Fábregas, I. *On algebraic abstractions for concurrent separation logics.* Proceedings of the ACM on Programming Languages, POPL'21. (https://software.imdea.org/~aleks/popl21/popl21.pdf)

Workshops, Conferences:
- [FMBC'21](https://fmbc.gitlab.io/2021/index.html):
- Chair: Bruno Bernardo
- PC member: Zaynah Dargaye, Lacramioara Astefanoaei
- [CPP'21](https://popl21.sigplan.org/home/CPP-2021?#)
- Lightning talk: Formally Verified Decentralized Exchange with
Mi-Cho-Coq, Arvid Jakobsson
- Attended (remote): Germàn A. Delbianco, Boubacar Sall
- [CoqPL, POPL'21](https://popl21.sigplan.org/):
- Attended (remote): Germàn A. Delbianco, Boubacar Sall
- [CAV'21](http://cav2021.org/):
- Attended (remote): Boubacar Sall

Working groups:
- GDR Securité (https://gdr-secu-jn2021.sciencesconf.org/resource/page/id/2):
- Presentation: Formal Methods at NL (Zaynah Dargaye) (https://gdr-secu-jn2021.sciencesconf.org/data/zaynah_dargaye_fm_72022.pdf)
- [JFLA'21](http://jfla.inria.fr/jfla2021.html)
- General chair: Yann Regis-Gianas
- [JFLA'22](http://jfla.inria.fr/jfla2022.html)
- Program committee member: Diane Gallois-Wong
- Reviewers: Germàn A. Delbianco, Boubacar Sall

Academic Projects:
- TransForm (Digicosme) : Julien Tesson, German Delbianco, Zaynah Dargaye

Blog articles:
* [A Deep Dive into the Octez Prevalidator](https://research-development.nomadic-labs.com/a-deep-dive-into-the-octez-prevalidator.html): François Thiré

* [A tale of two reductions in gas consumption in Tezos](https://research-development.nomadic-labs.com/a-tale-of-two-reductions-in-gas-consumption-in-tezos.html)

ANR:
- Participation au montage : "Towards a specification language and an ecosystem to specify, test, and verify OCaml programs" : Mehdi Bouaziz,Valentin Chaboche, Zaynah Dargaye, Thomas Letan, Yann Regis-Gianas (as engineers participating in making the theoretical approach more practical, NL is use cases provider).