News 2019

Programming Languages & Verification

MPI-SWS student receives best presentation award at the iFM'19 PhD Symposium

December 2019
Other Awards and Prizes
Debasmita Lohar, a doctoral student at MPI-SWS, has received an award for the best presentation at the iFM 2019 PhD Symposium. The award was given for her talk on "Sound Probabilistic Numerical Error Analysis.”

Max Planck researchers publish 8 papers at POPL 2020 + a new record!

November 2019
Homepage News, New publications
Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the new Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 8 papers accepted to POPL 2020 (over 10% of all accepted papers).  This is the third year in a row that MPI-SWS researchers have published 5 papers in POPL.  Furthermore, MPI-SWS faculty member Derek Dreyer is the first person ever to publish 4 papers in a single POPL.  ...
Researchers from the Max Planck Institute for Software Systems (MPI-SWS) and the new Max Planck Institute for Security and Privacy (MPI-SP) have authored a total of 8 papers accepted to POPL 2020 (over 10% of all accepted papers).  This is the third year in a row that MPI-SWS researchers have published 5 papers in POPL.  Furthermore, MPI-SWS faculty member Derek Dreyer is the first person ever to publish 4 papers in a single POPL.  Congratulations to all our POPL authors!

MPI-SWS papers:

  • The Future is Ours: Prophecy Variables in Separation Logic. Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs. [pdf]

  • The High-Level Benefits of Low-Level Sandboxing. Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak. [pdf]

  • Persistency Semantics of the Intel-x86 Architecture. Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis. [pdf]

  • RustBelt Meets Relaxed Memory. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer. [pdf]

  • Stacked Borrows: An Aliasing Model for Rust. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer. [pdf]


MPI-SP papers:

  • Formal Verification of a Constant-Time Preserving C Compiler. Gilles Barthe, Sandrine Blazy, Benjamin Gregoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu. [pdf]

  • A Probabilistic Separation Logic. Gilles Barthe, Justin Hsu, Kevin Liao. [pdf]

  • Relational Proofs for Quantum Programs. Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou. [pdf]

Read more

Former MPI-SWS postdoc receives ERC starting grant

September 2019
Alumni News, ERC Awards
Ori Lahav was awarded an ERC starting grant on "Verification-Aware Programming Language Concurrency Semantics".  Ori was formerly a postdoctoral fellow in the Software Analysis and Verification group, and is now a tenure-track faculty member at Tel Aviv University. Read more about this year's ERC Starting Grants here.

Advanced Automata Theory Course at TU Kaiserslautern

May 2019
Courses
Damien Zufferey and Daniel Neider are co-teaching Advanced Automata Theory at the University of Kaiserslautern in the Summer 2019 semester.

Azalea Raad selected to attend Heidelberg Laureate Forum

April 2019
Other Awards and Prizes
MPI-SWS postdoctoral fellow Azalea Raad has been selected to attend the 7th annual Heidelberg Laureate Forum in September 2019. An international committee of experts selected Azalea for one of only 200 spots reserved for young researchers from around the world.

The Heidelberg Laureate Forum gives young computer science and math researchers the opportunity to interact with some of the world's top scientists. The speakers for the 2019 Forum, for example, include 17 different Turing Award winners, ...
MPI-SWS postdoctoral fellow Azalea Raad has been selected to attend the 7th annual Heidelberg Laureate Forum in September 2019. An international committee of experts selected Azalea for one of only 200 spots reserved for young researchers from around the world.

The Heidelberg Laureate Forum gives young computer science and math researchers the opportunity to interact with some of the world's top scientists. The speakers for the 2019 Forum, for example, include 17 different Turing Award winners, as well as numerous winners of the Fields Medal, the Abel Prize, and the ACM Prize in Computing.
Read more

Derek Dreyer general chair of ICFP'19

February 2019
Leadership roles
Derek Dreyer has been selected as general chair of the 24th ACM SIGPLAN International Conference on Functional Programming, to be held August 19-21, 2019 in Berlin. ICFP is an international conference providing a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming.

MPI-SWS researchers have a distinguished paper at POPL 2019

January 2019
Best Paper Award
Vineet Rajani and Deepak Garg, along with their co-authors Marco Vassena, Alejandro Russo and Deian Stefan, have won a Distinguished Paper Award at the 2019 ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) for their paper titled "From fine- to coarse-grained dynamic information flow control and back".

Five MPI-SWS papers at POPL 2019!

January 2019
Homepage News, New publications
Just as in 2018, MPI-SWS researchers again authored a total of five POPL papers in 2019:

  • Bridging the Gap Between Programming Languages and Hardware Weak Memory Models by Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis.

  • From Fine- to Coarse-Grained Dynamic Information Flow Control and Back by Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan.

  • Formal verification of higher-order probabilistic programs by Tetsuya Sato,
...
Just as in 2018, MPI-SWS researchers again authored a total of five POPL papers in 2019:


  • Bridging the Gap Between Programming Languages and Hardware Weak Memory Models by Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis.

  • From Fine- to Coarse-Grained Dynamic Information Flow Control and Back by Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan.

  • Formal verification of higher-order probabilistic programs by Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu.

  • Grounding Thin-Air Reads with Event Structures by Soham Chakraborty and Viktor Vafeiadis.

  • On Library Correctness under Weak Memory Consistency by Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis.


What's more, the MPI-SWS Software Analysis and Verification group has a whole session to itself at POPL 2019. The weak memory session on Thursday, Jan 17, is comprised of the three papers by Viktor Vafeiadis, his students, postdocs, and collaborators.
Read more