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

Tachio Terauchiمشاهده پروفایل

استاد

• Programming Languages
• Program Verification
• Program Synthesis
• +۶ مورد دیگر

Tachio Terauchi is a Professor in the Department of Computer Science and Engineering at Waseda University, Japan. Previously, he held academic positions at JAIST (Professor, 2014-2017), Nagoya University (Associate Professor, 2011-2014), and Tohoku University (Assistant Professor, 2007-2011). He actively participates in program committees for premier conferences including POPL, PLDI, and SPLASH, with current service for SPLASH 2025 and POPL 2025. His academic background: B.S. in Computer Science, Columbia University (2000) M.S. in Computer Science, University of California, Berkeley (2004) Ph.D. in Computer Science, University of California, Berkeley (2006) Terauchi's research centers on techniques for building reliable computational systems through programming languages and formal methods. His core contributions span program verification for higher-order functional programs, security analysis of timing channels and regex vulnerabilities, and refinement type systems. Recent work demonstrates particular expertise in regular expressions with backreferences and temporal logic verification. His publications from 2020-2025 reveal a dominant focus on regular expression security (ReDoS vulnerabilities and repair methods) and advanced program verification techniques. This work bridges theoretical foundations in automata theory and mathematical logic with practical security applications, showing increasing specialization in regex analysis since 2022 while maintaining contributions to verification frameworks. Scientific Awards: None explicitly mentioned in the provided text. He currently advises a substantial cohort of students across all academic levels at Waseda University, with his lab actively recruiting prospective students. The lab, located in room 209B of Building 62W, supports research in programming languages and security verification through regular appointments. PhD Students: Tianrui Chen (D2), Taisei Nogami (D1) Master's Students: Kazuma Kawahara (M2), Yuta Uchijo (M2), Naoya Anada (M2), Yuki Nakayama (M1), Taisei Iida (M1) Bachelor's Students: Riru Oda (B4), Riku Ito (B4), Haruto Ishiyama (B4), Rei Tomori (B3), Rio Onoda (B3) Visiting Scholar: Nariyoshi Chida

• Software Engineering
• Software Evolution
• Knowledge Worker Productivity
• +۴ مورد دیگر

Gail Murphy is a Professor in the Department of Computer Science and Vice-President Research & Innovation at the University of British Columbia (UBC). A co-founder of Tasktop Technologies Incorporated, she leads the Software Practices Lab and is affiliated with CAIDA (Centre for Artificial Intelligence Decision-making and Action) and ICICS (UBC Institute for Computing, Information and Cognitive Systems). B.Sc. (Honours), University of Alberta (1987) M.Sc., University of Washington (1994) Ph.D., University of Washington (1996) Her research focuses on software engineering , particularly improving knowledge worker productivity and tools for evolving large-scale systems. She combines lightweight design approaches with industrial evaluations, addressing structural degradation in software systems through: Techniques for understanding/imposing structure in existing systems Design approaches for component reuse and flexible architectures Her recent work includes developer discussion analysis for design recovery (2022), semantic-based task relevance detection (2022), and automated resource-task association (2023). Awards include SIGSOFT Outstanding Research Award (2023), ACM Fellow (2023), and Royal Society of Canada Fellow (2023). She has taught courses like Introduction to Software Engineering (CPSC 310) and Software Construction (CPSC 210).

Dmitriy Traytelمشاهده پروفایل

دانشیار

• Interactive Theorem Proving
• Runtime Verification
• Logic
• +۱۱ مورد دیگر

Dmitriy Traytel is an Associate Professor at the Department of Computer Science (DIKU), Faculty of Science, University of Copenhagen, where he leads the Software, Data, People & Society (SDPS) section. He earned his PhD from TU München under the supervision of Tobias Nipkow in 2015 and previously held a senior researcher position at ETH Zürich's Information Security Group. His primary research interests include interactive theorem proving, runtime verification, logic, automata, decision procedures, and coinduction. He works extensively with the Isabelle/HOL proof assistant, developing foundational theories and verified tools. His work bridges theoretical logic and practical system verification, focusing on correctness, expressiveness, and scalability. The recent publications highlight a strong focus on verified runtime monitoring, formalization of logical systems, and efficient query evaluation. Key themes include the development of formally verified monitoring tools (e.g., TimelyMon, WhyMon, VeriMon), foundational work on corecursion and datatypes in Isabelle, and translations of logical formalisms into executable and verifiable code. Several publications have received distinguished paper awards, indicating high impact in the programming languages and verification communities. Distinguished Paper Award, POPL 2025: 'Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings' Distinguished Paper Award, POPL 2023: 'Admissible Types-to-PERs Relativization in Higher-Order Logic' Distinguished Paper Award, ATVA 2018: 'Optimal Proofs for Linear Temporal Logic on Lasso Words' Best Student Paper Award, FSCD 2016: 'Formal Languages, Formally and Coinductively' Traytel has (co)supervised numerous PhD, MSc, and BSc students, many of whose projects contribute directly to his research agenda in verified systems and formal methods. He is actively involved in the academic community, serving on program committees for POPL, ITP, RV, and CPP, and has chaired conferences such as CPP 2023 and 2024. His tools, including TimelyMon, VeriMon, and WhyMon, are practical outcomes of his research, enabling scalable, explainable, and trustworthy runtime verification. He leads a research group focused on trustworthy stream processing, distributed streaming computations, and explainable monitoring. His work often involves collaboration with researchers at ETH Zürich and other institutions, particularly in the areas of security and monitoring.

Igor Walukiewiczمشاهده پروفایل

پژوهشگر

• Concurrency Theory
• Model Checking
• Timed Automata
• +۷ مورد دیگر

Igor Walukiewicz is a Researcher at the Laboratoire Bordelais de Recherche en Informatique (LaBRI) , affiliated with Université de Bordeaux , France. His work focuses on Concurrency Theory , Model Checking , Timed Automata , Higher-Order Model Checking , and Automata Theory . His recent research explores parametric systems , timed automata , and higher-order concurrency . Articles highlight advancements in verification techniques , synthesis of distributed algorithms , and partial-order reduction methods . Key subfields include deadlock avoidance , active learning , and logical frameworks for timed systems . He has secured significant ANR grants such as FREDDA (FoRmal Methods for Distributed Algorithms) and Ticktac (Verification of Real-Time Systems). He contributes to tools like TChecker , a model-checking tool for real-timed systems developed at LaBRI. Walukiewicz participates in editorial and organizational roles, including the Fundamenta Informaticae editorial board and HIGHLIGHTS conference steering committee. He has presented at major venues like LICS , CONCUR , and ICALP .

Amrita Sureshمشاهده پروفایل

عضو هیئت علمی

• Formal Verification
• Automata Theory
• Temporal Logics
• +۴ مورد دیگر

Amrita Suresh is a Research Associate in the Department of Computer Science at the University of Oxford, working under Professor Nobuko Yoshida. She specializes in formal verification, focusing on communicating automata and session types. Previously, she completed her PhD at ENS Paris-Saclay under advisors Alain Finkel and Benedikt Bollig, with research on subclasses of communicating automata and decidability in verification. PhD in Computer Science (ENS Paris-Saclay) MSc in Computer Science (ENS Paris-Saclay) BE in Computer Science (BITS Pilani) Her research interests span formal verification, automata theory, temporal logics, and distributed systems. She has contributed to foundational work on input-bounded FIFO systems, synchronizability via Message Sequence Charts, and extensions of Well-Structured Transition Systems. Her publications highlight advancements in decidability of reachability problems and frameworks for synchronizability. Awards include the Best Teaser Talk Award at CONCUR’21 and Best Paper Award at CONCUR’20. Amrita has taught courses in Systems and Architecture, Programming I (undergraduate), and Tree Automata and Their Applications. She actively participates in academic events, including serving on program committees for conferences like ICE’22 and as Technical Chair for QONFEST’21. She is affiliated with Nobuko Yoshida’s research group and collaborates on theoretical computer science challenges, particularly in formal methods for distributed systems.

Emanuele D'Osualdoمشاهده پروفایل

استاد

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

Emanuele D'Osualdo is a Tenure-Track Professor of Formal Methods for Software Engineering at the University of Konstanz, Department of Computer and Information Science. Previously, he was a Postdoctoral Researcher at Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken until April 2024, working with Derek Dreyer on verification of concurrent software. Before that, until September 2020, he was a Marie Curie Fellow at Imperial College London, working with Prof. P. Gardner. From 2015 to 2017, he was a PostDoc in the Concurrency Theory Group at the University of Kaiserslautern, working with Prof. Roland Meyer. His educational background includes: PhD (DPhil) in Computer Science from the University of Oxford (2015), supervised by Prof. C.-H. Luke Ong Undergraduate and master's studies at the University of Udine, Italy, graduating with honors and supported by the Scuola Superiore scholarship Emanuele D'Osualdo's research focuses on Formal Methods for the verification of software, with particular emphasis on two main approaches: automatic verification methods using static analysis and infinite-state model checking; and compositional methods, focusing on program logics for properties beyond safety. His work spans several areas including Programming Languages, Verification, Security, Concurrency Theory, Probabilistic Programs, Types, Static Analysis, Process Algebra, and Model Checking. His research has led to the development of tools such as Soter for automatic safety verification of Erlang programs and James Bound for analyzing π-calculus. His recent publications demonstrate a strong focus on advanced verification techniques for concurrent and distributed systems, with particular attention to linearizability, session types, security protocols, and probabilistic reasoning. His work bridges theoretical foundations with practical applications in software verification, showing a progression from foundational work on π-calculus to more applied verification of concurrent data structures and probabilistic systems. He has received notable recognition for his work, including: Winner of the 2016 CPHC/BCS Distinguished Dissertation award Marie Curie Fellow Emanuele actively supervises students and leads research in formal methods. He is involved in several research projects related to software verification and has presented his work at top-tier conferences including POPL, OOPSLA, ESOP, and CAV. He is scheduled to give a keynote at HYPER'25 in Zagreb and will be attending POPL'25. His research group appears to focus on developing theoretically sound yet practical verification techniques for modern concurrent and distributed software systems.

Sagiv Shmuelمشاهده پروفایل

استاد

• Software verification
• Shape analysis
• Smart contracts
• +۷ مورد دیگر

Prof. Sagiv Shmuel is a Full Professor at Tel-Aviv University's Department of Computer Science. He has held various academic roles, including Associate Professor (2004–2005), Senior Lecturer (2000–2004), and visiting positions at institutions such as the University of Chicago and University of Copenhagen. His research focuses on software verification, shape analysis, smart contracts, and programming languages. Education: Ph.D. in Computer Science, Technion (1986–1990) B.A. in Computer Science, Technion (1982–1985), cum laude Research Interests: His work addresses challenges in static analysis, formal verification, and program analysis. Notable areas include invariant inference, smart contract security, and parametric shape analysis. These contributions have led to practical tools like Ivy and the foundation of Certora, a company specializing in smart contract verification. Awards: ACM Fellow (2016) Friedrich Wilhelm Bessel Research Award (2002) Microsoft Outstanding Collaborator Award (2016) Grants & Leadership: Principal Investigator (PI) of a Senior ERC Grant (1.57M Euros) for software composition verification Editor of Foundations and Trends in Programming Languages Chair of program committees for POPL, SAS, and other leading conferences His research has been applied to real-world systems, such as improving the Java concurrent library and ensuring kernel extension security in Linux.

Dimirovski Georgiمشاهده پروفایل

استاد

• Control Systems
• Neural Networks
• Cyber-Physical Systems
• +۷ مورد دیگر

Dimirovski Georgi is a Professor at the Department of Control and Systems Engineering, Faculty of Electrical Engineering and Information Technologies, Ss. Cyril and Methodius University of Skopje. His research focuses on advanced control systems, neural networks, cyber-physical systems, and computational cybernetics. He has extensively contributed to theoretical and applied aspects of switched systems, nonlinear control, fault-tolerant mechanisms, and networked control systems. His work integrates methodologies such as Lyapunov theory, adaptive control, and reinforcement learning to address complex challenges in robotics, aerospace, and industrial automation. Recent studies emphasize resilient control under adversarial attacks, optimal resource allocation, and synchronization of dynamic systems. Key research trends include: (1) developing robust control strategies for systems with time-delays and uncertainties, (2) enhancing cybersecurity in cyber-physical systems through deception attack detection and mitigation, and (3) advancing machine learning techniques for real-time system estimation and prediction. Dimirovski has published over 200 peer-reviewed articles, with recent contributions appearing in top journals and conferences. His work frequently explores intersections between control theory and artificial intelligence, particularly in applications requiring safety-critical performance guarantees.

• Type 1 Diabetes Management
• Pediatric Endocrinology
• Diabetes Technology
• +۳ مورد دیگر

Craig Taplin is a Clinical Associate Professor at the UWA Medical School, affiliated with the UWA Centre for Child Health Research and The Kids Research Institute Australia. His work focuses on pediatric diabetes management, diabetes technology, and public health. He is reachable at craig.taplin@uwa.edu.au via phone 64565897. Research Interests: Dr. Taplin’s expertise includes Type 1 Diabetes Management, Pediatric Endocrinology, and Diabetes Technology. His studies explore advanced therapies like hybrid closed-loop systems, socioeconomic impacts on glycemic outcomes, and regulatory standards for medical devices. He also investigates physical activity’s role in youth diabetes care and insulin pump accessibility. Grant Activity: He is an Investigator on a Stan Perron Charitable Foundation-funded project (2023-2025) developing an integrated diabetes data management platform to benefit patients, families, and clinicians.

• Programming Languages
• Information Security
• Software Security
• +۱۲ مورد دیگر

Dr Yi Lu is a Senior Lecturer at the Queensland University of Technology (QUT), Faculty of Science, School of Computer Science. He serves as Deputy Academic Lead (HDR) for the School of Computer Science, contributing to higher degree research leadership. His academic journey includes a PhD in Computer Science from the University of New South Wales (2008) and prior roles as a Lecturer at UNSW (2007–2013) and Principal Researcher at Oracle Labs (2013–2019). PhD in Computer Science, University of New South Wales, 2008 Bachelor of Information Technology (Honours), Queensland University of Technology, 2002 Dr Lu's research lies at the intersection of programming languages and information security, with a focus on theoretical and practical aspects of software security. His work includes type systems for object synchronization, ownership types, information flow control, and the application of deep learning to vulnerability detection. He has made significant contributions to static analysis, points-to analysis, and secure multithreaded programming. His recent publications span topics such as threat hunting in industrial control systems, nontransitive security types, and multi-class vulnerability prediction using graph neural networks. These works reflect a strong trend toward combining formal methods with machine learning to enhance software security, particularly in complex and critical systems. Dr Lu has been involved in significant research initiatives, including the Cyber Security Cooperative Research Centre and the ARC Linkage Project on Java language-based security conformance. His industry experience at Oracle Labs led to patented solutions for real-world cybersecurity problems, demonstrating the practical impact of his research. He supervises research projects on fine-grained vulnerability detection, reproducible deep learning workflows, and open-source supply chain analysis. His teaching includes courses such as Principles of Software Security and Object-Oriented Design, aligning closely with his research expertise. Dr Lu is affiliated with the School of Computer Science at QUT, a research-active unit within the Faculty of Science, contributing to cybersecurity education and innovation in Australia.

• Term Rewriting Systems
• Tree Languages
• XML Schema Evolution
• +۴ مورد دیگر

Pierre RETY serves as a Lecturer with HDR (Habilitation à Diriger des Recherches) at the University of Orleans, France, affiliated with the Laboratoire d'Informatique Fondamentale d'Orléans (LIFO). His academic position grants him the qualification to supervise doctoral research within the French higher education system. LIFO operates within the university's Faculty of Sciences, focusing on fundamental computer science research. RETY's research spans theoretical computer science with significant contributions to term rewriting systems and tree languages, later expanding into XML schema evolution and data management applications. His work demonstrates a progression from foundational theoretical frameworks to practical implementations in data systems. Key research themes include prefix-constrained rewrite systems, synchronized tree languages, and conservative XML schema evolution techniques. His methodological approach combines formal language theory with practical applications in data representation and transformation. Analysis of his publication timeline reveals a strategic research trajectory: early work (1996-2006) concentrated on term rewriting theory and tree automata, while later research (2007-2022) increasingly addressed XML data management challenges. This evolution reflects both the maturation of XML as a data standard and RETY's ability to adapt theoretical frameworks to emerging practical needs. His publications consistently appear in international peer-reviewed venues, demonstrating sustained scholarly contribution over 26 years. RETY maintains active research collaborations, most notably with Jacques Chabin, Yohan Boichut, and Nirina Andrianarivelo across multiple publications. His work at LIFO positions him within France's national computer science research ecosystem, contributing to theoretical foundations while addressing real-world data management challenges.

Yingfei Xiongمشاهده پروفایل

دانشیار

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

Yingfei Xiong is an Associate Professor at Peking University specializing in Software Engineering and Programming Languages. His research focuses on program synthesis, automated program repair, and software analysis techniques with extensive contributions to top-tier conferences including ASE, ICSE, PLDI, and SPLASH/OOPSLA. Dr. Xiong's primary research interests include: Program Synthesis and Inductive Programming Automated Program Repair and Bug Fixing Static and Dynamic Program Analysis Machine Learning Applications in Software Engineering Compiler and Language Implementation Techniques Software Testing and Verification His publication trends show a strong shift toward neural approaches in program repair, with significant integration of large language models in synthesis tasks since 2023. His work bridges theoretical foundations with practical applications, evidenced by industrial collaborations such as the Alibaba case study on static taint analysis. Recent contributions include GrammarT5 for code generation, Tare for type-aware neural repair, and Equality Saturation techniques guided by LLMs. At Peking University, Dr. Xiong is affiliated with the School of Electronics Engineering and Computer Science (SEI) as indicated by his institutional website domain. He actively contributes to the academic community through program committee service for major software engineering conferences and mentoring student researchers.

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

Alexander J. Summers is an Associate Professor and Associate Head of Graduate Affairs in the Department of Computer Science at the University of British Columbia (UBC), where he joined in 2020. Prior to UBC, he was a senior researcher (Oberassistent) at ETH Zurich. His research focuses on program correctness, including specification and verification logics, type systems, and automated tools for deductive verification. He leads the Prusti Project, developing verification tools for the Rust programming language, and collaborates on the Viper Project, an intermediate verification language framework. Summers is also actively involved in teaching, offering courses on advanced software engineering and program verifiers. His research interests span formal methods, programming languages, and automated reasoning, with a particular emphasis on Rust and ownership-based systems. He has contributed to the development of verification tools like Viper and Prusti, which aim to enhance software reliability through deductive techniques. Summers has been recognized with awards such as the Distinguished Reviewer Award (ACM SIGPLAN) and the Amazon Research Award. Summers has published extensively in top venues like POPL, PLDI, and OOPSLA, with recent work addressing challenges in Rust's ownership model, formal verification frameworks, and automated reasoning techniques. His lab focuses on advancing the state of the art in program verification while maintaining strong ties to practical tool development and empirical studies of programming practices. He actively mentors students at UBC, including PhD and M.Sc. candidates, and has supervised postdoctoral researchers. Summers is also engaged in academic service, serving on program committees for conferences like OOPSLA and IJCAR, and contributes to the broader formal methods community through tool development and educational initiatives.

• Deep Learning
• Artificial Intelligence
• Computer Vision
• +۱۵ مورد دیگر

Hamit Erdem is a Professor at Baskent University 's Electrical and Electronics Engineering Program. His research spans Deep Learning , Artificial Intelligence , and Computer Vision , with recent work focusing on Visual Speech Recognition and Fuzzy Control for robotics. Notable Fields: Deep Learning, Power Electronics, Harmonic Analysis, and TinyML His publications highlight trends in applying Neural Networks to Turkish lip reading (2024), Optimization Algorithms for power converters (2017), and Fuzzy Control for Sumo robots (2007-2012). He has contributed to Signal Processing and Sensor Calibration via low-cost microcontroller implementations (2010). Hamit Erdem has supervised multiple students, including Sahin Burak Dalkilic , Yağmur Yarımbıyık , and Talya Tumer Sıvr , in theses on topics ranging from TinyML-based keyword detection to Deep Learning for Nail Type Recommendation . He is reachable via email at herdem@baskent.edu.tr .

Oliver Bračevacمشاهده پروفایل

پژوهشگر

• Functional Language Compilers
• Dependent Types
• Effect Systems
• +۶ مورد دیگر

Oliver Bračevac is a researcher affiliated with Purdue University in the United States and EPFL (École Polytechnique Fédérale de Lausanne) in Switzerland, where he is part of the LAMP (Programming Methods Laboratory) group. His work focuses on advanced type systems and functional language compilation, particularly in the context of Scala 3 . His research interests include functional language compilers , dependent types , effect systems , capture types , co-effects , separation logic , and ownership . He has made significant contributions to the development of reachability types and their integration into practical programming languages. He has published extensively in top-tier conferences such as ECOOP , POPL , OOPSLA , ICFP , and SPLASH , focusing on type safety, compiler optimizations, and formal verification. His recent work includes modeling reachability types with logical relations and developing ergonomic capture tracking systems for generic data structures in Scala 3. Oliver serves on numerous program committees and artifact evaluation committees, including roles at OOPSLA 2025 , POPL 2025 , SPLASH 2024 , and ECOOP 2022 . He is actively involved in organizing workshops such as The Scala Workshop 2025 . He maintains a personal website at https://bracevac.org and is active on GitHub under the username bracevac .