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

• Operating Systems
• Real-Time Systems
• Security
• +۴ مورد دیگر

Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at the University of New South Wales (UNSW) in Sydney, Australia, leading the Trustworthy Systems research group focused on mathematically proven secure systems development. His research centers on operating systems, real-time systems, security, and safety through formal verification methodologies, pioneering the world's first fully verified general-purpose microkernel (seL4) with machine-checked proofs of implementation correctness, timeliness, and security enforcement. This work bridges theoretical formal methods with practical system security for critical infrastructure. Professor Heiser's accolades include: ACM Fellow for contributions to high-assurance systems IEEE Fellow for leadership in secure operating systems ATSE Fellow for technology and engineering excellence 2019 ACM SIGOPS Hall of Fame Award for the seL4 microkernel breakthrough He maintains significant industry impact through co-founding Open Kernel Labs (acquired by General Dynamics in 2012), whose OKL4 Microkernel shipped in billions of mobile chips and iOS secure enclaves. Current roles include Chief Scientist at HENSOLDT Cyber (Munich) and Chief Scientific Officer at Neutrality (Geneva), while founding chairman of the seL4 Foundation drives ecosystem development for security-critical deployments. Leading UNSW's Trustworthy Systems group, he champions rigorous research quality over publication quantity, producing high-impact work averaging 100+ citations per paper within five years, and frequently mentors junior researchers on achieving academic excellence through methodological precision.

• Embedded Systems
• Formal Verification
• Synchronous Languages
• +۱ مورد دیگر

Timothy Bourke holds dual appointments as a Researcher at Inria (PARKAS team) and Adjunct Professor at École polytechnique's Informatics Department. His research develops rigorous methods for modeling, programming, and verifying embedded control systems, with applications ranging from medical devices to wireless protocols. Dr. Bourke employs synchronous languages and interactive theorem provers to create practical verification approaches. His team has worked on projects involving robotic wheelchairs, microkernel operating systems, and wireless routing protocols. Current research focuses on bridging theoretical frameworks with real-world embedded system challenges. As an active member of the programming languages community, he serves on program committees for leading conferences including EMSOFT, ECRTS, and iFM. His pedagogical contributions include courses on programming language theory at École normale supérieure and École polytechnique.

Anton Burtsevمشاهده پروفایل

دانشیار

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

Anton Burtsev is an Associate Professor at the Kahlert School of Computing, University of Utah. His research focuses on redefining operating system architectures to address modern challenges like security attacks, data center workloads, and heterogeneous hardware. He leads the Mars Research Group, developing systems like the formally verified Atmosphere microkernel in Rust/Verus, and the high-performance DRAMHiT hash table. Key projects include Rust for Linux kernel integration, verified drivers (Veld), and isolation mechanisms like RedLeaf OS. Research interests include kernel isolation, formal verification, language safety (Rust), and overcoming the memory wall. Current work emphasizes clean-slate OS designs and retrofitted security solutions for existing kernels. Collaborative projects include Horizon (secure scientific cloud computing) and RedLeaf OS verification efforts. Advising undergraduate to PhD students interested in OS research. Notable grants include NSF CAREER (NgOS) and collaborative NSF grants on verified systems. Active in the MARS reading group and open-source contributions via repositories.

Michael Norrishمشاهده پروفایل

دانشیار

• Formal Methods
• Interactive Theorem Proving
• Programming Languages
• +۴ مورد دیگر

Michael Norrish is an Associate Professor at the School of Computing, Australian National University (ANU) , specializing in formal methods, programming language semantics, and interactive theorem proving. His career spans roles at NICTA, Data61, and ANU, with a focus on mechanised mathematics and verified systems. PhD in Computer Science (University of Cambridge, 1999) Undergraduate degree from Victoria University of Wellington His research bridges interactive theorem-proving (ITP) systems like HOL4 with real-world systems verification, particularly in programming languages and compilers. He leads the CakeML project, developing a verified compiler for functional languages. His work intersects formal verification with practical system design, including projects on reproducibility debt in scientific software and verified processors. Recent publications highlight verified compilation techniques, reproducibility challenges, and Kolmogorov complexity formalization. He actively participates in conference program committees (e.g., CPP, PLDI) and promotes trustworthy systems development through tools like HOL4. Current affiliations: ANU, CakeML Project, Trustworthy Systems Research Group (UNSW) Collaborations: Chalmers University (postdoc opportunities), seL4 microkernel ecosystem

Gary Tanمشاهده پروفایل

استاد

• computer security
• formal methods
• programming languages
• +۳ مورد دیگر

Gang (Gary) Tan is a Professor in the Computer Science and Engineering Department at Pennsylvania State University, co-directing the Institute for Networking and Security Research (INSR). His research bridges computer security, formal methods, and programming languages to develop practical solutions for software vulnerabilities and AI fairness. Education: B.E. in Computer Science from Tsinghua University Ph.D. in Computer Science from Princeton University Dr. Tan specializes in applying compiler techniques and formal verification to security challenges, with seminal work on cache side-channel attacks and fairness in machine learning. His Security of Software (SOS) Group develops frameworks that integrate theoretical guarantees into real-world systems, emphasizing measurable security outcomes and ethical AI. Recent projects focus on quantifying bias in neural networks and mitigating speculative execution vulnerabilities. Analysis of his 2021-2025 publications reveals a strategic pivot toward AI security, where he pioneers methods for fairness testing (e.g., information-theoretic debugging) and repair (e.g., NeuFair). Concurrently, his security work evolves from foundational side-channel research (SpecSafe, 2021) toward hardware-software co-design solutions, demonstrating consistent innovation across theoretical and applied domains. Scientific Awards: James F. Will Career Development Professorship NSF CAREER Award Google Research Award (two instances) Distinguished Reviewer Award at 2018 IEEE Symposium on Security and Privacy Outstanding Research Award at Penn State Ruth and Joel Spira Excellence in Teaching Award Best Paper Award at PLDI 2024 Dr. Tan leads the SOS Group with funding from NSF (including CAREER), DARPA (ISAT study group membership), and industry partners like Google. His grants support interdisciplinary projects spanning secure compilation, fairness engineering, and hardware security, while his teaching excellence award reflects commitment to pedagogy in core systems courses. He co-directs Penn State's Institute for Networking and Security Research (INSR), fostering collaboration between systems, security, and AI researchers. The SOS Group maintains active partnerships with industry security teams and contributes to open-source tools for vulnerability detection, with recent work expanding into fairness certification for machine learning pipelines.