CPP 2015
Martin Bodin, Thomas Jensen, and Alan Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Certified Programs and Proofs (CPP), 2015.
Link
Hide
Show
Hide All
Show All
Ligilo
Malafiŝi
Afiŝi
Malafiŝi ĉion
Afiŝi ĉion
Lien
Cacher
Montrer
Cacher tout
Montrer tout
I am a PhD student at INRIA Rennes under the supervision of Alan Schmitt and Thomas Jensen. I work on formal analysis of JavaScript.
Mi estas doktoriĝanto ĉe INRIA Rennes superrigardate de Alan Schmitt kaj Thomas Jensen. Mi laboras pri formalaj analizoj de Javaskripto.
Je suis doctorant à l’INRIA de Rennes sous la supervision d’Alan Schmitt et de Thomas Jensen. Je travaille sur des analyses formelles de JavaScript.
I am part of the JSCert and the SecCloud projects. The the JSCert project aims to build models of JavaScript in the Coq proof assistant and to design automated tools based on those semantics. The the SecCloud project aims to provide a comprehensive language-based approach to the definition, analysis and implementation of secure applications developed using JavaScript and similar languages.
Mi estas parton de la projektoj JSCert kaj SecCloud. La projekto JSCert celas al konstrui modelojn de Javaskripto en la pruvhelpilo Coq kaj konstrui aŭtomatajn ilojn purvatajn per tiuj semantikoj. La projekto SecCloud celas ellabori lingvaĵbazajn laborgvidojn por la difino, analizo kaj realigo de sekuraj programaĵoj ellaboritaj per Javaskripto aŭ similaj lingvaĵoj.
Je fais partie des projets JSCert et SecCloud. Le projet JSCert a pour but de construire des modèles de JavaScript en Coq et de concevoir des outils d’analyses automatiques basés sur ces modèles formels. Le projet SecCloud a pour but de concevoir une approche orientée langages de programation pour la définition, l’analyse et l’implémentation d’applications sécurisées développées en JavaScript ou en des langages similaires.
Publications
Eldonaĵoj
Publications
CPP 2015
Martin Bodin, Thomas Jensen kaj Alan Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Certified Programs and Proofs (CPP), 2015.
CPP 2015
Martin Bodin, Thomas Jensen et Alan Schmitt, Certified Abstract Interpretation with Pretty-Big-Step Semantics, Certified Programs and Proofs (CPP), 2015.
POPL 2014
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiūnienė, Alan Schmitt, and Gareth Smith, A Trusted Mechanised JavaScript Specification, Symposium on Principles of Programming Languages (POPL), 2014.
POPL 2014
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiūnienė, Alan Schmitt kaj Gareth Smith, A Trusted Mechanised JavaScript Specification, Symposium on Principles of Programming Languages (POPL), 2014.
POPL 2014
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudžiūnienė, Alan Schmitt et Gareth Smith, A Trusted Mechanised JavaScript Specification, Symposium on Principles of Programming Languages (POPL), 2014.
ITP 2013
Jörg Endrullis, Dimitri Hendriks, and Martin Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, Interactive Theorem Proving (ITP), 2013.
ITP 2013
Jörg Endrullis, Dimitri Hendriks kaj Martin Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, Interactive Theorem Proving (ITP), 2013.
ITP 2013
Jörg Endrullis, Dimitri Hendriks et Martin Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, Interactive Theorem Proving (ITP), 2013.
APLAS 2011
David Monniaux and Martin Bodin, Modular Abstractions of Reactive Nodes using Disjunctive Invariants, Programming Languages and Systems (APLAS), 2011.
APLAS 2011
David Monniaux kaj Martin Bodin, Modular Abstractions of Reactive Nodes using Disjunctive Invariants, Programming Languages and Systems (APLAS), 2011.
APLAS 2011
David Monniaux et Martin Bodin, Modular Abstractions of Reactive Nodes using Disjunctive Invariants, Programming Languages and Systems (APLAS), 2011.
Workshops
Babilkongresoj
Ateliers
JFLA 2016
Martin Bodin, Thomas Jensen, and Alan Schmitt, An Abstract Separation Logic for Interlinked Extensible Records, Journées Francophones des Langages Applicatifs (JFLA), 2016.
JFLA 2016
Martin Bodin, Thomas Jensen kaj Alan Schmitt, An Abstract Separation Logic for Interlinked Extensible Records, Journées Francophones des Langages Applicatifs (JFLA), 2016.
JFLA 2016
Martin Bodin, Thomas Jensen et Alan Schmitt, An Abstract Separation Logic for Interlinked Extensible Records, Journées Francophones des Langages Applicatifs (JFLA), 2016.
JFLA 2014
Martin Bodin, Thomas Jensen, and Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation, Journées Francophones des Langages Applicatifs (JFLA), 2014.
JFLA 2014
Martin Bodin, Thomas Jensen kaj Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation, Journées Francophones des Langages Applicatifs (JFLA), 2014.
JFLA 2014
Martin Bodin, Thomas Jensen et Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation, Journées Francophones des Langages Applicatifs (JFLA), 2014.
Festschrift of David Schmidt
Martin Bodin, Thomas Jensen, and Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version), Festschrift of David Schmidt, 2013.
Festverkaĵaro al David Schmidt
Martin Bodin, Thomas Jensen kaj Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version), Festschrift of David Schmidt, 2013.
Festschrift pour David Schmidt
Martin Bodin, Thomas Jensen et Alan Schmitt, Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version), Festschrift of David Schmidt, 2013.
JFLA 2013
Martin Bodin and Alan Schmitt, A Certified JavaScript Interpreter, Journées Francophones des Langages Applicatifs (JFLA), 2013.
JFLA 2013
Martin Bodin kaj Alan Schmitt, A Certified JavaScript Interpreter, Journées Francophones des Langages Applicatifs (JFLA), 2013.
JFLA 2013
Martin Bodin et Alan Schmitt, A Certified JavaScript Interpreter, Journées Francophones des Langages Applicatifs (JFLA), 2013.
Thesis
Doktoriĝo
Thèse
Certified Semantics and Analysis of JavaScript
I defended my PhD Thesis in 2016. My PhD advisors were Alan Schmitt and Thomas Jensen.
Certigitaj semantiko kaj analizo de JavaSkripto
Mi doktoriĝis en 2016. Miaj doktoriĝestroj estis Alan Schmitt kaj Thomas Jensen.
Sémantique et analyse certifiées de JavaScript
J’ai soutenu en 2016. Mes encadrants étaient Alan Schmitt et Thomas Jensen.