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

Mark Battyمشاهده پروفایل

استاد

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

Mark Batty is a Professor in the School of Computing at the University of Kent, specializing in formal methods for concurrent systems. His work bridges hardware-software interfaces, focusing on memory models for C/C++, OpenCL, and architectures including x86, ARM, POWER, and GPUs. As a member of the Programming Languages and Systems Research Group, he develops mathematical specifications and verification tools for real-world concurrency challenges. His research centers on empirical testing of hardware/compiler behavior, formal modeling of system components, and verification of fine-grained concurrent algorithms. Key contributions address relaxed memory semantics, transactional memory, and compositional reasoning for concurrent data structures. His work combines theoretical rigor with practical tool development to ensure correctness in complex concurrent environments. Analysis of his 2015-2025 publications reveals consistent focus on memory consistency models, formal verification of weak memory concurrency, and compiler optimizations. Dominant themes include C/C++11 standards, GPU concurrency semantics, and mechanized verification techniques. His research demonstrates strong industry relevance through collaborations with hardware vendors and contributions to language standards. Mark Batty has received significant recognition: John C. Reynolds Doctoral Dissertation Award (2015) from ACM SIGPLAN CPHC and BCS Distinguished Dissertation Award (2015) Lloyds Register Foundation and Royal Academy of Engineering Research Fellowship (2016) He actively leads major research initiatives and mentors next-generation researchers: Current Funding: EPSRC Standard Grant 'Verifiably Correct transactional memory' (2018), VeTTS Grant 'Specification and verification of C++ data structure libraries' (2018), EPSRC First Grant 'Compositional, dependency-aware C++ concurrency' (2018) PhD Recruitment: Actively seeking candidates for UKRI-funded studentship in Verified Trustworthy Software Systems Batty drives community engagement through Kent Concurrency Workshop (2016) and South of England Programming Language Seminars, fostering national collaboration in programming languages research. His leadership in organizing Royal Society discussions underscores his influence in trustworthy systems verification.

Peter Sewellمشاهده پروفایل

استاد

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

Peter Sewell is Professor of Computer Science at the University of Cambridge Computer Laboratory, where he builds rigorous foundations for real-world computer systems to enhance robustness, security, and formal verification of hardware-software interactions. His educational background includes undergraduate studies at the University of Cambridge and University of Oxford, followed by a PhD from the University of Edinburgh in 1995 under Robin Milner's supervision. Professor Sewell's research focuses on concurrency models (x86, ARM, Power, C/C++11), verified compilation, formal semantics for C/linking/filesystems/TLS, and applied semantics tools. He pioneers executable ISA specifications through projects like Sail and Cerberus, addressing relaxed-memory concurrency and capability-based security architectures. His 2020-2026 publications reveal a clear trajectory toward formal verification of hardware security properties, with increasing emphasis on capability systems (Arm Morello, CHERI) and real-world applicability of concurrency models across ARM, RISC-V, and MIPS architectures. Scientific recognition: Royal Society University Research Fellowship (1999-2007) He leads major research initiatives in systems security formalization, supported by Cambridge positions and collaborative projects with industry partners. His work bridges theoretical formal methods and practical systems engineering through executable semantics frameworks. As a core member of Cambridge's Systems Research Group, he directs projects including Sail (ISA semantics), Cerberus (C semantics), and verification frameworks for capability architectures, fostering interdisciplinary collaboration across hardware and software security domains.

Hamed Nematiمشاهده پروفایل

استادیار

• Security of systems software
• Formal methods and program logics
• Interactive theorem proving
• +۲ مورد دیگر

Hamed Nemati is an Assistant Professor at the Division of Network and Systems Engineering under the School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology in Stockholm, Sweden. He was previously a Visiting Assistant Professor at Stanford University and a Research Group Leader at the Helmholtz Center for Information Security (CISPA) , where he also worked as a PostDoc and Research Fellow. Education : PhD in Computer Science from KTH Royal Institute of Technology Research Interests : Security of systems software, formal methods and program logics, interactive theorem proving, machine code analysis, applied machine learning Current Projects : Systematic verification of multi-language security protocols, hardware-software co-design for Spectre mitigation, capability-based access control models Scientific Awards : WASP (Wallenberg AI, Autonomous Systems and Software Program) faculty member Teaching Activities : Formal Methods in Security (Fall 2020-2023) at CISPA/Saarland University Digital Forensics and Incident Response (EP2780) (Fall 2024) at KTH

Simone Aonzoمشاهده پروفایل

مدرس

• Cybersecurity
• Malware Analysis
• Android Security
• +۵ مورد دیگر

Simone Aonzo is a Class 2 Lecturer in the Digital Security department at EURECOM, a leading research and education institution in France focused on digital sciences. He is actively engaged in cybersecurity research with a strong emphasis on malware analysis, Android security, and machine learning applications in threat detection. His research interests span several critical areas in modern cybersecurity, including: Android and Windows malware analysis Evasive techniques used by malware Machine learning vulnerabilities in security systems Binary analysis and cryptographic function detection Phishing and social engineering attacks Security hardening using AI The trends in his recent publications (2024–2025) reflect a deep focus on adversarial machine learning, evasive malware behaviors, and the application of AI in both offensive and defensive security contexts. His work frequently appears in top security venues such as RAID, NDSS workshops, and IEEE-affiliated conferences, demonstrating his active contribution to the research community. He has no listed scientific awards in the provided text. Simone Aonzo is involved in mentoring and training through academic collaborations and educational events such as the PEPR Cybersecurity Winter School. While specific advisees are not listed, his collaborative publications suggest an active role in guiding junior researchers. There is no mention of grants, but his publication output implies ongoing research funding. He also contributes to community knowledge through talks and workshops. He is associated with the Digital Security research group at EURECOM, which focuses on cutting-edge cybersecurity challenges, including malware analysis, privacy, and system security. The team employs advanced techniques in machine learning, reverse engineering, and automated analysis to study modern threats.

• Computer Architecture
• Parallel Computing
• Compiler Technology
• +۳ مورد دیگر

Keiji Kimura is a Professor in the Department of Computer Science and Engineering at Waseda University's Faculty of Science and Engineering, School of Fundamental Science and Engineering. He earned his Doctor of Engineering from Waseda University and has held academic positions at the university since 1999, progressing from Research Associate to Assistant Professor (2004-2005), Associate Professor (2005-2012), and Professor (2012-present). He is affiliated with multiple professional organizations including ACM, IEEE Computer Society, The Institute of Electronics, Information and Communication Engineers, and Information Processing Society of Japan. His research focuses on computer architecture, particularly parallel computing systems and compiler technology. Kimura has made significant contributions to the development of the OSCAR (Optimally Scheduled Advanced Multiprocessor) automatic parallelizing compiler framework. His work spans multiple areas including multicore processor architecture, power reduction techniques for embedded systems, non-volatile memory systems, and parallelization methods for heterogeneous architectures. His research interests specifically include Multiprocessor Architecture and Parallelizing Compiler development, with applications in real-time systems and energy-efficient computing. Analysis of his recent publications reveals a strong focus on practical implementations of parallel computing technologies across diverse hardware platforms including RISC-V, ARM, and heterogeneous multicore systems. His work demonstrates a consistent trajectory from theoretical compiler development toward practical applications in embedded systems, security, and non-volatile memory technologies. The publications show increasing emphasis on RISC-V architecture, persistent memory programming, and power-efficient computing solutions. MEXT Award for Science and Technology (Research category), 2014.04 Ministry of Education, Culture, Sports, Science and Technology (MEXT) Kimura has served on numerous prestigious conference program committees including PACT, IPDPS, HPCA, and LCPC. His research has been supported through collaborations with major technology companies and government initiatives such as the METI/NEDO project entitled "Multicore Technology for Realtime Consumer Electronics." His work with the OSCAR compiler framework has demonstrated significant performance improvements and power reductions in real-world applications. He leads research in the APAL laboratory (http://www.apal.cs.waseda.ac.jp/) at Waseda University, focusing on advanced parallel processing technologies. His team works on compiler-directed approaches to solve challenges in heterogeneous multicore architectures, with particular emphasis on making parallel programming more accessible while optimizing for both performance and power efficiency. Current research directions include RISC-V secure boot verification, non-volatile memory systems, and GPU-based persistent memory solutions.

Vasilios Kelefourasمشاهده پروفایل

مدرس

• Compiler Optimizations
• Deep Neural Networks
• Matrix/Tensor Computations
• +۲ مورد دیگر

Dr. Vasilios Kelefouras is Lecturer in Computer Science at the University of Plymouth's School of Engineering, Computing and Mathematics. His research optimizes software applications for execution time, energy consumption, and memory footprint across CPUs, GPUs and FPGAs. Notable contributions include analytical methodologies accelerating convolution layers in Deep Neural Networks (x1.1-7.2 speedup over Intel oneDNN) and optimization techniques for image processing algorithms (x2.8-40 speedup over Intel IPP). His compression work for Deep Neural Networks includes Tensor Train Decomposition methodologies for edge devices. Honors include HiPEAC Technology Transfer Award (2022) and Best Paper at SAMOS XXII. Teaches Parallel Computing, Computer Systems, and Computing Practice. Current PhD supervision focuses on accelerating ML algorithms on heterogeneous architectures.

• 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.

• Programming Languages
• Refactoring
• Parallel Programming
• +۱۲ مورد دیگر

Christopher Brown is a Lecturer in the School of Computer Science at the University of St Andrews, where he conducts research in programming languages, refactoring, parallel programming, and energy-efficient computing. He is a member of the Programming Languages research group and leads the EPSRC-funded Energise project, focused on energy-aware refactorings for embedded systems. Previously, he led the EU Horizon 2020 TeamPlay project, addressing time, energy, and security in parallel software. Research Interests: Programming Languages: semantics, compilers, static analysis Refactoring: sequential to parallel transformation, correctness verification Parallel and Concurrent Programming: tools, skeletons, GPUs, multi-core systems Energy Optimization: compiler and refactoring techniques for low-energy software Verification: dependent types, formal soundness, non-functional properties The recent publications reflect a strong focus on dependently-typed parallel languages, algorithmic skeletons, and specification-guided refactoring, with applications in energy efficiency and safety. His work bridges theoretical foundations with practical tool development, including open-source systems like Skel and ParaFormance. Scientific Awards: No scientific awards explicitly mentioned in the provided text. Advising and Grants: Supervision: Accepting postgraduate research students; no named students listed. Grants: Principal Investigator on two major projects: Energise (EPSRC): Refactorings and skeletons for energy-aware embedded systems (2021–2024) TeamPlay (EU Horizon 2020): Time, energy, and security analysis for heterogeneous platforms (2018–2021) Labs and Teams: Member of the Programming Languages group at the University of St Andrews. Actively involved in developing open-source tools such as Skel (Erlang parallel library) and ParaFormance (C/C++ refactoring suite), and contributes to collaborative research in parallelism and verification.

• Computer Science Education
• Parallel Programming
• Computer Architecture
• +۳ مورد دیگر

Saturnino Garcia, PhD, is an Associate Professor of Computer Science at the University of San Diego (USD) since 2012. He holds a PhD from the University of California, San Diego. His research focuses on programming systems, parallel programming, computer architecture, and innovative pedagogical methods in computer science education, particularly active learning strategies such as peer instruction and Process Oriented Guided Inquiry Learning (POGIL). He has contributed to integrating social justice topics into introductory computer science courses (CS1) and improving student preparedness through guided practice. Education: PhD in Computer Science, University of California, San Diego (2012). Research interests include: Design and implementation of active learning methodologies in systems courses Development of student-centered learning tools like the x86-64 simulator Parallel programming and architecture optimization (e.g., Kremlin oracle, Kismet speedup estimation) Educational equity through curriculum reform in CS1 Publications emphasize pedagogical innovations and parallel computing advancements. Notable works include studies on POGIL frameworks in CS classrooms and benchmark suites like CortexSuite. No scientific awards explicitly listed. Advising/Grants: No specific students or grants mentioned. Active in curriculum development and educational research initiatives. Labs/Teams: No lab affiliations explicitly noted, but collaborates with institutions on educational and technical projects.

Andreas Gerstlauerمشاهده پروفایل

استاد

• Embedded Systems
• Cyber-Physical Systems
• Internet of Things
• +۷ مورد دیگر

Andreas Gerstlauer is a Professor and holder of the Cullen Trust for Higher Education Endowed Professorship in Engineering #6 at The University of Texas at Austin. He serves as the Associate Chair for Academic Affairs in the Chandra Family Department of Electrical and Computer Engineering. His academic appointments include membership in the Architecture, Computer Systems, and Embedded Systems (ACSES) research area and the Integrated Circuits & Systems (ICS) research area. Dr. Gerstlauer received his Dipl.-Ing. (M.S.) degree in Electrical Engineering from the University of Stuttgart, Germany in 1997 and M.S. and Ph.D. degrees in Information and Computer Science from the University of California, Irvine in 1998 and 2004, respectively. Prior to joining UT Austin in 2008, he was an Assistant Researcher in the Center for Embedded Computer Systems (CECS) at UC Irvine. His research focuses on embedded systems, cyber-physical systems, and the Internet of Things, with particular emphasis on electronic system-level design methods, system modeling, design languages, and embedded hardware/software synthesis. His work spans from novel hardware/software fabrics and System-on-Chip architectures to system-level design automation methods and tools, with special emphasis on underlying system modeling foundations. His research group, the System-Level Architecture and Modeling (SLAM) Lab, investigates resource-constrained and application-specific embedded, high-performance, and edge computing systems. Dr. Gerstlauer's publication record shows a consistent trajectory in advancing system-level design methodologies, with recent work focusing on IoT applications, deep learning inference at the edge, power modeling using machine learning techniques, and advanced simulation frameworks for heterogeneous architectures. His research bridges the gap between theoretical design methodologies and practical implementation, with commercial applications used by organizations including JAXA and NEC Toshiba Space Systems. Humboldt Research Fellowship (2016-2017) Best Research Paper Award at DAC (2016) Best Paper Award at SAMOS (2015) Outstanding Paper Award at ECRTS (2023) IEEE HSTTC Top Pick in Hardware Security (2021) Best Paper Award at MLCAD (2021) Dr. Gerstlauer has successfully mentored numerous Ph.D. and Master's students who have gone on to prominent positions at companies including Google, NVIDIA, Apple, AMD, Facebook, Intel, and Samsung. His research has been supported by major funding agencies including NSF, DOE, SRC, Sandia National Labs, and industry partners such as AMD, ARM, Intel, Qualcomm, and Samsung. He has served in leadership roles for major conferences including General Co-Chair for ESWEEK 2020-2021 and Program Committee Chair for CODES+ISSS 2015-2016. The SLAM Lab, under his direction, currently pursues active research in neuromorphic computing system co-design, accelerator-rich heterogeneous system architectures, and predictive modeling for next-generation heterogeneous computer system design. The lab maintains strong industry partnerships and has produced multiple open-source software tools including QLA-RTS, DeepThings, LIPPo, and NoSSim that have been adopted by both academic and industrial researchers.

• Computer Architecture
• Parallel Processing
• Multi-core Programming
• +۴ مورد دیگر

Professor Lasse Natvig is a faculty member at the Norwegian University of Science and Technology (NTNU) in the Faculty of Information Technology and Electrical Engineering , specifically the Department of Computer Science . His research focuses on computer architecture , parallel processing , multi-core programming , and energy-efficient computing . His work includes studying vectorization techniques , cache management , power emulation models , and task scheduling policies to improve performance and energy efficiency in modern processors. He has published extensively in journals like Expert Systems With Applications , The Journal of Supercomputing , and Lecture Notes in Computer Science , with recent 2024 work on micromobility simulation tools. Lasse Natvig's research spans computer architecture , green computing , parallel algorithms , and energy measurement through publications addressing vectorization , cache optimization , and heterogeneous processing . His articles reveal a consistent focus on performance-energy tradeoffs , hardware-software co-design , and simulation tools for computational challenges. Email: lasse.natvig@ntnu.no

Warren Hunt Jr.مشاهده پروفایل

استاد

• Formal Methods
• Computer Architecture
• Hardware Verification
• +۶ مورد دیگر

Warren A. Hunt, Jr. is a Professor at the The University of Texas at Austin in the Department of Computer Sciences . He specializes in formal methods , computer architecture , and computational biology , with a focus on X86 specification in ACL2 , RSFQ computing , and biological-inspired computing . 25+ years in hardware verification First mechanical verification of a microprocessor (1985) Associate Editor, Formal Methods in System Design journal Research Interests include formal specification, program verification, automated theorem-proving, and computational biology tools. His work spans microprocessor design validation , symbolic simulation , and linear/nonlinear arithmetic in ACL2 . Scientific Awards : ACM 2015 Distinguished Engineer Advising : Supervises current PhD students Gavin Meil and Balasubraman Muthuveli . Has advised 12 PhD graduates, including Sol Swords (Intel) and Serita Nelesen (co-advised with Tandy Warnow). Grants & Collaborations : Leads NSF-funded projects like TC: Small (memory analysis) and TWC: Large (internet routing). Collaborates with ARM Corporation , Intel , and Centaur Technology . Labs & Conferences : Active in the ACL2 theorem proving community , served as FMCAD Steering Committee Chair (1996-2020), and co-organized FMCAD 2000 .

Warren A. Hunt, Jr.مشاهده پروفایل

استاد

• Formal Methods
• Computer Architecture
• Low-Power Computing
• +۷ مورد دیگر

Warren A. Hunt, Jr. is a Professor in the Department of Computer Sciences at The University of Texas at Austin. His research focuses on formal methods for hardware and software verification, computer architecture, low-power computing, and biological-inspired systems. He leads projects in specifying and validating computer memory models, extending the ACL2-based x86 specification, and exploring rapid single-flux quantum (RSFQ) computing. Research Interests Formal specification and verification of hardware/software systems Computer architecture and low-power design Biological-inspired computing ACL2 theorem prover applications X86 ISA modeling Notable Contributions Verification of complex microprocessor designs Development of formal tools for hardware/software co-verification Leadership in the FMCAD conference (chairman until 2020) Academic Collaborations Work with Centaur Technology on x86 processors Collaborations with industry partners (Intel, AMD, ARM) Keynote talks at international venues (Newton Institute, Royal Society) Publications (2017–2025) span formal verification of multipliers, self-timed circuits, RSFQ systems, and x86 machine-code analysis. His Google Scholar page lists all his work. PhD Students Current: Balasubraman Muthuvelu, Gavin Meil, Carl Kwan Graduates: Jun Sawada (1999), Sol Swords (2010), Shilpi Goel (2016), and others Leadership Chairman of FMCAD steering committee (1996–2020) Editorial roles in multiple FMCAD/CHARME conferences

• Distributed computing
• Systems software
• Information systems
• +۶ مورد دیگر

Jade Alglave is a Professor of Computer Science at University College London, working within the Department of Computer Science. She is affiliated with the PPLV research group led by Peter O'Hearn, focusing on foundational aspects of programming languages and verification. Her work bridges the gap between theoretical computer science and practical systems implementation, particularly in the domain of memory models and concurrency. Alglave's research spans distributed computing, systems software, information systems, theory of computation, and software engineering, with a particular emphasis on weak memory models and concurrent systems . Her work develops formal methods for specifying, verifying, and testing memory models across various hardware architectures including ARM, POWER, and x86. She has made significant contributions to understanding the formal semantics of concurrent programming and has developed tools like the diy7 suite for generating and analyzing litmus tests that expose subtle concurrency behaviors. Her publications reveal a consistent research trajectory focused on creating rigorous formal frameworks for understanding weak memory behaviors, with applications to hardware verification, compiler design, and operating system development. The work has significant implications for ensuring correctness in concurrent and parallel systems where memory consistency is critical. Alglave actively contributes to the research community through professional activities including serving as a conference referee for major venues, participating in the ERC member DAC, reviewing for journals like TOPLAS, serving on program committees for JFLA and PLDI, and organizing workshops like CAV.

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

دانشیار

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

Dr. Azalea Raad is an Associate Professor (Reader) in the Department of Computing at Imperial College London, leading the Veritas Lab. She is also co-director of the UK Research Institute on Verified, Trustworthy Software Systems (VeTSS). Her research focuses on programming languages, formal verification, and weak memory models, with contributions to persistent memory technology and concurrency. Raad has held visiting roles at Facebook and Bloomberg, and has been recognized with awards such as the UKRI Future Leaders Fellowship and the SIGPLAN Distinguished Paper Award. Her work bridges theoretical foundations with practical tools for ensuring software correctness. Education & Roles: PhD (Imperial College London, 2016) Reader/Associate Professor (Imperial College London, 2021–present) Co-Director, UK VeTSS Institute (2023–present) Research Interests: Her research explores formal methods for persistent programming, including non-volatile memory semantics, weak memory models, and concurrency. She develops tools like Incorrectness Separation Logic and frameworks for verifying binaries (e.g., IsaBIL). Her work emphasizes practical applications in industrial settings, such as Intel PMDK transactions and RDMA robustness. Grants & Awards: EPSRC Research Grant: Safe and Secure Remote Direct Memory Access (2023) UKRI Future Leaders Fellowship (2021) Meta Research Gift (2022) Imperial College President’s Award (2021) Professional Activities: Program Committee Member: ESOP (2024), CAV (2022), ICFP (2022) Keynote Speaker: MFPS (2022), PLDI (2021) Labs & Teams: Leads the Veritas Lab, focusing on verified software systems, and collaborates with industry partners like Intel and Bloomberg through applied research initiatives.