جست‌وجوی استاد و پژوهشگر

• Program Analysis
• Program Synthesis
• Program Transformation
• +۵ مورد دیگر

Kihong Heo is an Associate Professor at the School of Computing, Korea Advanced Institute of Science and Technology (KAIST), where he leads the Programming Systems Laboratory. He received his Ph.D. in Computer Science & Engineering from Seoul National University and previously served as an Assistant Professor at KAIST (2017-2019) and a Post-doctoral Researcher at the University of Pennsylvania (2009-2017). His research focuses on developing program reasoning systems for safe and reliable software, with three main thrusts: AI-based program analysis systems for detecting deep semantic software bugs, general-purpose program simplification systems for secure and efficient software, and scalable program synthesis systems for automatic software generation and repair. His work bridges formal methods, programming languages, and machine learning to address critical challenges in software reliability and security. Prof. Heo's recent publications demonstrate a strong trend toward integrating machine learning techniques with traditional program analysis and verification methods. His research spans compiler correctness (particularly for JavaScript engines), mobile security verification, and automated program transformation. The work on 'Safeguarding Mobile GUI Agent via Logic-based Action Verification' (MobiCom 2025) and 'Optimization-Directed Compiler Fuzzing for Continuous Translation Validation' (PLDI 2025) exemplifies his focus on practical verification techniques for real-world systems. ACM SIGSOFT Distinguished Paper Award (FSE 2025) Amazon Research Award (2024) The Soo-Young Lee Teaching Innovation Award, KAIST (2024) Prize for Excellence in Teaching, KAIST (2024) Best Artifact Award, ICSE (2022) ACM SIGPLAN Distinguished Paper Award, PLDI (2019) Prof. Heo actively mentors graduate students, currently advising three Ph.D. students (Yeonhee Ryou, Taeeun Kim, Sujin Jang) and four Master's students. He serves on program committees for major conferences including ICSE, PLDI, OOPSLA, and SAS, and is an Associate Editor for ACM Transactions on Software Engineering and Methodology (TOSEM). His Programming Systems Laboratory develops tools like Sparrow, a state-of-the-art static analyzer for C programs that applies abstract interpretation techniques to verify the absence of fatal bugs.

Anders Møllerمشاهده پروفایل

استاد

• Programming Languages
• Software Engineering
• Static Program Analysis
• +۴ مورد دیگر

Anders Møller is a Professor and Vice Head of Department at the Department of Computer Science, Aarhus University, Denmark. He is a leading researcher in programming languages and software engineering, with a primary focus on static and dynamic program analysis. He serves as Chairman of the PhD Committee and holds leadership roles in the international research community, including Vice-Chair of ACM SIGPLAN and Associate Editor for ACM TOPLAS and ACM TOSEM. His research interests include programming languages, software engineering, static and dynamic analysis, program verification, and security. His work bridges theoretical foundations and practical applications, particularly in improving software reliability and security through advanced analysis techniques. The trends in his recent publications reflect a strong emphasis on static analysis for security, scalability, and real-world impact—especially in web applications, smart contracts, and open-source software supply chains. His research has evolved toward practical deployment, demonstrated by the founding and acquisition of Coana by Socket in 2025 for enhanced vulnerability detection. Recipient of the Danish Elite Research Prize 2020 ACM Distinguished Member He actively mentors students and contributes to the academic community through conference leadership (e.g., OOPSLA, PLDI, ICSE). He also co-authored the widely used textbook Static Program Analysis with Michael I. Schwartzbach. His work is deeply integrated into both academic and industrial advancements in software analysis and security.

Tuan Phong Ngoمشاهده پروفایل

پژوهشگر

• Formal methods
• Concurrent program verification
• Weak memory models
• +۲ مورد دیگر

Tuan Phong Ngo is a Researcher in Computer Science at Uppsala University , Sweden, affiliated with the Department of Information Technology under the Disciplinary Domain of Science and Technology . He specializes in formal methods and software verification.

Jeff Huangمشاهده پروفایل

دانشیار

• Programming Languages
• Software Engineering
• Concurrency
• +۱ مورد دیگر

Jeff Huang is an Associate Professor in the Department of Computer Science and Engineering at Texas A&M University, specializing in programming languages and software engineering with a focus on concurrency and runtime verification. His research develops advanced program analysis techniques and tools to enhance software performance and reliability. Programming Languages Software Engineering Concurrency Runtime Verification His work has been recognized with prestigious awards including the ACM SIGSOFT Early Career Researcher Award, NSF CAREER Award, Google Faculty Research Award, and DARPA Young Faculty Award. Notably, his research has earned multiple SIGPLAN Research Highlights and PLDI Distinguished Paper Awards. ACM SIGSOFT Early Career Researcher Award NSF CAREER Award Google Faculty Research Award Mozilla Research Award Facebook Research Award DARPA Young Faculty Award ACM SIGSOFT Outstanding Dissertation Award ACM SIGPLAN PLDI Distinguished Paper Award SIGPLAN Research Highlights Jeff Huang actively contributes to academic communities as a committee member in venues like SPLASH, ICSE, ISSTA, and PLDI. He has authored influential papers on concurrency bug detection, pointer analysis, and language translation tools, spanning both theoretical foundations and practical implementations.

• Computer Systems Security
• Compilers
• Operating Systems
• +۳ مورد دیگر

V. N. Venkatakrishnan is a Professor and Associate Dean for Research and Graduate Studies at the College of Engineering, University of Illinois at Chicago. His research focuses on Computer Systems Security with applications in web security, exploit detection, and security automation. Education: Ph.D in Computer Science (2004), Stony Brook University Research Interests: Spanning Computer Systems Security , Venkatakrishnan's work integrates compilers , operating systems , and formal methods to develop defenses against cyber attacks. His recent publications emphasize automated attack detection, exploit generation, and security frameworks for web applications. Scientific Awards: Distinguished Paper Award at USENIX Security 2018 Best Paper Award at IEEE QRS 2016 2009 ATT Award for Best Applied Security Research Best Paper Award at ACSAC 2003 Advising and Collaborations: He has mentored numerous Ph.D. and M.S. students including Sadegh Momemi and Maliheh Monshizadeh. Former advisees include Birhanu Mekuria (now at University of Michigan) and Rigel Gjomemo (now Research Assistant Professor at UIC).

Gergely Mezeiمشاهده پروفایل

دانشیار

• Model-driven engineering
• Multi-level modeling
• Formal verification
• +۶ مورد دیگر

Dr. Gergely Mezei is an Associate Professor and Deputy Head of the Department of Automation and Applied Informatics at the Budapest University of Technology and Economics (BME) , Hungary. He is affiliated with the Applied Computer Science Group within the department and is actively involved in research and education in model-driven engineering and formal methods. His research interests lie at the intersection of multi-level modeling , formal verification , and model transformation systems . He has contributed extensively to the development of modeling languages and tools, particularly in the context of DMLA (Deep Multi-Level Architecture) and Melanee , focusing on enabling rigorous, scalable, and verifiable modeling practices. Dr. Mezei's work emphasizes performance optimization in model transformations, visual modeling frameworks , and domain-specific languages . His research spans both theoretical foundations and practical tool implementations, with a strong focus on bridging the gap between formal semantics and usable modeling environments. His recent publications reflect a consistent focus on advancing the state-of-the-art in multi-level modeling and formal verification , with contributions to international workshops such as MULTI and MPM . These works explore challenges in model validation, transformation correctness, and the usability of modeling tools in complex systems engineering. Contact: Email: gmezei@aut.bme.hu Office: Q.B228, Budapest University of Technology and Economics, 1117 Budapest, Magyar tudósok krt. 2., Hungary Phone: +36 (1) 463-3491

Karsten Wolfمشاهده پروفایل

استاد

• Theoretical Computer Science
• Formal Methods
• Model Checking
• +۳ مورد دیگر

Professor Karsten Wolf holds the Chair of Theoretical Computer Science at the Institute of Computer Science, University of Rostock. He serves as Vice-Rector for Studies and Teaching and holds several key positions including Member of the Senate Commission for Studies, Teaching and Evaluation, and Spokesperson of the specialist group "Petri Nets and Related System Models" of the German Informatics Society. His research focuses on theoretical computer science, particularly in the areas of: Development of correct systems Computer-aided verification Algorithms for Web Services Petri Nets and related system models Professor Wolf's publication record demonstrates consistent expertise in formal verification methods, with recent work emphasizing modular state spaces, temporal logic verification, and approximation techniques. His involvement in the Model Checking Contest (2018-2024) shows his commitment to advancing verification methodologies through empirical evaluation and benchmarking. His professional service includes: Editorial board member of LNCS subseries ToPNOC (Theory of Petri nets and other models of concurrency) Editorial board member of Petri Net Newsletter Member of the German Computer Science Society (GI) Head of the Study Commission of the Faculty Day of Computer Science As Vice-Rector for Studies and Teaching, Professor Wolf plays a critical role in shaping educational policies and academic programs at the University of Rostock, bridging his theoretical expertise with practical educational leadership.

Tolga Ovatmanمشاهده پروفایل

استاد

• Algorithms and Computing Theory
• Computer Software and Software Engineering
• Cloud Computing
• +۶ مورد دیگر

Prof. Dr. Tolga Ovatman is a faculty member at the Department of Computer Engineering, Istanbul Technical University , where he has been serving as Head of Department since 2024. His academic career spans roles from Research Assistant (2004-2012) to Associate Professor (2019-2023) and full Professor (2023-present). He previously held administrative roles such as Vice Dean (2018-2022) and Deputy Head of Department (2016-2018). PhD in Computer Engineering (2005-2011) MS in Computer Engineering (2003-2005) BSc from Hacettepe University (1999-2003) His research focuses on model checking , replicated state machines , cloud computing , and object-oriented software . Recent work addresses computation offloading in 6G networks , collaborative text editing data structures , and energy-efficient environmental monitoring systems . Key projects led include Design of a Multiplexed State Machine Storage System for Edge Computing (2022-2024) and Microservice Compatible Symphony Infrastructure Research (2020). He has supervised numerous theses on topics ranging from collaborative text editing to AI applications in watershed management . Publications span IEEE Transactions , Springer , and conferences like CSCE and CLOSER .

Cynthia Kopمشاهده پروفایل

دانشیار

• Term Rewriting
• Higher-Order Term Rewriting
• Implicit Complexity
• +۶ مورد دیگر

Cynthia Kop is an Associate Professor in the Software Science group at Radboud University Nijmegen's Institute for Computing and Information Sciences. She holds a prominent position in the academic community with significant contributions to term rewriting systems and their applications in computer science. Her research interests span several interconnected areas of theoretical computer science: Term rewriting systems (both first and higher-order) Implicit computational complexity Program verification and equivalence Constrained rewriting systems Automated reasoning techniques Her recent work demonstrates a clear trajectory toward applying term rewriting techniques to solve practical problems in program verification and complexity analysis. The three most recent publications from 2019 show her focus on constrained rewriting for program equivalence, higher-order dependency frameworks, and cons-free rewriting for implicit complexity characterization. These works represent the intersection of theoretical foundations with practical applications in software verification. Dr. Kop has secured significant research funding through competitive grants including: NWO VIDI project CHORPE (2021-2026): Constrained Higher-Order Rewriting and Program Equivalence NWO TOP project ICHOR (2019-2023): Implicit Complexity through Higher Order Rewriting Marie Curie project HORIP (2015-2017): Higher Order term Rewriting for Intensional Properties She actively supervises PhD students including Liye Guo, Kasper Hagens, and Deivid do Vale, and has developed several influential tools for the rewriting community: WANDA (termination analysis), CTRL (constrained rewriting), and Cora (comprehensive rewriting analysis framework). Her professional service includes chairing the IFIP working group 1.6 on rewriting and serving on numerous program committees for major conferences in her field.

Thomas P. Jensenمشاهده پروفایل

استاد

• Program Analysis
• Static Program Analysis
• Abstract Interpretation
• +۷ مورد دیگر

Thomas P. Jensen is a Directeur de recherche (Research Director) at INRIA, the French National Institute for Computer Science and Applied Mathematics. He has been affiliated with INRIA since 2010, previously serving as a researcher at CNRS (French National Center for Scientific Research) from 1993 to 2010. Currently, he leads the Epicure project-team on semantic analysis and compilation for secure execution platforms, and since 2022, he serves as director of the Laboratoire d'Excellence CominLabs. His educational background includes a Cand. scient. in Computing and Mathematics from the University of Copenhagen (1990), a PhD from Imperial College, University of London (1992), and a Habilitation à diriger des recherches from Université Rennes 1 (1999). Dr. Jensen's research focuses on program analysis and software security , with particular expertise in static program analysis based on abstract interpretation theory, language-based security, information flow control, and Software Fault Isolation. His work bridges theoretical foundations with practical applications in secure compilation and program verification. His recent publications reveal a strong trend toward formally verified security mechanisms, particularly in the integration of Software Fault Isolation with verified compilers like CompCert. His research spans both theoretical aspects of program semantics and practical security applications, with increasing emphasis on algebraic data types, relational analysis, and formal verification of program transformations. Best paper award at GPCE 2018 for Verification of High-Level Transformations with Inductive Refinement Types Editor of Strategic research and innovation roadmap for the SPARTA cybersecurity competence network (2022) Dr. Jensen has been actively involved in numerous research projects including JavaSec, Decert, Seccloud, AJACS, Anastasec, SPARTA, and SecurEval. His leadership roles in research teams and projects demonstrate his significant contributions to both academic research and practical cybersecurity applications. His work often involves collaboration with researchers across Europe on large-scale cybersecurity initiatives. He maintains strong connections with the international programming languages and security research communities, regularly publishing in top venues including PLDI, POPL, ICFP, SAS, ESOP, and CSF, and participating in program committees for major conferences in these fields.

• Programming Languages
• Formal Verification
• Functional Programming
• +۹ مورد دیگر

Li-yao Xia is a researcher at INRIA Saclay in France, with a focus on programming languages, formal verification, and functional programming. His research explores bidirectional programming, lazy evaluation, concurrency, and mechanized verification using tools like Coq and Haskell. His work spans conferences such as ICFP, POPL, and SPLASH, where he has authored and co-authored papers on topics including interaction trees, transactional objects, and demand semantics for cost analysis. He has also served on program committees for Haskell and HIW. For more details, visit his personal website: https://poisson.chat .

Ningning Xieمشاهده پروفایل

پژوهشگر

• Functional Programming
• Type Systems
• Logics
• +۳ مورد دیگر

Ningning Xie is a researcher affiliated with the University of Toronto, specializing in functional programming, type systems, and logics. Their work spans applications in compilers, code generation, and machine learning, with a focus on compositional programming and effect handling. Research interests include: Functional programming Type systems Logics Compiler design Multi-stage programming Effect handlers Recent publications demonstrate expertise in type-level programming, staged compilation, and effect systems. Key areas include distributive disjoint polymorphism, parallel algebraic effect handlers, and macro systems for OCaml and Haskell. Their work bridges theoretical formalisms with practical language implementations. Contributions to academic service include organizing and reviewing for conferences like POPL, PLDI, ICFP, and Haskell workshops. Notable roles include Publicity Chair for POPL 2026 and Co-chair for PLMW and Artifact Evaluation committees.

Zachary Kincaidمشاهده پروفایل

دانشیار

• Program Analysis
• Logic
• Programming Languages
• +۷ مورد دیگر

Zachary Kincaid is an Associate Professor in the Department of Computer Science at Princeton University. His research focuses on program analysis , logic , and programming languages , with emphasis on making analysis compositional and robust . PhD, University of Toronto (2016) BSc, Western University Research Interests Dr. Kincaid develops algebraic program analysis frameworks combining symbolic methods with abstract interpretation. His work addresses challenges in: Compositional analysis of concurrent and recursive programs Termination analysis for loops with complex control flow Non-linear numerical invariant generation Strategy synthesis for logical games Parameterized program verification Publication Trends His research output spans program analysis (2024-2010), formal verification (2018-2010), concurrency (2016-2010), and automated synthesis (2013-2012). Recent work (2024) explores polynomial ideals and nonlinear ranking functions , while foundational contributions include vector addition systems and recurrence-based invariants . Scientific Engagement Dr. Kincaid contributes to the academic community through: Program Committee service (PLDI, POPL, CAV, IJCAI, LICS, FMCAD, ESOP, etc.) Co-developing the Duet analyzer for unbounded concurrency Collaborative work with leading researchers (Tom Reps, Azadeh Farzan, Jason Breck) Advising & Grants He advises PhD students and leads research funded by the ONR grant N00014-19-1-2318 . Current advisees include Jake Silverman and Shaowei Zhu, while former student Charlie Murphy (PhD 2023) now holds a postdoctoral position at University of Wisconsin-Madison. Labs & Teams Dr. Kincaid co-developed the Duet program analyzer and contributes to tools like Srk and SimSat . His work integrates SMT solvers (MathSAT, Z3) and mathematical frameworks (rational vector addition systems, recurrence relations) for robust program analysis.

• Cyber-Physical Systems
• Hybrid Systems Verification
• Formal Methods
• +۳ مورد دیگر

Stefan Alexander Schupp is a researcher affiliated with the Department of Cyber-Physical Systems at Technische Universität Wien (TU Wien). His work focuses on formal verification, hybrid systems, and controller synthesis for cyber-physical systems. Department: Cyber-Physical Systems (E191-01) Research Affiliation: TU Wien Network Lab Research interests include: Hybrid and stochastic system verification Controller synthesis for real-time systems Formal methods in software engineering Design and analysis of safety-critical systems Automated model checking techniques Flowpipe construction for reachability analysis Recent publications highlight collaborations with researchers from multiple institutions, covering topics such as: Hyperproperty verification in distributed systems Metric Temporal Logic (MTL) controller synthesis Adaptive simplex architectures for bounded-liveness properties Stochastic hybrid automata analysis tools HyPro verification tool developments Probabilistic reachability optimization

Nada Aminمشاهده پروفایل

استادیار

• Programming Languages
• Artificial Intelligence
• Metaprogramming
• +۴ مورد دیگر

Nada Amin is an Assistant Professor of Computer Science at Harvard University's John A. Paulson School of Engineering and Applied Sciences (SEAS), where she leads the metareflection lab . Her research combines programming languages (PL) and artificial intelligence (AI), focusing on neuro-symbolic systems that are correct by construction, with applications in program synthesis, verification, and precision medicine. Harvard John A. Paulson School of Engineering and Applied Sciences (2019–Present) University Lecturer in Programming Languages at University of Cambridge (2017–2019) Doctoral and postdoctoral work at EPFL (2011–2017) Her research spans three core themes: Safer : Type systems and formal verification (Coq, Dafny, Frama-C) Faster : Multi-stage programming and interpreter collapsing techniques Easier : Neuro-symbolic AI for program manipulation and biological reasoning Key publications include: 2025: Modular Imperative with LLMs (LMPL), Multi-stage Relational Programming (PLDI) 2024: Persimmon for extensible variant types (OOPSLA) 2023: LURK for recursive knowledge (ICFP), Dolorem language growth pattern (ECOOP) Scientific honors include: Teaching Assistant Team Award (EPFL, 2015) Michigan Cambridge Research Initiative Grant (2018) ArsDigita Prize (1999) She has served on program committees for GPCE (co-chair), ICFP, PLDI, and organized workshops in metaprogramming and logic programming. Her teaching portfolio includes graduate courses on neurosymbolic programming, program synthesis, and advanced PL theory.