A Pre-expectation Calculus for Probabilistic Sensitivity
Sensitivity properties study how the output of a program changes when we make small changes to its input. How can we reason about sensitivity of programs that have probabilistic behavior?
Archive of posts tagged: formal verification
Verifying a Quantum Compiler
Learn how techniques from traditional compiler verification can be applied to the emerging domain of quantum computing.
Verifying Randomized Algorithms: Why and How?
Randomized algorithms and probabilistic programs play a growing role in many areas of computer science. What can we do to help ensure that these intricate programs are correct, without the bugs and flaws that plague today’s software?
People of PL: Derek Dreyer
People of PL is a series of interviews with PL researchers. In today’s post, John Wickerson chats with Derek Dreyer, who is Faculty at the Max Planck Institute for Software Systems (MPI-SWS), and Honorarprofessor of Computer Science, Saarland University.
Synthesizing Small Programs for Big Impact
The authors of POPL’s 2020 most influential paper reflect on the journey that produced their award winning research on program synthesis, and the impact the work has had on them, the research community, and society at large, ever since.
