جستجوی استاد راهنمای دانشگاهی

• Software Verification
• Formal Methods
• Programming Languages
• +۵ مورد دیگر

Jenna Wise DiVincenzo is an Assistant Professor at the Elmore Family School of Electrical and Computer Engineering at Purdue University. She specializes in research areas such as software verification, formal methods, and programming languages, with a focus on gradual verification techniques that combine static and dynamic analysis. Her work emphasizes usability and scalability in verification tools, and she has contributed to projects like Gradual C0 and gradual null-pointer analysis. Dr. DiVincenzo earned her PhD in Software Engineering from Carnegie Mellon University (2023) and a BS in Mathematics and Computer Science from Youngstown State University (2017). She has interned at IBM Research, MIT Lincoln Laboratory, and the Software Engineering Research and Empirical Studies Lab at YSU. Her awards include the Google PhD Fellowship, NSF GRFP Fellowship, and 2022 Rising Star in EECS. Her research projects span theoretical advancements in gradual verification, empirical studies on usability, and practical tool development. She advises PhD students (e.g., Craig Liu, Conrad Zimmerman) and collaborates on initiatives like gradual verification for Rust and educational tools to teach verification concepts. Her work also explores leveraging large language models for specification generation and enhancing verification tool soundness through formal proofs.

Andreas Lööwمشاهده پروفایل

مدرس

• Hardware Verification
• Software Verification
• Symbolic Execution
• +۵ مورد دیگر

Andreas Lööw is a Lecturer at Royal Holloway, University of London , focusing on hardware and software verification. Previously, he was a postdoctoral researcher at Imperial College London under Philippa Gardner , contributing to the Gillian Platform . He completed his PhD at Chalmers University of Technology under Magnus Myreen , specializing in interactive theorem proving and hardware verification. His research explores symbolic execution, separation logic, and formal verification of hardware/software systems. Key projects include Betterlog (Verilog semantics reformulation) and foundational work on the Gillian Platform . 2025 : Compositional Symbolic Execution for Memory Models 2025 : Simulation Semantics of Synthesisable Verilog 2024 : Compositional Symbolic Execution for Correctness/Incorrectness 2023 : Exact Separation Logic (Distinguished Paper at ECOOP'24) 2023 : Hardware Verification of Pipelined Processors 2022 : Verilog Concurrency Analysis 2021 : Verified Verilog Compiler (Lutsig) Scientific Awards : Distinguished Paper at ECOOP 2024 He maintains the vv Verilog visualization tool and collaborates on the Gillian Platform . Contact: andreas.loow@rhul.ac.uk

Roberto Giacobazziمشاهده پروفایل

استاد

• Theory of computation
• Programming languages
• Abstract interpretation
• +۳ مورد دیگر

Roberto Giacobazzi is a Professor at the University of Arizona specializing in theoretical computer science with a focus on abstract interpretation, program analysis, and verification. His research bridges theoretical foundations with practical applications in software security and verification systems. Dr. Giacobazzi received his Ph.D. from the University of Pisa in Italy in 1993, establishing a long-standing academic career focused on the theoretical underpinnings of program analysis. His educational background forms the foundation for his contributions to abstract interpretation theory. His primary research interests center around abstract interpretation, a theoretical framework for approximating program semantics. This work spans theory of computation , programming languages , program analysis and verification , and logic in computer science . Giacobazzi has made significant contributions to understanding completeness and precision in abstract interpretation, with applications extending to code obfuscation, security analysis, and more recently, AI fairness in legal contexts. His work demonstrates how theoretical computer science concepts can address practical software engineering challenges. An analysis of his recent publications (2022-2025) reveals a consistent research trajectory with increasing sophistication in abstract interpretation theory. His work shows a growing emphasis on completeness properties, precision limitations, and security applications. Notably, his 2024 publication on "Fairness of AI Systems in the Legal Context" indicates an expansion of his theoretical expertise into AI ethics and regulatory compliance, demonstrating the versatility of abstract interpretation frameworks. Dr. Giacobazzi has contributed extensively to major conferences in programming languages and verification, including SAS (Static Analysis Symposium), POPL (Principles of Programming Languages), and VMCAI (Verification, Model Checking, and Abstract Interpretation). His publications reflect deep theoretical insights while maintaining relevance to practical software analysis challenges. His research has significant implications for software security, particularly in code obfuscation techniques based on abstract interpretation. The systematic approach to measuring incompleteness in abstract interpretations has provided new frameworks for understanding and improving program analysis tools. His work continues to influence both academic research and practical applications in program verification and security.

Benjamin Lucien Kaminskiمشاهده پروفایل

استاد

• formal verification
• semantics
• probabilistic programs
• +۱۰ مورد دیگر

Benjamin Lucien Kaminski is a Professor at Saarland University and a Lecturer at University College London . He specializes in quantitative aspects of formal program verification , with a focus on probabilistic and quantum programs , incorrectness logic , and non-classical computation models . His research includes semantics , probabilistic program verification , expected runtimes , and explainable verification . He leads the Examination Board for B.Sc. Computer Science (English) and actively mentors PhD, Master’s, and Bachelor’s students in logic and verification. 2025 : A Taxonomy of Hoare-Like Logics (POPL), Partial Incorrectness Logic (TPSA) 2024 : Quantitative Weakest Hyper Pre (OOPSLA), Caesar: A Verifier for Probabilistic Programs (Dafny), Hoare-Like Triples (Incorrectness-track) 2023 : A Deductive Verification Infrastructure (OOPSLA), Lower Bounds (OOPSLA), A Calculus for Amortized Expected Runtimes (POPL) He has received notable awards including the Ackermann Award (2020), Best Paper at LOPSTR 2020 , and EATCS Best Paper Award at ETAPS 2016 . He has also served on program committees for leading conferences like CAV , POPL , and LICS , and reviewed for prestigious journals such as Journal of the ACM and TOCL .

Binoy Ravindranمشاهده پروفایل

استاد

• Computer Systems
• Software Verification
• Concurrency
• +۷ مورد دیگر

Binoy Ravindran is a Professor at Virginia Tech’s College of Engineering, Department of Electrical and Computer Engineering, leading the Systems Software Research Group (SSRG). His research focuses on computer systems, emphasizing security, performance, concurrency, distributed systems, and real-time computing, with recent work in software verification and heterogeneous-ISA platforms. Key projects: Low-level Reasoning Machine (LLRM), Popcorn Linux, LibrettOS, Hyflow, HermiTux, SlimGuard, HydraVM, KairosVM. He has co-authored 15+ papers from 2025 to 2022, spanning venues like ASPLOS, POPL, PLDI, VEE, PPoPP, and MIDDLEWARE, with awards including ACM Distinguished Scientist and eight Best Paper Awards. Service roles: Editorial Boards (IEEE Transactions on Cloud Computing, ACM TECS), Program Co-Chair (ACM Systor 2025), Committee memberships across ASPLOS, PLDI, and more.

• Programming Languages
• Formal Verification
• Weak Memory Models
• +۴ مورد دیگر

Azalea Raad is a Reader (Associate Professor) in the Department of Computing at Imperial College London, leading the Veritas Lab. She holds a PhD in Computer Science from Imperial College London and is a UKRI Future Leader Fellow since 2021. Her research focuses on programming languages, formal verification, and persistent memory systems, particularly addressing challenges in weak memory models, concurrency, and software correctness. Affiliations: Co-director of the UK Research Institute on Verified, Trustworthy Software Systems Adjunct roles at Facebook (2020–2022) and Bloomberg (2022–present) Education: MEng from Imperial College London PhD in Computer Science from Imperial College London Research Interests: Azalea’s work bridges theoretical foundations and practical system implementation, emphasizing: Formal semantics of persistent and weak memory systems Verification frameworks for concurrent and persistent programs Bug detection in libraries and binaries Transactional memory and system validation Publications: Her recent work explores compositional bug detection, persistent programming principles, and scalable non-termination analysis. Key contributions include frameworks like IsaBIL and Memento, and foundational papers on RDMA robustness and C/C++ memory model extensions. Awards: UKRI Future Leader Fellowship (2021–present). Research recognized through collaborations with industry (e.g., Intel PMDK validation). Labs/Teams: Leads the Veritas Lab, advancing formal methods for trustworthy software systems.

Zhoulai Fuمشاهده پروفایل

دانشیار

• Programming Language Theory and Implementation
• Program Analysis
• Testing and Verification
• +۵ مورد دیگر

Zhoulai Fu is a tenured Associate Professor at the State University of New York (SUNY), Korea, specializing in programming languages and software security. He also holds joint appointments as a Research Associate Professor at Stony Brook University and is affiliated with the Electrical and Computer Engineering Department at Virginia Tech. His educational background includes: Ph.D., 2009-2013, INRIA – Université de Rennes 1, France M.Eng., 2008-2009, Télécom ParisTech, France M.S, B.S, and French engineer degrees (Ingénieur), 2005-2008, École Polytechnique, France Professor Fu's research focuses on the intersection of Programming Languages, Software Security, and Large Language Models, with special emphasis on improving software reliability through formal methods, numerical error analysis, and scalable verification techniques . His work spans abstract interpretation, automated testing, and verification tools development. He has made significant contributions to floating-point analysis and program verification, with publications at top-tier conferences including PLDI, POPL, OOPSLA, ICSE, and CAV. His publication record shows a consistent trajectory in programming language theory with increasing practical applications. Early work focused on foundational aspects of abstract interpretation and floating-point analysis, while recent papers address security concerns through programming language techniques and incorporate modern approaches like incorrectness logic. Key themes across his publications include formal verification of low-level code, numerical error analysis, and developing scalable analysis tools for real-world software systems. His notable achievements include: Principal Investigator for DARPA E-BOSS Program funding Sole Principal Investigator for National Research Foundation of Korea funding Program Committee membership for POPL 2026, FSE 2024, and PLDI 2023 Professor Fu actively mentors students and has taught courses including Foundations of Computer Science, Programming Abstractions, and Research in Computer Science. His research is supported by significant grants from DARPA and NRF, enabling him to lead the Data & Intelligent Computing Lab at SUNY Korea. He is currently seeking postdocs, PhD, and graduate students to join his research team. He leads the Data & Intelligent Computing Lab, which focuses on advancing programming language techniques for software reliability and security. The lab collaborates with institutions including Virginia Tech, Stony Brook University, and international partners across Europe, working on projects that bridge theoretical computer science with practical software engineering challenges.

• Formal Verification
• Programming Languages
• Type Systems
• +۷ مورد دیگر

Arthur Azevedo de Amorim is an Assistant Professor in the Department of Computer Science at the Rochester Institute of Technology (RIT), part of the College of Computing and Information Sciences. His research lies at the intersection of programming languages, formal verification, and software security. Ph.D., University of Pennsylvania (advised by Benjamin Pierce and Cătălin Hrițcu) Postdoctoral Fellow, Boston University and Carnegie Mellon University B.S., Unicamp and Polytechnique His research focuses on enhancing software security and reliability through formal methods, particularly using formal verification , programming languages , and type systems . Key areas include cryptographic protocols , where he develops formalisms based on separation logic to verify protocols like TLS, and compartmentalization , where he analyzes and implements formally verified techniques to limit the impact of vulnerabilities in low-level code. His work includes the development of SECOMP , the first formally verified realistic compartmentalizing compiler. His recent publications span top conferences such as POPL, CCS, ESOP, and ICALP, reflecting a strong trend toward foundational work in program logics, secure compilation, and type-based security. His research often involves deep formalization in the Coq proof assistant, and he contributes to the formal methods community through open-source tools and educational resources like the Software Foundations textbook. He is actively involved in academic service, having served on program committees for POPL, ICFP, PLDI, and others. He mentors several graduate and undergraduate students at RIT and has previously mentored researchers at Boston University. Notable software contributions include: Cryptis : Extension of Iris separation logic for cryptographic protocols Deriving : Coq library for automating class instances Extensional Structures : Coq library for finite data structures Netter : Language for probabilistic network modeling

Arthur Azevedo de Amorimمشاهده پروفایل

استادیار

• Programming Languages
• Formal Verification
• Security
• +۳ مورد دیگر

Arthur Azevedo de Amorim is an Assistant Professor in the Department of Computer Science at the Rochester Institute of Technology's College of Computing. His research focuses on making software more secure and reliable using techniques based on formal verification, programming languages, and type systems. Previously, he held postdoctoral positions at Boston University and Carnegie Mellon University after completing his Ph.D. at the University of Pennsylvania under Benjamin Pierce and co-advised by Cătălin Hrițcu. His educational background includes undergraduate studies in computer science and engineering at Unicamp and Polytechnique. He is also one of the authors of Software Foundations, an introductory textbook to the Coq proof assistant, and maintains an active blog about Coq. Dr. de Amorim's research spans several critical areas in programming languages and security. His work on cryptographic protocols leverages recent advances in program verification (particularly separation logic) to verify cryptographic protocols. His research on compartmentalization analyzes formal guarantees of techniques for limiting the scope of vulnerabilities in low-level languages like C and C++. These research areas reflect his commitment to bridging theoretical foundations with practical security applications. His recent publications demonstrate strong activity across multiple top-tier conferences including POPL, PLDI, CCS, and ICALP, with research spanning formal verification, secure compilation, differential privacy, and programming language theory. His work consistently combines theoretical rigor with practical applications in security and reliability. Dr. de Amorim has served on numerous program committees for major programming languages conferences including POPL, PLDI, ICFP, and CoqPL, demonstrating his active engagement with the research community. He has also contributed to important educational resources through his work on Software Foundations. He currently advises several graduate students at RIT working on various aspects of programming languages and security. His lab develops multiple open-source software projects including Cryptis (for verifying cryptographic protocols), Deriving (a Coq library for automating class instances), and Extructures (a Coq library of finite data structures).

Peter W. O'Hearnمشاهده پروفایل

استاد

• Programming Languages
• Formal Verification
• Separation Logic
• +۵ مورد دیگر

Peter W. O'Hearn is a Professor of Computer Science at University College London and a Research Scientist at Meta AI (FAIR). He has held academic positions at Syracuse University, Queen Mary University of London, and University College London, before joining Facebook (now Meta) in 2013 as part of the acquisition of the verification startup Monoidics. His career spans over 25 years of research in programming languages and logic, with significant contributions to both theoretical foundations and practical industrial applications. O'Hearn's research primarily focuses on formal reasoning about programs, with his most notable contributions being the co-invention (with John Reynolds) of Separation Logic and the development of Incorrectness Logic. His work bridges the gap between theoretical computer science and practical software engineering, emphasizing how fundamental theory, tool development, and real-world application can mutually reinforce each other. He has consistently advocated for the integration of formal methods into industrial software development practices. His research has led to the development of the Infer program analyzer, which runs internally on Meta's code bases and has detected over 100,000 bugs that have been fixed by developers. Infer is also used in production at other major companies including Amazon, Mozilla, Spotify, and Marks and Spencer. His recent work on Incorrectness Logic represents a paradigm shift from traditional program verification approaches, focusing on bug finding rather than correctness proving. O'Hearn has received numerous prestigious awards recognizing both his theoretical contributions and practical impact: Fellow of the Royal Society (elected 2018) Fellow of the Royal Academy of Engineering (2016) 2016 Gödel Prize 2016 CAV Award Two POPL MIP awards Honorary doctorate from Dalhousie University (2018) 2021 IEEE Cybersecurity Award for Practice Throughout his career, O'Hearn has successfully translated theoretical advances into practical tools used at scale in industry. His work on Separation Logic led directly to Infer, while his more recent work on Incorrectness Logic aims to provide foundations for next-generation bug catching tools. He has maintained a strong academic presence while working in industry, continuing his professorship at UCL alongside his role at Meta. O'Hearn leads research efforts at the intersection of formal methods and practical software engineering at Meta, focusing on scaling static analysis techniques to handle the massive codebases typical of modern technology companies. His work has significantly influenced how large tech companies approach software verification and bug detection.

Tobias Wrigstadمشاهده پروفایل

استاد

• Type Systems
• Reference Capabilities
• Programming Languages
• +۲ مورد دیگر

Tobias Wrigstad is a faculty member at Uppsala University, Sweden, with research interests spanning type systems, reference capabilities, programming language design, scripting languages, and concurrent/parallel programming. His work focuses on memory management, concurrency safety, and language extensions for performance optimization. Education: Not explicitly mentioned in provided data Research Interests: Designing type systems to enforce concurrency safety and memory correctness Reference capabilities for manual and automatic memory management Actor model programming and garbage collection co-design Cache locality optimization without program restructuring Formal verification of language designs using Dafny Recent Publications (2025-2015): Explore concurrency safety through region ownership Develop parallel array programming models in Kappa Investigate energy-efficient garbage collection Design capability-based dynamic languages for data race freedom Create formal models for heap invariants and incorrectness Optimize memory allocation via load barriers Conference Involvement: 2025: IWACO Committee Member, OOPSLA Associate Chair 2024: Program Co-Chair for IWACO, Author in VIMPL, MPLR, ISMM 2023: SPLASH Steering Committee, ECOOP PC Member 2022-2015: Active in PLDI, ECOOP, ICFP, and related workshops

Peter O'Hearnمشاهده پروفایل

استاد

• Separation Logic
• Program Verification
• Static Analysis
• +۵ مورد دیگر

Peter O'Hearn is a Professor of Computer Science at University College London and Research Scientist at Meta AI (FAIR), renowned for co-developing separation logic which bridges theoretical computer science and industrial-scale program analysis. His dual affiliation exemplifies the synergy between academic research and practical tool development that characterizes his career. His research interests focus on program verification , separation logic , static analysis , and his recent groundbreaking work on incorrectness logic as a complementary approach to traditional verification. O'Hearn pioneered the concept of local reasoning which enables modular verification of large codebases by focusing only on relevant memory regions, forming the theoretical foundation for Facebook Infer. His publications reveal a consistent trajectory from foundational theory to industrial application, with recent work emphasizing Scalable verification for million-line codebases Compositional reasoning for concurrent systems Practical deployment of formal methods in developer workflows Bug-oriented reasoning through incorrectness logic His research consistently addresses the tension between theoretical soundness and practical applicability in program analysis. Notable scientific awards include: 2021 IEEE Cybersecurity Award for Practice 2016 Gödel Prize for separation logic 2016 CAV Award for outstanding contributions POPL 2019 Most Influential Paper Award Fellow of the Royal Society (FRS) Fellow of the Royal Academy of Engineering (FREng) O'Hearn has made substantial contributions to industrial practice through Facebook Infer, which analyzes millions of lines of code daily across Meta's codebase. His work on continuous reasoning integrates formal verification into developer workflows, while his recent focus on incorrectness logic addresses the critical need for effective bug detection in large systems. He maintains active leadership in the programming languages community through conference organization and keynotes.

Roberta Goriمشاهده پروفایل

دانشیار

• Modelling and Simulation of Biological Systems
• Formal Verification
• Floating-Point Arithmetic Analysis
• +۴ مورد دیگر

Roberta Gori is an Associate Professor at the Dipartimento di Informatica of the University of Pisa. Her research focuses on formal verification techniques for biological systems and floating-point intensive programs, leveraging abstract interpretation and coinductive methods. She collaborates with BUGSENG Srl on safety-critical systems verification and has led multiple projects including 'Metodi Informatici Integrati per la Biomedica' (UniPi 2020-2021) and PRIN initiatives since 2000. Her work bridges theoretical computer science with practical biomedical applications, addressing challenges in program obfuscation, numerical analysis, and systems biology. Education: Background in Computer Science with focus on formal methods Key research interests include: Verification of floating-point computations Modeling biological systems using reaction networks Formal program analysis and abstract interpretation Development of verification tools like FPSE and ECLAIR Notable collaborations include work with Simula Research Laboratory (Norway) and the University of Parma. Her contributions span over 60 publications, emphasizing both foundational theory and industrial applications in safety-critical domains.

Azalea Raadمشاهده پروفایل

پژوهشگر

• Program Logics
• Separation Logic
• Weak Memory Concurrency
• +۱۲ مورد دیگر

Azalea Raad is a researcher at Imperial College London, actively contributing to the fields of programming languages, formal methods, and concurrency. She has a strong presence in top-tier academic conferences such as POPL, PLDI, SPLASH, and ICFP, serving in key roles including program committee member, session chair, and organizing committee member across multiple tracks and co-located events. Her research interests center on weak memory concurrency, non-volatile memory, program logics, separation logic, concurrent reasoning, and verification . She has pioneered work in incorrectness logic and under-approximate reasoning , enabling scalable bug detection in concurrent and persistent systems. Her work bridges formal theory with practical systems challenges, particularly in memory models and semantics for C/C++ and assembly-level concurrency. The recent publications highlight a strong trend toward formalizing memory persistency , extending memory models , and developing logical frameworks for bug detection . The keywords across her work include concurrency, verification, program logics, and systems correctness, with sub-fields spanning separation logic, incorrectness logic, TSO, RDMA, and crash consistency. Her research increasingly focuses on scalable and compositional methods for analyzing unsafe libraries and binaries. She has contributed to academic service through organizing workshops such as O'Hearn Fest , The Future of Weak Memory , and Incorrectness , and has co-chaired the Student Research Competition at POPL. While no grants are explicitly mentioned, her leadership in multiple conference tracks suggests active involvement in funded research and student mentorship. Azalea Raad leads or contributes to collaborative research teams focused on formal semantics and verification tools, often working within frameworks like Isabelle/HOL and developing new logical systems for program analysis. Her personal website, https://www.SoundAndComplete.org , serves as a hub for her research outputs and projects.

Benjamin Kaminskiمشاهده پروفایل

استاد

• Formal Verification
• Probabilistic Programs
• Quantitative Verification
• +۱۲ مورد دیگر

Benjamin Kaminski is a Professor at Saarland University and a Lecturer at University College London, where he contributes to the field of computer science with a strong emphasis on formal verification and logic. He is currently the Head of the Examination Board for the B.Sc. in Computer Science (English) program at Saarland University and actively supervises PhD, Master’s, and Bachelor’s students in research projects related to logic and verification. His research centers on the quantitative aspects of formal program verification , particularly in probabilistic and quantum programs. Key interests include weakest-precondition reasoning, expected runtimes, incorrectness logic, and the integration of machine learning with formal methods. He advocates for explainable verification and explores non-classical models such as weighted programming. His recent publications reflect a consistent focus on probabilistic semantics , runtime analysis , and deductive verification of programs, utilizing formal logic and mathematical structures to ensure correctness and efficiency. These works span high-impact venues such as POPL, LICS, and JACM. Ackermann Award for outstanding dissertations 2020 Distinguished Paper at POPL 2021 Best Paper Award at LOPSTR 2020 EATCS Best Paper Award at ESOP 2016 Borchers Badge for doctoral distinction 2019 Best scientific production award at Université Paris-Saclay 2022 Benjamin Kaminski has advised numerous students at various levels, including current PhD candidates Tobias Gürtler, Lena Verscht, Anran Wang, and Linpeng Zhang. He has served on program committees for top conferences such as POPL, CAV, LICS, and ICALP, and has reviewed for prestigious journals including Journal of the ACM and TOPLAS . He has also evaluated research proposals for the Israel Science Foundation and Czech Science Foundation, highlighting his role in shaping global research agendas. His editorial work includes contributions to Foundations of Programming and Software Systems (2019). He is actively involved in the formal methods research community, contributing to workshops and symposia on static analysis, dependable software engineering, and quantitative evaluation of systems. His leadership in organizing and reviewing for major conferences underscores his influence in theoretical computer science.