Michaël Périn's home page

  • Enseignement

  • Research activities

    • Efficient algorithms on Polyhedra
      Efficient Elimination of Redundancies in Polyhedra using Raytracing
      with A.Maréchal, VMCAI'2017. [ pdf | bib ]
    • Decision procedure
      Polyhedral Approximation of Multivariate Polynomials using Handelman's Theorem with A.Maréchal, A.Fouilhé, T.King and D.Monniaux, VMCAI'2016. [ 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