Nadia Polikarpova is an Associate Professor in the Department of Computer Science and Engineering at the University of California, San Diego . She earned her PhD from ETH Zurich in 2014 under Bertrand Meyer , followed by postdoctoral research at MIT CSAIL with Armando Solar-Lezama . Her academic contributions have been recognized with prestigious awards including the 2020 Sloan Fellowship , 2020 Intel Rising Stars Award , and 2020 NSF CAREER Award . Polikarpova's research focuses on program synthesis , program verification , and type systems . She leads the Programming Systems group at UCSD and contributes to the IFIP Working Group 2.8 on Functional Programming since 2022. Her work spans foundational research and practical tools, including projects like Synquid , SuSLik , and Laurel that combine formal methods with machine learning for code generation. Her recent publications in venues like OOPSLA , NeurIPS , and ICFP reveal trends in AI-assisted programming , live programming environments , and formal verification . She has advised numerous PhD and Master’s students including Shraddha Barke , Zheng Guo , and Tristan Knoth , many of whom have moved to prominent academic and industry positions. Notable artifacts from her lab include tools like ColDeco for spreadsheet inspection and Superfusion for eliminating intermediate data structures. 2020 : Sloan Fellow 2020 : Intel Rising Stars Award 2020 : NSF CAREER Award 2021 : Distinguished Paper at POPL 2023 : Distinguished Artifact at PLDI 2023 : Distinguished Paper at OOPSLA Polikarpova actively contributes to academic service, serving on program committees for PLDI , POPL , and OOPSLA , and co-chairing the OOPSLA Review Committee in 2023. She has delivered keynotes at APLAS'20 and PLDI'24 , emphasizing the integration of large language models with formal methods.
Sean Welleck is an Assistant Professor at Carnegie Mellon University's School of Computer Science, Language Technologies Institute, leading the L3 Lab. His research focuses on bridging informal and formal reasoning with AI, spanning machine learning for mathematics and code, inference algorithms, and AI agents. PhD in Computer Science from New York University (advised by Kyunghyun Cho) Postdoctoral work at University of Washington (advised by Yejin Choi) His work explores AI-driven formal methods for mathematics and code generation, test-time compute scaling, and algorithms enabling AI improvement over time. Recent publications analyze reasoning evaluation, premise selection, and automated proof optimization in systems like Lean. Key article trends include neural theorem proving, code generation, and inference-time compute optimization. Awards: NVIDIA AI Labs Pioneering Research Awards (2017, 2018), NAACL 2025 Best Paper. Current advisees include PhD students Pranjal Aggarwal, Weihua Du (co-advised with Yiming Yang), Andre He (co-advised with Daniel Fried), and Seungone Kim (co-advised with Graham Neubig). He co-organizes workshops like Autoformalization for the Working Mathematician (ICERM 2025) and VerifAI: AI Verification in the Wild (ICLR 2025), and teaches Advanced NLP at CMU.
Anil Madhavapeddy serves as Professor of Planetary Computing at the University of Cambridge's Department of Computer Science and Technology and directs the Cambridge Centre for Carbon Credits (4C). A Fellow of Pembroke College, he integrates systems research with environmental conservation through the Computer Laboratory's Environment and Energy Group. His career spans industry leadership (NetApp, Citrix, Intel), academic appointments (Cambridge, Imperial, UCLA), and entrepreneurial ventures (XenSource, Unikernel Systems, Docker). Madhavapeddy earned his PhD at Cambridge's Computer Laboratory in 2006. His research bridges computational systems and planetary-scale environmental challenges, with deep expertise in open-source development (OCaml, Xen, Docker, OpenBSD) and technology strategy advising for organizations including Zededa, Tezos Foundation, and Tarides. His work centers on environmental computing and climate informatics, leveraging distributed systems and functional programming to develop sensing infrastructure for conservation. Recent projects focus on carbon credit systems, AI-driven biodiversity monitoring, and sustainable computing architectures that minimize ecological footprints while maximizing analytical capability. Analysis of his 2025 publications reveals a concentrated effort on AI-integrated conservation tools, privacy-preserving carbon accounting, and energy-efficient computing. Key themes include spatial networking for ecological data, LLM-enhanced evidence retrieval in conservation science, and novel metrics for extinction risk assessment—demonstrating computational innovation applied to urgent planetary boundaries. No scientific awards were documented in the source material. Madhavapeddy advises multiple technology firms on strategic development while leading the Cambridge Centre for Carbon Credits, though specific grant funding details remain unreported. He actively contributes to the Environment and Energy Group at Cambridge's Computer Laboratory and directs the interdisciplinary Cambridge Centre for Carbon Credits (4C). His open-source leadership spans critical infrastructure projects including OCaml, Xen, and Docker, fostering collaborative development communities that underpin modern cloud and container technologies.
Cezary Kaliszyk is a Professor in Theoretical Computer Science at the University of Melbourne, previously affiliated with the University of Innsbruck. He is actively involved in research and leadership in formal methods, automated reasoning, and machine learning for theorem proving. Research Interests: Automated Reasoning and Interactive Theorem Proving Formalized Mathematics and Proof Automation Machine Learning for Logic and Theorem Proving Integration of AI with Proof Assistants (Coq, Isabelle) Dependent Type Theory and Higher-Order Logic His recent publications (2023–2025) span topics in dependently-typed logic, learning for proof guidance, formalization of surreal numbers, and blockchain-based formal methods. The works consistently bridge formal logic with machine learning, emphasizing automation, explainability, and cross-system integration. Scientific Leadership and Projects: Principal Investigator, ERC project FormalWeb3 Lead Developer, CoqHammer , Tactician , ProofWeb WG5 Leader, COST Action EuroProofNet (until 2024) Contributor to HOL(y)Hammer , Isabelle Enigma He supervises multiple PhD students and has mentored several graduates in formal methods and AI. He teaches courses in theoretical computer science, logic, and machine learning. There are no listed awards in the provided data, but his extensive publication record and project leadership indicate significant recognition in the field. Labs and Research Groups: He leads a research group focused on formal methods and learning-based reasoning, collaborating internationally on projects involving proof automation, formal libraries, and semantic technologies.
Professor Peter Y. K. Cheung is a Professor of Digital Systems at Imperial College London, holding dual affiliations within the Department of Electrical and Electronic Engineering and the Dyson School of Design Engineering. His work focuses on reconfigurable systems, FPGA architectures, and high-level synthesis tools. He co-founded one of the UK's leading FPGA research groups with Professor Wayne Luk, addressing challenges in variability mitigation, reliability, and application-specific FPGA deployments. His research spans Field-Programmable Gate Arrays (FPGAs) Reconfigurable computing Neural network acceleration Cryptographic protocols Embedded systems He has pioneered techniques such as logic shrinkage for FPGA-based neural networks and developed frameworks like LUTNet for efficient inference. His contributions also include fault-tolerant FPGA designs and methodologies for distributed computation protocols. Key collaborations include work with the Department of Computing on FPGA-based AI acceleration and cybersecurity applications. His recent work explores edge computing, secure decentralized systems, and pandemic modeling using adaptive control strategies. Notable projects include the DSCS protocol for secure distributed computation, acceleration of gravitational wave detection algorithms, and energy-efficient CNN implementations. His research bridges hardware-software co-design with real-world applications in healthcare, finance, and aerospace.
Talia Ringer is an Assistant Professor in the Department of Computer Science at the University of Illinois, where she is a member of the PL/FM/SE (Programming Languages/Formal Methods/Software Engineering) research group. She leads the Illinois Theorem Provers (ITP) lab, which focuses on advancing proof engineering technologies to make formal verification accessible to programmers of all skill levels across all domains. Research Interests Dr. Ringer's research spans multiple aspects of proof engineering with a strong focus on integrating techniques from dependent type theory, program transformations, and neural proof synthesis to solve real-world verification challenges. Her work addresses how to build systems that allow programmers to prove the absence of costly or dangerous bugs in software. She is particularly interested in proof repair, machine learning for proofs, and developing new methodologies that can drive the creation of large, secure, and robust verified software and hardware systems. Research Trends Dr. Ringer's recent publications demonstrate a strong shift toward integrating machine learning with formal verification, particularly in proof repair and synthesis. Her work explores how large language models can assist with theorem proving, how reinforcement learning can automate verification processes, and how to make proof engineering more practical for real humans. Many publications involve collaborations with students and researchers from multiple institutions, reflecting her commitment to interdisciplinary research. Awards and Recognition Distinguished Paper Award at ESEC/FSE 2023 for "Baldur: Whole-Proof Generation and Repair with Large Language Models" ACM SIGPLAN Distinguished Service Award in 2023 Mentoring and Service Dr. Ringer is a dedicated mentor who has advised numerous undergraduate and graduate students. She is the founder and president of the Computing Connections Fellowship, which provides transitional funding for computer science PhD students needing to escape unhealthy environments. She is also the founder and previous chair of the SIGPLAN Long-Term Mentoring Committee (SIGPLAN-M), which connects more than 200 mentors and 300 mentees across more than 44 countries. Her service work was formally recognized with the 2023 ACM SIGPLAN Distinguished Service Award. Laboratory and Collaborations Dr. Ringer leads the Illinois Theorem Provers (ITP) lab with current members including postdocs, PhD students, masters students, and undergraduates. She collaborates extensively with researchers at the University of Washington, UMass Amherst, Google Research, Galois, and other institutions on various proof engineering projects.
John Wawrzynek is a Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He is affiliated with the Department of Electrical Engineering and Computer Sciences in the College of Engineering and serves as Co-Director of the Berkeley Wireless Research Center and Co-PI of the CONIX Research Center, one of the six centers in the Joint University Microelectronics Program sponsored by DARPA. Dr. Wawrzynek received his B.S. in Electrical Engineering from SUNY, Buffalo (1977), M.S. in EE from the University of Illinois, Urbana/Champaign (1979), and Ph.D. in Computer Science from Caltech (1987). Before joining the Berkeley faculty in 1988, he worked as a consultant at Schlumberger Palo Alto Research. His research focuses on Computer Architecture, Reconfigurable Computing, Wireless Systems, and Integrated Circuit and System Design . His work spans both theoretical foundations and practical implementations, with particular emphasis on FPGA-based computing systems, reconfigurable architectures, and wireless communication systems. His research group has made significant contributions to the field of reconfigurable computing, including the development of the Garp architecture and various tools for reconfigurable computing systems. Analysis of his recent publications (2022-2025) reveals continued focus on reconfigurable computing, FPGA design, wireless networking, and formal methods for hardware verification. His work shows an evolution from traditional computer architecture towards specialized hardware acceleration, machine learning for EDA, and wireless systems research, with particular emphasis on SAT sampling, differentiable computing, and efficient FPGA implementation of neural networks. DAC's Most Influential Paper Award (2025) NSF Presidential Young Investigator (PYI) (1989) Charles Lee Powell Fellowship (1985) NASA Certificate of Recognition (1983) Rensselaer Engineering and Science Medal (1975) Professor Wawrzynek has advised numerous graduate students throughout his career, many of whom have gone on to prominent positions in both industry and academia including Google, Xilinx, and MIT Lincoln Laboratory. His research has been supported by various grants from NSF, DARPA, and industry partners. He leads the Berkeley Wireless Research Center, which focuses on next-generation wireless communication systems and technologies, and is actively involved in the CONIX Research Center which explores connected intelligence at the network's edge.
Siddharth Garg is the Institute Associate Professor of Electrical and Computer Engineering at NYU Tandon School of Engineering, leading the EnSuRe Research Group. He holds a Ph.D. from Carnegie Mellon University (2009) and a B.Tech. from IIT Madras. His research focuses on secure and energy-efficient computing systems, integrating machine learning, cybersecurity, and hardware design. He previously held roles as Assistant Professor at NYU Tandon (2014-2020) and the University of Waterloo (2010-2014). Key affiliations include NYU Center for Cybersecurity (CCS), NYU Wireless, and the Center for Advanced Technology in Telecommunications. His work has been recognized with prestigious awards like the NSF CAREER Award (2015) and inclusion in Popular Science’s 'Brilliant 10' (2016). Notable research includes private inference optimization, secure hardware IP protection, and adversarial machine learning defenses. Publications highlight advancements in zero-knowledge proofs, AI-driven chip design, and mitigating backdoor attacks in neural networks. His grants include funding from NYU Wireless and NSF initiatives like the Chips4All project. The EnSuRe group emphasizes bridging software and hardware design gaps using AI and fostering cybersecurity education.
Shuvendu K. Lahiri is a researcher at Microsoft Research, focusing on formal verification, program synthesis, and software testing. His work bridges artificial intelligence with formal methods, particularly in blockchain security and automated code generation. 2025 : Published LLM-Vectorizer (verified loop vectorizer) and neural synthesis for SMT-assisted proof-oriented programming 2024 : Explored LLM-based test-driven code generation and natural precondition inference 2023 : Developed resource management specifications and contributed to test generation with pre-trained models 2022 : Advanced Solidity type systems and merge conflict resolution using language models His research combines large language models with formal verification tools to improve software correctness. He actively contributes to conferences like ICSE, PLDI, and ISSTA as author and committee member.
Hans Tompits is an Associate Professor in the Department of Knowledge-Based Systems at Technische Universität Wien (Vienna University of Technology). His research focuses on computational logic, declarative logic programming, and formal methods, with a particular emphasis on Answer-Set Programming (ASP). He coordinates the Master's program in Logic and Computation and leads projects in areas such as formal methods for optimization, fault-tolerant autonomous systems, and algorithmic composition. His work bridges theoretical advancements with practical applications, including tools like SeaLion (an ASP IDE with debugging support) and dlvhex (an ASP-based semantic web reasoner). He has contributed to foundational topics like program equivalence, debugging techniques, and integration of ASP with external systems. His recent projects address challenges in autonomous vehicle architectures, music composition algorithms, and safety-critical system design. Tompits has published extensively on topics ranging from nonmonotonic reasoning and modal logics to the development of declarative programming tools. His interdisciplinary approach spans computer science, mathematics, and AI, with applications in both academic and industrial contexts.
Wei Ding is a Professor in the Department of Computer Science at the University of Massachusetts Boston (UMass Boston). She earned her Ph.D. in Computer Science from the University of Houston in 2008. From 2019 to 2023, she served as a Program Director at the National Science Foundation's Division of Information and Intelligent Systems (IIS), overseeing programs in Information Integration, Smart Health, Deep Learning Foundations, and Scalable Systems. Her research integrates knowledge discovery, data mining, and machine learning with applications spanning health sciences, astronomy, geosciences, and environmental sciences. She employs advanced techniques like spatio-temporal modeling, deep neural networks, and semantic analysis to address complex real-world problems such as disease subtyping, physical activity prediction, and environmental forecasting. Her work emphasizes interdisciplinary collaboration and societal impact. Analysis of her recent publications reveals a focus on AI-driven healthcare solutions (e.g., neuroimaging biomarkers, disorder diagnosis), fundamental ML advancements (e.g., generalization, GAN stability), and cross-domain applications (e.g., climate forecasting, animal behavior analysis). Recurring themes include low-data learning, interpretability, and scalable algorithms. Awards & Honors: IEEE Fellow (2023) NSF Director's Award (2022) WISAY Distinguished Woman in Science Award, Yale University (2019) AI for Earth Award (2018) Best Paper Awards (ICTAI 2011, ICCI 2010) Advising & Grants: She mentors PhD and Master’s students in the Knowledge Discovery Lab (KDLab), with alumni at institutions like Facebook, Google, and McKinsey. Her research is funded by NSF, NIH, NASA, and DOE, including: NIH R01: Predicting youth physical activity (2016) NSF EAGER: Machine learning for cancer subtyping (2017) NIH R01: Accelerometer/gyroscope data for activity estimation (2022) Leadership: She directs the KDLab and co-founded the Women in Sciences Club (WINS). She serves as Associate Editor for ACM TKDD, TIST, and KAIS journals.
Ralf Peeters is a Full Professor in Mathematics of Knowledge Engineering at Maastricht University's Faculty of Science and Engineering , Department of Advanced Computing Sciences. He serves as Vice-Dean of Research and Director of the STEM Graduate School, while leading the university's team at the inter-university research school DISC and co-chairing the Mathematics Centre Maastricht. Education: PhD in Mathematics (Free University, Amsterdam, 1994) Technical Mathematics (Delft University of Technology, 1988) Research Interests span applied mathematics, systems and control theory, signal/image processing, artificial intelligence, and biomedical engineering applications. His work bridges mathematical techniques with real-world challenges in healthcare and industrial systems. Recent Publications highlight advancements in deep learning for cardiac signal reconstruction, tensor-based signal decomposition, and recurrence plot analysis. These works integrate machine learning with clinical diagnostics, particularly in electrocardiographic imaging and arrhythmia characterization. Key Collaborations: Mathematics Centre Maastricht Dutch Mathematics Platform Dutch Institute of Systems and Control Leadership Roles: Vice-Dean of Research (FSE), Director of STEM Graduate School, Head of DISC-affiliated team, and Co-Chair of Mathematics Centre Maastricht. He has supervised over 25 PhD projects, emphasizing applied research across health and industrial domains.
Zachary Tatlock is an Associate Professor at the Paul G. Allen School of Computer Science & Engineering at the University of Washington, where he leads the Programming Languages & Software Engineering Group (PLSE) and the SAMPL Group. His research spans programming languages, formal verification, compilers, and computational fabrication. He is also an Amazon Scholar with AWS's Automated Reasoning Group and previously advised OctoML. Tatlock's work bridges theoretical foundations with practical systems, focusing on making it easier to write tricky code while ensuring correctness through rigorous proofs and measurements. PhD in Computer Science & Engineering, University of California, San Diego (2014) Thesis: Reducing the Costs of Proof Assistant Based Formal Verification Advisor: Sorin Lerner BS in Computer Science (Honors) and Mathematics, Purdue University (2007) Professor Tatlock's research focuses on the intersection of programming languages, formal methods, and systems. His work in compilers and formal verification aims to make it easier to write tricky code while ensuring correctness through rigorous proofs. He explores computational fabrication techniques that bridge digital design with physical manufacturing. His recent work on equality saturation (via the egg framework) has transformed program optimization and synthesis. Tatlock also investigates floating-point numerics, distributed systems verification, and hardware/software co-design, always seeking to balance theoretical rigor with practical implementation. Tatlock's recent publications demonstrate a strong focus on equality saturation techniques (egg framework), computational fabrication, and verified systems. His work increasingly integrates machine learning with program analysis and synthesis. There's a clear trajectory toward more practical applications of formal methods in real-world systems, particularly in numerical computing and fabrication. His research group has made significant contributions to e-graph technology, floating-point accuracy, and the verification of distributed systems. Distinguished Paper Award for Rewrite Rule Inference Using Equality Saturation (OOPSLA 2021) Spotlight Paper Award for Dynamic Tensor Rematerialization (ICLR 2021) Distinguished Paper Award for egg: Fast and Extensible Equality Saturation (POPL 2021) Faculty Appreciation for Career Education & Training (FACET) Award (2020) NSF CAREER Award: Verifying Distributed System Implementations (2017) Distinguished Paper Award for Automatically Improving Accuracy for Floating Point Expressions (PLDI 2015) Distinguished Teaching Award Nomination (2015) Professor Tatlock has advised numerous doctoral, master's, and undergraduate students who have gone on to prominent positions in academia and industry, including faculty positions at the University of Utah and Brown University, and leadership roles at companies like OctoML and Certora. His research is supported by significant funding from NSF, DARPA, DOE, and industry partners, totaling millions of dollars. Current grants include projects on computer-aided reasoning, formal verification, computational fabrication, and machine learning systems. He has served on numerous program committees and organized workshops including FPTalks, EGRAPHS, and PNW PLSE. As co-leader of the Programming Languages & Software Engineering (PLSE) research group and affiliate of the SAMPL Group at the University of Washington, Tatlock has developed influential tools including egg (an equality saturation toolkit), Carpentry Compiler, and Odyssey. His group actively collaborates with industry partners including Amazon Web Services, where he serves as an Amazon Scholar. The group has made significant contributions to equality saturation, floating-point accuracy, program synthesis, and computational fabrication, with applications ranging from compiler optimization to 3D printing.
Roopsha Samanta serves as an Assistant Professor in the Department of Computer Science at Purdue University, where she leads the Purdue Formal Methods (PurForM) research group and participates in the Purdue Programming Languages (PurPL) initiative. Her academic foundation includes a PhD from the University of Texas, Austin (2013) and postdoctoral research at the Institute of Science and Technology Austria prior to joining Purdue in 2016. Education: PhD in Computer Science, University of Texas, Austin (2013) Postdoctoral Researcher, Institute of Science and Technology Austria Professor Samanta's research centers on bridging formal methods with programming languages to enhance software reliability, with core expertise in program verification, program synthesis, and concurrency. Her work uniquely targets both professional developers and non-programmers, developing techniques to ensure programs align with user intent through automated reasoning and synthesis. Recent efforts focus on distributed systems verification where traditional methods face scalability challenges. Analysis of her 2020-2024 publications reveals a dominant trajectory in distributed agreement systems, particularly advancing parameterized verification for unbounded process networks. Key innovations include bounded verification techniques for doubly-unbounded systems, explainable synthesis through specification localization, and secure multi-party computation frameworks like HACCLE. Her work consistently integrates theoretical formal methods with practical system implementation. Scientific Awards: NSF CAREER Award (2019) for “Robustness of Inductive Reasoning Engines” Amazon Research Award (2021) supporting secure computation research Her research is primarily funded through competitive grants including the NSF CAREER award and Amazon Research Award, enabling exploration of verification robustness and secure multi-party computation. While specific advising details aren't publicly documented, her leadership of the PurForM group indicates active mentorship of graduate researchers in formal methods. Current projects suggest expanding applications to privacy-preserving technologies and explainable AI-assisted programming. The PurForM research group, under her direction, develops foundational tools for program verification and synthesis with emphasis on distributed and concurrent systems. Collaborations within PurPL and industry partners like Amazon drive translational research from theoretical models to practical verification frameworks applicable to real-world distributed infrastructure.
Michael Benedikt is a Professor of Computer Science at the University of Oxford and a Governing Body Fellow of University College. He holds the role of Director of the Advanced MSc in Computer Science program. His research focuses on databases, Web data management, logical methods in computer science, and theoretical computer science. Benedikt's work intersects with artificial intelligence, machine learning, and algorithms, with contributions to query languages, data integration, and formal methods. Education: Ph.D. in Mathematics, University of Wisconsin, 1993 Prior roles: Distinguished Member of Technical Staff at Bell Laboratories (1994–2006), visiting researcher at Yahoo! Labs Research Interests: Databases and information exchange Web and Web 2.0 data management Logical methods in computer science Formal verification and query optimization Applications in AI and machine learning Key Projects: FOX : Query-driven data acquisition from web-based sources PDQ : Proof-driven query answering over web-based data TRANCE : Transforming nested collections efficiently Awards: Best Paper Award at ICALP 2017 (Track B) EPSRC Established Career Fellowship (2015–2020) Advising & Grants: Directed the MSc in Advanced Computer Science program Supervised PhD students including Chia-Hsuan Lu and past advisees such as Luying Chen and Ben Spencer Received funding for projects like the ERC DIADEM initiative Labs & Teams: Active in the Department of Computer Science’s research groups, including the Algorithms At Large and Databases teams.
