[23] Tiago Soares and Mário Pereira. Verificação de Programas OCaml Imperativos de Ordem Superior, através de Desfuncionalização. In INForum 2021, September 2021. [ bib | .pdf ]
[22] Carlos Pinto, Mário Pereira, and Simão Melo de Sousa. Deductive Verification of Realistic OCaml Code. In OCaml Workshop 2021, August 2021. [ bib | .pdf ]
[21] Mário Pereira and António Ravara. Cameleer: A Deductive Verification Tool for OCaml. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 677--689. Springer, 2021. [ bib | DOI | http ]
[20] Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, and Mário Pereira. GOSPEL --- Providing OCaml with a Formal Specification Language. In Annabelle McIver and Maurice ter Beek, editors, FM 2019 23rd International Symposium on Formal Methods, Porto, Portugal, October 2019. [ bib | http ]
[19] Álvaro Santos, Mário Pereira, João Leitão, and João Costa Seco. Regent: Uma Arquitectura para a Evolução de Micro-Serviços. In INForum 2019, September 2019. [ bib | .pdf ]
[18] Mário Pereira. Desfuncionalizar para Provar. In INForum 2019, September 2019. [ bib | .pdf ]
[17] Luís Pedro Arrojado Horta, Mário Pereira, and Simão Melo de Sousa. Semântica Operacional Executável para Michelson em Why3. In INForum 2019, September 2019. [ bib | .pdf ]
[16] Filipe Meirim, Mário Pereira, and Carla Ferreira. CISE3: Verificação de aplicações com consistência fraca em Why3. In INForum 2019, September 2019. [ bib | .pdf ]
[15] Pedro Barroso, Mário Pereira, and António Ravara. Lógica Animada: conversão funcional correta para forma normal conjuntiva. In INForum 2019, September 2019. [ bib | .pdf ]
[14] Tiago Roxo, Mário Pereira, and Simão Melo de Sousa. Programação funcional com estilo e sem custo: Transformação CPS à la carte. In INForum 2019, September 2019. [ bib | .pdf ]
[13] Mário José Parreira Pereira. Tools and Techniques for the Verification of Modular Stateful Code. Theses, Université Paris Saclay (COmUE), December 2018. [ bib | http ]
Keywords: Modularity ; OCaml ; OCaml library ; Efects ; Why3 ; Deductive verification ; Modulaire ; OCaml ; Vérification déductive ; Why3 ; Effets ; Bibliothèque OCaml
[12] Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, Mário Pereira, and Simão Melo de Sousa. A toolchain to Produce Correct-by-Construction OCaml Programs. Technical report, 2018. artifact: https://www.lri.fr/~mpereira/correct_ocaml.ova. [ bib ]
[11] Jean-Christophe Filliâtre, Mário Pereira, and Simão Melo de Sousa. Vérification de programmes fortement impératifs avec Why3. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib ]
[10] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. Journal of Automated Reasoning, 60(3):365--383, 2018. [ bib | DOI ]
[9] Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and François Pottier. VOCAL -- A Verified OCaml Library. ML Family Workshop, September 2017. [ bib ]
[8] Mário Pereira. Défonctionnaliser pour prouver. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ]
[7] Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib ]
[6] Jean-Christophe Filliâtre and Mário Pereira. Producing all ideals of a forest, formally (verification pearl). In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib ]
[5] Jean-Christophe Filliâtre and Mário Pereira. A modular way to reason about iteration. In Sanjai Rayadurgam and Oksana Tkachuk, editors, 8th NASA Formal Methods Symposium, volume 9690 of Lecture Notes in Computer Science, Minneapolis, MN, USA, June 2016. Springer. [ bib ]
In this paper we present an approach to specify programs performing iterations. The idea is to specify iteration in terms of the nite sequence of the elements enumerated so far, and only those. In particular, we are able to deal with non-deterministic and possibly innite iteration. We show how to cope with the issue of an iteration no longer being consistent with mutable data. We validate our proposal using the deductive verication tool Why3 and two iteration paradigms, namely cursors and higher-order iterators. For each paradigm, we verify several implementations of iterators and client code. This is done in a modular way, i.e., the client code only relies on the specication of the iteration.
[4] Jean-Christophe Filliâtre and Mário Pereira. Itérer avec confiance. In Vingt-septièmes Journées Francophones des Langages Applicatifs, Saint-Malo, France, January 2016. [ bib ]
[3] Mário Pereira, Sandra Alves, and Mário Florido. Liquid intersection types. Electronic Proceedings in Theoretical Computer Science, 177:24--42, mar 2015. [ bib | DOI | http ]
[2] Mário Pereira and Simão Melo de Sousa. Complexity checking of arm programs, by deduction. In Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC '14, pages 1309--1314, New York, NY, USA, 2014. ACM. [ bib | DOI | http ]
Keywords: ARM, complexity checking, deductive software verification, hoare logic, unstructured control flow graph, why3
[1] Mário Pereira, Jean-Christophe Filliâtre, and Simão Melo de Sousa. ARMY: a deductive verification platform for ARM programs using Why3. In INForum 2012, September 2012. [ bib | .pdf ]
Unstructured (low-level) programs tend to be challenging to prove correct, since the control flow is arbitrary complex and there are no obvious points in the code where to insert logical assertions. In this paper, we present a system to formally verify ARM programs, based on a flow sequentialization methodology and a formalized ARM semantics. This system, built upon the why3 verification platform, takes an annotated ARM program, turns it into a set of purely sequential flow programs, translates these programs' instructions into the corresponding formalized opcodes and finally calls the Why3 VCGen to generate the verification conditions that can then be discharged by provers. A prototype has been implemented and used to verify several programming examples.
Keywords: Why3

This file was generated by bibtex2html 1.99.