Michaël Périn's home page

  • Enseignement

  • Research activities

    • Vulgarisation
      L'IA générative expliquée à des non-informaticiens Séminaire ESPG (jun 24), INPI (oct 23, avr 24), Polytech (jun 23,24). [pdf]
    • Pédagogie
      Qui sont ces nouveaux Z'élèves de la génération Z ? Séminaire Polytech Grenoble, Juillet 2022. [ pdf, vidéo ]
    • Decision procedure
      Automatic Grading (take a CEGAR and let the machine do your job), Verimag seminar, May 2018. [ pdf ]
      Polyhedral Approximation of Multivariate Polynomials using Handelman's Theorem with A.Maréchal, A.Fouilhé, T.King and D.Monniaux, VMCAI'2016. [ pdf | bib ]
    • Efficient algorithms on Polyhedra
      The development of a Verified Polyhedra Library made of untrusted parts mixing Ocaml, C++, threads, ... and just a little bit of Coq for certification,
      invited talk at TAPAS'2017 and Coq en Stock'2017
      Scalable Minimizing-Operators on Polyhedra via Parametric Linear Programming
      with A.Maréchal and D.Monniaux, SAS'2017. [ pdf | bib ]
      Efficient Elimination of Redundancies in Polyhedra using Raytracing
      with A.Maréchal, VMCAI'2017. [ pdf | bib ]
    • Certification using Coq
      A Linearization Technique for Multivariate Polynomials using Polyhedra based on Handelman-Krivine's Theorem with A.Maréchal, JFLA'2015. [ pdf | bib ]
      Efficient generation of correctness certificates for the abstract domain of polyhedra,
      with Alexis Fouilhé and David Monniaux, SAS'2013. [ pdf | bib ]
    • Invariant generation
      Robustness of Invariants in BIP models with J-O.Blech, T-H.Nguyen. In WING'09 [ slides | pdf | bib ]
    • Certification of verification tools by automatic proof generation
      Automatic Coq Proofs Generation from Static Analyzers by Lightweight Instrumentation with M.Garnacho and the help of Mathias Péron (the developper of the Enkidu static analyzer). Unpublished, Verimag Technical Report 2011-18 [ pdf | bib]
      Certifying Deadlock-freedom for BIP Models with J-O.Blech. In SCOPES'09 [ pdf | bib]
      Convincing proofs for program certification with M.Garnacho. In SafeCert'08 [ slides | pdf | bib]
    • Certification of security applications for smart card (Eden2 project)
      Certification of Smart-Card Applications in Common Criteria: Proving Representation Correspondences with I.Narasamdya. In FASE'09 [ pdf | bib]
      Certification of Smart-Card Applications in Common Criteria with I.Narasamdya.
      In SAC/SVT'09 [ pdf | bib]

    • Verification of cryptographic protocols
      Certification of Cryptographic Protocols by Abstract Model-Checking and Proof Concretization with R.Janvier and Y.Lakhnech. In ITCES'06 [ slides | pdf | bib]
      Pattern-based abstraction for verifying secrecy in protocols with L. Bozga, Y. Lakhnech. In STTT:8:57-76 , Feb 2006 [pdf | bib]

  • Position at Université Grenoble Alpes

    • MCF (Assistant professor) since 2001 at Polytech'Grenoble
    • Member of the research team « Proof and Code Analysis for Safety and Security » at Verimag Lab.
    email: evaluate the expresssion   swap( perin . micKael[K/h] ) @ reverse(gami) . fr

    phone: (+33|0) 45 74 222 37

  • Developing tools in Ocaml

    • here are my personal librairies for students (not the most efficient ones but clean and simple code for beginners)
    • The significant developments are available on gitHub

  • Other activities: en montagne, sur tatami pour pratiquer l'aïkido renwakaï, dans la blogosphère ou carrément en train de buller