{"id":558255,"date":"2019-01-03T13:11:54","date_gmt":"2019-01-03T21:11:54","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-event&p=558255"},"modified":"2020-04-20T07:55:01","modified_gmt":"2020-04-20T14:55:01","slug":"popl-2019","status":"publish","type":"msr-event","link":"https:\/\/www.microsoft.com\/en-us\/research\/event\/popl-2019\/","title":{"rendered":"Microsoft @ POPL 2019"},"content":{"rendered":"

Venue: <\/strong>Hotel Cascais Miragem (opens in new tab)<\/span><\/a>
\nAv.Marginal n.8554
\n2754-536
\nCascais\/Lisbon
\nPortugal<\/p>\n

Website:<\/strong> POPL 2019 (opens in new tab)<\/span><\/a><\/p>\n","protected":false},"excerpt":{"rendered":"

Microsoft is excited to be a Platinum sponsor of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages. Stop by our booth to learn about our latest research and find out about career opportunities with Microsoft.<\/p>\n","protected":false},"featured_media":558522,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_startdate":"2019-01-13","msr_enddate":"2019-01-19","msr_location":"Cascais\/Lisbon, Portugal","msr_expirationdate":"","msr_event_recording_link":"","msr_event_link":"https:\/\/popl19.sigplan.org\/attending\/Registration","msr_event_link_redirect":false,"msr_event_time":"","msr_hide_region":false,"msr_private_event":false,"footnotes":""},"research-area":[13560],"msr-region":[239178],"msr-event-type":[197941],"msr-video-type":[],"msr-locale":[268875],"msr-program-audience":[],"msr-post-option":[],"msr-impact-theme":[],"class_list":["post-558255","msr-event","type-msr-event","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-region-europe","msr-event-type-conferences","msr-locale-en_us"],"msr_about":"Venue: <\/strong>Hotel Cascais Miragem<\/a>\r\nAv.Marginal n.8554\r\n2754-536\r\nCascais\/Lisbon\r\nPortugal\r\n\r\nWebsite:<\/strong> POPL 2019<\/a>","tab-content":[{"id":0,"name":"About","content":"Microsoft is excited to be a Platinum sponsor of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages<\/a>. Stop by our booth to learn about our latest research and find out about career opportunities with Microsoft.\r\n

Microsoft Attendees<\/h3>\r\n

Tom Ball<\/a>\r\nAntoine Delignat-Lavaud<\/a>\r\nChris Hawblitzel<\/a>\r\nNuno Lopes<\/a>\r\nJonathan Protzenko<\/a>\r\nTahina Ramananandro<\/a>\r\nAndrey Rybalchenko<\/a>\r\nSantiago Zanella-Beguelin<\/a>\r\nAndy Gordon<\/a>\r\nNikhil Swamy<\/a><\/p>\r\n\r\n

Research Paper Committee<\/h3>\r\n

Dimitrios Vytiniotis<\/a>, Matthew Parkinson<\/a>, Nikhil Swamy<\/a><\/p>\r\n\r\n

Artifact Evaluation Committee<\/h3>\r\n

Jonathan Protzenko<\/a><\/p>\r\n\r\n

Steering Committee<\/h3>\r\n

Andrew D. Gordon<\/a><\/p>\r\n\r\n

Co-Located Conferences<\/h3>\r\n

Certified Programs and Proofs (CPP)<\/h4>\r\n

Chris Hawblitzel<\/a><\/p>\r\n\r\n

Principles of Secure Compilation(PriSC)<\/h4>\r\n

C\u00e9dric Fournet<\/a><\/p>\r\n\r\n

Invited Speakers<\/h3>\r\n

VMCAI 2019, co-located\r\nTuesday, January 15, 2019 | 9:00 AM\u201310:30 AM\r\nSemantics for Compiler IRs: Undefined Behavior is not Evil!<\/strong><\/a>\r\nNuno Lopes<\/a><\/p>"},{"id":1,"name":"Accepted Papers","content":"

Wednesday, January 16, 2019 | 1:45 PM\u20132:07 PM | Probabilistic Programming and Semantics\r\nProbabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic<\/a><\/h4>\r\n

Maria I. Gorinova<\/a>, Andrew D. Gordon<\/a>, Charles Sutton<\/a><\/p>\r\n\r\n

Friday, January 18, 2019 | 5:21 PM\u20135:43 PM | Verified Compilation and Concurrency\r\nA Verified, Efficient Embedding of a Verifiable Assembly Language<\/a><\/h4>\r\n

Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel<\/a>, Bryan Parno, Aseem Rastogi<\/a>, Nikhil Swamy<\/a><\/p>\r\n\r\n

Co-Located Conferences<\/h3>\r\n

Tuesday, January 15, 2019 | 4:30 PM\u20135:00 PM | Networks and Concurrency at VMCAI\r\nFast BGP Simulation of Large Datacenters<\/a><\/h4>\r\n

Nuno Lopes<\/a>, Andrey Rybalchenko<\/a><\/p>"},{"id":2,"name":"Open Source Tools","content":"

Open Source Tools for System Correctness<\/h4>\r\nAutomata:<\/strong> Automata<\/a> is a .NET library that provides algorithms for composing and analyzing regular expressions, automata, and transducers. In addition to classical word automata, it also includes algorithms for analysis of tree automata and tree transducers. The library covers algorithms over finite alphabets as well as their symbolic counterparts. Predicates can be supported by an SMT solver as a plugin.\r\n\r\nCorral Program Verifier:<\/strong>\u00a0Corral<\/a> is a whole-program analysis tool for\u00a0Boogie<\/a>\u00a0programs. Corral uses goal-directed symbolic search techniques to find assertion violations.\u00a0It leverages the automated\u00a0theorem prover Z3. Corral, by default, does a bounded search up to a recursion depth and fixed number of context switches. Corral also supports the\u00a0Duality<\/a>\u00a0extension for constructing\u00a0inductive proofs of correctness of programs.\r\n\r\nIvy:<\/strong> IVy<\/a> is a tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.\r\n\r\nLean Theorem Prover:<\/strong> Lean<\/a> is an open source theorem prover and programming language. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.\r\n\r\nP\/P#:<\/strong> P\/P#<\/a> are languages for asynchronous event-driven programming that allow the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P\/P# unifies modeling and programming into one activity for the programmer. Not only can a P\/P# program be compiled into executable code, but it can also be validated using systematic testing.\r\n\r\nProject Everest:<\/strong> Everest<\/a> is the combination of the following projects, that together are used to prove correct\/secure and generate a C library that efficiently implements TLS 1.3\r\n