Meta tags:

Headings (most frequently used words):

postdoc, at, institute, lionel, blatter, about, me, publications, talk, books, research, teaching, supervision, contact, max, planck, karlsruhe, of, technology, phd, thesis,

Text of the page (most frequently used words):
the (50), and (35), for (26), verification (23), relational (17), pdf (16), #lionel (16), blatter (16), with (12), 2018 (12), properties (11), france (11), jasmin (10), security (10), programs (10), research (9), programming (9), university (9), paris (9), 2019 (9), frama (8), compiler (8), gilles (8), barthe (8), time (8), saclay (8), orsay (8), virgile (8), doi (8), formal (7), phd (7), prevosto (7), nikolai (7), kosmatov (7), supervised (6), floating (6), point (6), 2022 (6), generation (6), speculative (6), 2025 (6), constant (6), introduction (6), following (6), software (6), pascale (6), gall (6), 2024 (5), sct (5), santiago (5), arranz (5), olmos (5), correctness (5), points (5), that (5), specification (5), analysis (5), using (5), proofs (5), institute (5), mpi (4), germany (4), thesis (4), preconditions (4), internship (4), automatic (4), certified (4), preservation (4), functional (4), logic (4), can (4), focused (4), work (4), hoare (4), proof (4), easycrypt (4), proving (4), was (4), bochum (3), 2021 (3), distributed (3), support (3), 2016 (3), 2017 (3), information (3), rpp (3), based (3), language (3), session (3), tool (3), soundness (3), are (3), which (3), scientific (3), languages (3), group (3), karlsruhe (3), high (3), cryptographic (3), max (3), planck (3), privacy (3), self (3), benjamin (3), between (3), september (3), dot (2), jonas (2), krämer (2), inferring (2), interval (2), valued (2), 2020 (2), annotations (2), supervising (2), xingyu (2), verifying (2), policy (2), transformation (2), ongoing (2), supervision (2), object (2), deductive (2), lecture (2), computer (2), imperative (2), total (2), link (2), two (2), into (2), called (2), contract (2), acsl (2), keywords (2), multi (2), party (2), types (2), computations (2), taint (2), scripts (2), leakage (2), user (2), assistant (2), condition (2), function (2), errors (2), arithmetic (2), combines (2), level (2), passing (2), this (2), methods (2), application (2), oriented (2), resumed (2), items (2), postdoc (2), technology (2), compilation (2), probabilistic (2), constante (2), cryptography (2), rocq (2), code (2), composable (2), cryptoline (2), tactic (2), jazzline (2), attacks (2), speculation (2), hardware (2), decompiling (2), spectre (2), chapter (2), foundation (2), composition (2), tacas (2), grégoire (2), vincent (2), laporte (2), zhiyuan (2), zhang (2), accepted (2), oopsla (2), 2026 (2), about (2), post (2), doctoral (2), researcher (2), led (2), last, updated, february, font, theme, mimoza, luciole, orcid, address, universitaetsstr, 140, 44799, email, firstname, lastname, org, contact, master, tobias, hombücher, system, mpiv, bachelor, maximilian, von, gaisberg, verificationn, sorting, algorithms, parmida, javadian, selective, load, hardening, protections, jieyu, zheng, adding, avx512, instruction, prema, narayan, ochoa, part, program, upec, créteil, ensiie, evry, constraint, prolog, isty, univ, versailles, sqy, vélizy, git, graphics, advanced, communication, systems, ruhr, teaching, implementation, previous, plugin, design, approaches, integrated, standard, extention, during, worked, platform, context, summarised, developpement, shell, checks, specified, definition, tain, coq, contracts, recursive, calls, pointers, formalization, synthesis, functions, generated, guarantee, provided, accuracy, requirements, satisfied, avoiding, unreliable, numerical, due, aggregated, roundoff, caused, developed, conditions, absence, deadlocks, fidelity, any, number, participant, usually, written, low, like, uses, message, libraries, parallelisation, relies, real, abstraction, implies, susceptible, interesting, semantics, none, interference, recently, started, library, includes, mecanization, different, logics, associate, completness, xhl, writing, assurance, speed, aided, primarily, currently, working, safty, their, formalizing, interaction, trees, tooling, inspired, extend, resulting, ensatz, nsatz, flow, ensures, protected, against, timing, side, channel, consider, exploide, programme, formosa, crypto, robles, guide, wip, volume, foundations, books, preuve, automatique, propriétés, relationnelles, par, afadl, talk, static, dynamic, composed, tap, eva, darulova, mattias, ulbrich, ifm, efficient, vcgen, modular, isola, popl, josé, bacelar, almeida, manuel, barbosa, gustavo, delerue, joão, diogo, duarte, gregoire, tiago, oliveira, miguel, quaresma, pierre, yves, strub, ming, hsien, tsai, bow, yaw, wang, yin, yang, distinguished, paper, award, ccs, youcef, bouzid, sören, van, der, wall, dis, style, xie, preserves, paolo, torrini, submitted, publications, interests, include, safety, octobre, 2015, august, student, under, cea, list, nano, innov, centralesupelec, misc, team, ater, université, sud, january, july, kit, prof, bernard, beckert, since,

Text of the page (random words):
lionel blatter lionel blatter about me since september 2022 i am a post doctoral researcher at the max planck institute for security and privacy bochum germany in the group foundation of security and privacy led by gilles barthe between january 2020 and july 2022 i was a post doctoral researcher at karlsruhe institute of technology kit karlsruhe germany in the application oriented formal verification group led by prof dr bernard beckert between september 2018 and september 2019 i was ater at université paris sud orsay between octobre 2015 and august 2018 i was a phd student at university paris saclay france under the supervision of pascale le gall nikolai kosmatov and virgile prevosto at cea list nano innov and centralesupelec in the misc team my phd was about relational properties for specification and verification of c programs in frama c my research interests include formal methods programming languages safety and security of software and hardware publications submitted 2025 the jasmin compiler preserves cryptographic security santiago arranz olmos gilles barthe lionel blatter benjamin grégoire vincent laporte paolo torrini pdf accepted at oopsla 2026 dis proving spectre security with speculation passing style santiago arranz olmos gilles barthe lionel blatter xingyu xie zhiyuan zhang pdf accepted at oopsla 2026 decompiling for constant time analysis santiago arranz olmos gilles barthe lionel blatter youcef bouzid sören van der wall zhiyuan zhang pdf ccs 2025 jazzline composable cryptoline functional correctness proofs for jasmin programs josé bacelar almeida manuel barbosa gilles barthe lionel blatter gustavo delerue joão diogo duarte benjamin gregoire tiago oliveira miguel quaresma pierre yves strub ming hsien tsai bow yaw wang bo yin yang distinguished paper award doi pdf popl 2025 preservation of speculative constant time by compilation santiago arranz olmos gilles barthe lionel blatter benjamin grégoire vincent laporte doi pdf isola 2022 an efficient vcgen based modular verification of relational properties lionel blatter nikolai kosmatov pascale le gall virgile prevosto doi pdf ifm 2022 certified verification of relational properties lionel blatter nikolai kosmatov pascale le gall virgile prevosto doi pdf tacas 2022 inferring interval valued floating point preconditions jonas krämer lionel blatter eva darulova mattias ulbrich doi phd thesis 2019 relational properties for specification and verification of c programs in frama c lionel blatter pdf tap 2018 static and dynamic verification of relational properties on self composed c code lionel blatter nikolai kosmatov pascale le gall virgile prevosto doi pdf tacas 2017 rpp automatic proof of relational properties by self composition lionel blatter nikolai kosmatov pascale le gall virgile prevosto doi pdf talk afadl 2018 rpp preuve automatique de propriétés relationnelles par self composition lionel blatter nikolai kosmatov pascale le gall virgile prevosto pdf books wip total correctness lionel blatter chapter in volume 2 programming languages foundations of software foundation link specification and verification of high level properties lionel blatter nikolai kosmatov virgile prevosto virgile robles chapter in guide to software verification with frama c 2024 doi research postdoc at max planck institute my research at the max planck institute for security and privacy and formosa crypto can be resumed by the following items speculative constant time constant time ct and speculative constant time sct are information flow policy that ensures that programs are protected against timing side channel attacks sct consider spectre attacks which exploide speculation of hardware my research focused on the following points proving compiler preservation of sct pdf proving sct using programme transformation pdf decompiling for ct analysis pdf jasmin and easycrypt jasmin is a certified compiler for writing high assurance and high speed cryptography code and easycrypt is a proof assistant for computer aided cryptographic proofs my research focused primarily on the following points the jazzline tooling for composable functional correctness proofs for jasmin programs the work combines the jasmin compiler with easycrypt and cryptoline pdf this work inspired me to extend the nsatz tactic in rocq resulting in the ensatz tactic formalizing cryptographic security with interaction trees and proving compiler preservation with relational hoare logic pdf currently i m working on the generation of annotations for safty in jasmin and their verification in easycrypt recently i started to work on the rocq library xhl which includes the mecanization of different probabilistic relational hoare logics and associate soundness and completness proofs keywords certified compilation semantics of probabilistic programs relational hoare logic none interference constante time and speculative constante time cryptography postdoc at karlsruhe institute of technology my research at the application oriented formal verification group can be resumed by the following items formal verification of scientific software usually scientific software is written in low level languages like c uses message passing libraries for parallelisation and relies on floating point arithmetic for real abstraction this implies that scientific software is susceptible to programming errors and interesting for formal methods my research focused on the following two points the developed of a tool called mpi v which combines multi party session types and verification conditions generation for verifying the absence of deadlocks session fidelity and functional correctness of distributed c programs using mpi for any number of participant an automatic synthesis of preconditions for floating point functions the generated preconditions guarantee that user provided accuracy requirements are satisfied i e avoiding unreliable numerical computations due to aggregated roundoff errors caused by floating point arithmetic 3 soundness proof of relational verification using verification condition generation a formalization and soundness proofs in the coq proof assistant of relational verification using verification condition generation and relational function contracts for programs with recursive function calls and pointers 1 2 tain analysis for sh scripts the developpement of a tool for taint analysis of shell scripts the tool checks for information leakage using a user specified definition of leakage keywords deductive verification distributed programs multi party session types relational hoare logic floating point computations taint analysis phd thesis during my phd i worked on the formal verification of relational properties my research focused on the support of relational properties in the frama c platform i e in the context of the c language and the specification language acsl the work can be summarised by the following points extention for the acsl specification language to support relational properties design of relational contract based verification approaches that can be integrated into standard contract based verification of programs implementation of the two previous points into a frama c plugin called rpp 4 5 teaching 2025 lecture on total correctness ruhr university bochum germany link 2018 2019 introduction to logic university paris saclay orsay france 2018 2019 security of information and communication systems university paris saclay orsay france 2018 2019 introduction to object programming university paris saclay orsay france 2018 2019 introduction to imperative programming university paris saclay orsay france 2018 2019 advanced imperative programming university paris saclay orsay france 2018 2019 introduction to functional programming university paris saclay orsay france 2018 2019 introduction to computer graphics university paris saclay orsay france 2016 2018 lecture on constraint programming in prolog isty univ versailles sqy vélizy france git 2016 2017 deductive verification with frama c ensiie in evry france 2016 2017 introduction to object programming upec in créteil france supervision 2024 ongoing co supervising with gilles barthe the phd of santiago arranz olmos on the verification and preservation of security properties 2024 ongoing co supervising with gilles barthe the phd of xingyu xi on the part on verifying speculative constant time sct security policy with program transformation 2025 co supervised the internship of prema narayan ochoa on automatic generation of certified annotations for the jasmin compiler 2025 co supervised the internship of jieyu zheng on adding support for avx512 instruction to the jasmin compiler 2024 co supervised the internship of parmida javadian on automatic generation of selective speculative load hardening protections for the jasmin compiler 2021 2022 supervised the bachelor thesis of maximilian von gaisberg formal verificationn of sorting algorithms with frama c 2021 supervised the research internship of tobias hombücher verification of distributed system with frama c mpiv 2020 2021 co supervised the master thesis of jonas krämer inferring interval valued floating point preconditions contact email firstname dot lastname at mpi sp dot org address mpi sp universitaetsstr 140 44799 bochum germany orcid last updated on 18 february 2024 font luciole theme mimoza