OOPSLA 2016 was in Amsterdam this week. Each day of the conference, one of my students presented his work:
On Wednesday, Pavel Panchekha presented "Automated Reasoning for Web Page Layout". To create a good-looking HTML webpage, it is necessary to use CSS styling. Pavel's Cassius system takes as input a picture or mockup of a webpage, and it outputs a CSS stylesheet that will produce the given layout. This is one application of a formalization of CSS that can be used not just for synthesis of CSS code, but also for automated verification and debugging.
On Thursday, Konstantin Weitz presented "Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver". BGP is a networking protocol that determines how packets are routed through the internet. ISPs configure their routers with BGP configurations, with the aim of providing good service, making a profit, satisfying contractual obligations, and not disrupting other parts of the Internet. The Bagpipe tool verifies these properties, and it found multiple errors in real-world BGP configurations.
On Friday, Calvin Loncaric presented "A Practical Framework for Type Inference Error Explanation". Type inference is famous for being a powerful way to relieve programmers of the burden of writing types, and is equally famous for giving misleading error messages, often in the wrong part of the program, when the program contains an error. Calvin's work shows a way to improve the error messages that are produced by type inference.
If you missed the conference, then be sure to check out their papers!