BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:DAYLIGHT DTSTART:20180311T020000 RDATE:20180311T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20180712T171742Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20180713T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20180713T110000 DTSTAMP;VALUE=DATE-TIME:20180712T171742Z LAST-MODIFIED;VALUE=DATE-TIME:20180712T171742Z UID:http://calagator.org/events/1250473994 DESCRIPTION:Abstract: \;\nIn this talk\, I’ll give a high-level overvi ew of Penn’s Vellvm (Verified LLVM) project\, which aims to build formal semantics in Coq for the LLVM IR. I’ll sketch some of our past results\ , in which we verified memory safety transformations and a variant of LL VM’s mem2reg optimization\, focusing on the structure of the proof techn iques. Along the way\, I’ll highlight some of the challenges of reasoni ng about LLVM code (many of which are still open issues). I’ll wrap up w ith a status report about our ongoing efforts to re-engineer Vellvm as p art of the DeepSpec NSF Expeditions project. \;\n \;\nNo experienc e with LLVM or Coq will be assumed. \;\n \;\nBio: \;\nI study p rogramming languages and computer security. I have wide-ranging interest s\, and some of my most recent work touches on: Coq verification of LLVM program transformations and randomized algorithms\, type-directed progr am synthesis\, linear types and GUI programming. I have also spent a lot of time thinking about language-based enforcement of information-flow p olicies\, low-level code memory safety\, understanding dynamic security policies\, and authorization logic. I am also interested in secure concu rrent and distributed computing\, functional programming languages\, typ e theory\, linear and modal logics\, theorem proving and mechanized meta theory.\n\nTags: llvm\, coq\, verification\, computer science\, security \, formal semantics\n\nImported from: http://calagator.org/events/125047 3994 URL:https://galois.com/blog/2018/07/vellvm-verifying-the-llvm/ SUMMARY:Galois Tech Talk: Vellvm -- Verifying the LLVM LOCATION:Galois Inc: 421 Sw 6th Ave Ste 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR