I'm a member of the madPL group and I am looking for talented self-driven students to work on the following projects. Email your CV if interested.My research is about developing fundamental verification and synthesis techniques that
help programmers writesoftware that meets their intent
Can we predict when and understand why synthesis works? Can we design general logical frameworks for program synthesis? Can we solve synthesis problems with quantitative objectives? What is the relation between synthesis and machine learning? Take a look at SemGuS and Nay.
Design scalable and effective formal methods for proving robustness, fairness, and other properties of machine learning algorithms and models. Take a look at Antidote and FairSquare.
Allow network operators to verify, design, and repair network configurations by providing high-level intents (i.e., desirable network policies) instead of low-level configurations that are hard to program. Take a look at Genesis and D2R.
Combine automata theory with the power of decidable Boolean theories (e.g., SMT solvers) to reason about strings and tress over complex and infinite alphabets. Read more here.