Find Academic Supervisors

Kathleen FisherView profile

Adjunct Professor

• Programming Languages
• Domain-Specific Languages (DSLs)
• Program Synthesis
• +5 more

Kathleen Fisher is the Director of the Information Innovation Office at DARPA and an Adjunct Professor of Computer Science at Tufts University. She previously served as a full Professor and Chair of the Department of Computer Science at Tufts (2016–2021) and held roles as a Program Manager at DARPA (managing the HACMS and PPAML programs) and Principal Member of Technical Staff at AT&T Labs Research. She earned her PhD in Computer Science from Stanford University. Education: PhD in Computer Science, Stanford University. Research Interests: Kathleen’s work focuses on advancing programming languages theory and practice, with three core thrusts: (1) Domain-Specific Languages (DSLs) (e.g., Hancock, PADS, Forest), (2) Program Synthesis (e.g., generating programs from specifications), and (3) Formal Methods for provably correct software (e.g., the DARPA HACMS program). Her research emphasizes collaboration and interdisciplinary applications in cybersecurity and data wrangling. Publications: Her recent work spans DSL design, verified parsers, binary message format inference, and lens synthesis. Key trends include leveraging formal methods for security and advancing program synthesis techniques for practical systems. Awards: ACM Fellow (2011), Hertz Foundation Fellow, SIGPLAN Distinguished Service Award, and past leadership roles in SIGPLAN and the CRA-W Committee. Advising & Grants: Advised PhD students (e.g., Matthew Ahrens), led DARPA-funded projects, and contributed to open-source tools like Hoopl and ANTLR. Her lab, the TuPL Group , focuses on programming language innovations and education. Labs/Teams: Founded the Tufts Programming Languages (TUPL) research group and co-leads the Fisher Lab, advancing interdisciplinary applications of programming language techniques.

Roman IakymchukView profile

Associate Professor

• Numerical Linear Algebra
• Parallel Programming
• High Performance Computing
• +3 more

Roman Iakymchuk is an Associate Professor at the Department of Computing Science within Umeå University, Sweden. His work focuses on numerically reliable and sustainable algorithmic solutions, emphasizing accuracy, reproducibility, and energy efficiency in high-performance computing environments. Research Interests: Numerical linear algebra, parallel programming models, sustainable computing, and optimization of distributed systems. Teaching: Courses on scientific computing, CUDA/OpenMP/MPI-based parallel programming, and floating-point error correction. The articles highlight his contributions to mixed-precision computing, numerical reliability in Krylov solvers, and energy-efficient practices in HPC systems. His work spans algorithm design, tool-assisted implementation, and European collaborative projects like CEEC.

Stacey JefferyView profile

Professor

• Quantum Cryptography
• Quantum Algorithms
• Quantum Walks
• +2 more

Roles & Affiliations: Senior Researcher at Centrum Wiskunde & Informatica (CWI), member of QuSoft Professor of Quantum Information at the Korteweg-de Vries Institute for Mathematics, University of Amsterdam Education: PhD in Computer Science (2014), University of Waterloo, supervised by Prof. Michele Mosca Postdoctoral Scholar at Caltech's IQIM (2014–2016) Research Interests: Focuses on quantum algorithms and quantum cryptography, including secure delegation of quantum computation, quantum algorithm frameworks, quantum walks, and quantum complexity theory. Her work emphasizes practical applications such as verifiable delegated computation and quantum time-space tradeoffs. Recent Trends in Articles: Recent publications explore verifiable quantum computation (e.g., quasilinear resource schemes), quantum time complexity (e.g., taming quantum algorithms), and multidimensional quantum walks (e.g., recursion and divide-and-conquer strategies). These contributions highlight advancements in quantum efficiency, security, and algorithmic design. Awards & Grants: ERC Starting Grant (2022) Quantum Delta NL Award (2023) NWO Veni Grant (2017) CIFAR Fellowship in Quantum Information Science (2019) Advising & Grants: Active in grant-funded projects like Quantum time-space tradeoff lower bounds and Algorithms, Security and Complexity for Quantum Computers (ASC-Q) . Teaches advanced courses on quantum algorithms at the University of Amsterdam. Labs & Collaborations: Affiliated with QuSoft, a Dutch research center for quantum software, and collaborates on international initiatives like the Lorentz Center Informatics Advisory board.

Frank de BoerView profile

Researcher

• Formal Methods
• Concurrency Theory
• Object-Oriented Programming
• +3 more

Frank de Boer is a researcher at Centrum Wiskunde & Informatica (CWI), Amsterdam , focusing on formal methods , concurrency theory , and software verification . His work bridges theoretical foundations with practical applications in object-oriented programming and parallel systems. Key research areas: Separation logic for heap reasoning Behavioral subtyping and history-based verification Active objects and actor models Concurrency and deadlock analysis Selected scientific recognition: Best Paper (ESSOC 2017) Bronzen Achievement Award (Trust4All 2008) Forum-Architectuurprijs (Archimate 2008) Recent publications (2025–2021) emphasize footprint logic, history-based reasoning, and formal verification of concurrent systems. Collaborations span institutions in The Netherlands, Germany, and China, with applications to Java collections, multicore memory systems, and transition system models.

Jana WagemakerView profile

Assistant Professor

• Formal Methods
• Program Analysis
• Kleene Algebra
• +4 more

Jana Wagemaker is an Assistant Professor at Radboud University in Nijmegen, affiliated with the Software Science Group since July 2024. Previously, she was a postdoc at Reykjavik University collaborating with Antonis Achilleos and Luca Aceto. She earned her PhD at Radboud University under Jurriaan Rot and Alexandra Silva, defending her thesis titled Extensions of (Concurrent) Kleene Algebra in October 2022. Education: PhD in Computer Science (Radboud University, 2022) Her research focuses on formal methods for program analysis, using algebraic frameworks like Kleene algebra to provide mathematical guarantees about software behavior. She explores modular specification language development and the logical foundations of monitorability in runtime verification, emphasizing correctness proofs, decidability, and behavioral guarantees. Key Research Areas: Formal Methods, Program Analysis, Kleene Algebra, Runtime Verification, Automated Reasoning

Bernhard BeckertView profile

Professor

• Formal Methods
• Software Verification
• Security and Dependability
• +9 more

Prof. Dr. Bernhard Beckert is a faculty member at the Karlsruhe Institute of Technology (KIT) , affiliated with the Department of Informatics and the Institute of Information Security and Dependability (KASTEL) . His research focuses on formal verification of software systems, particularly through logic-based methods, security and dependability analysis, automated deduction in classical and non-classical logics, and applications to voting algorithms, industrial automation, and scientific software. Email: beckert@kit.edu Office: Building 50.34, Room 224, KASTEL, Am Fasanengarten 5, 76131 Karlsruhe, Germany He develops and applies the KeY system for deductive verification of object-oriented software, with applications in Java, PLCs, and safety-critical systems. His work addresses challenges in regression verification, information flow security, and multi-phase verification for robotic surgery. Recent publications focus on equivalence analysis of control software variants, program slicing, loop bound computation, and formalization of voting rules using bounded model checking. Key contributions include integrating design and verification workflows, dynamic logic extensions for concurrency, and tools for security-sensitive software engineering.

Piotr SzwedView profile

Lecturer

• Data Mining
• Software Engineering
• Computational Intelligence
• +5 more

Dr inż. Piotr Szwed is a Lecturer in the Department of Applied Computer Science at AGH University of Science and Technology, Kraków. He is affiliated with the Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering (EAIiIB), where he teaches courses ranging from imperative and object-oriented programming to data exploration and computational intelligence. Research Interests: Data mining and knowledge discovery Fuzzy cognitive maps and their applications in transportation, risk assessment, and security Software engineering methodologies, including agile and ontology-driven development Intelligent transportation systems (ITS) and real-time traffic management Natural language processing for Polish texts, stylometry, and authorship attribution Ontology engineering, enterprise architecture verification, and model checking His work often bridges theoretical computer science with practical applications in urban mobility, safety systems, and enterprise software. Scientific Contributions: Pioneered the integration of fuzzy cognitive maps with evolutionary algorithms to predict traffic flows. Developed rule-based and machine-learning approaches to determine speed limits from geospatial data. Contributed to the INSIGMA intelligent transportation system aimed at enhancing urban mobility in Polish cities. Created formal verification techniques for ArchiMate business processes using NuSMV model checking. Advanced stylometric analysis for Polish texts, introducing part-of-speech features for authorship attribution. Teaching & Academic Service: Regularly teaches Programming (C, C++, Java), Software Engineering, Data Exploration, and Computational Intelligence. Supervises engineering and master theses in applied computer science. Maintains a public wiki with course materials, lab exercises, and consultation schedules for students. Utilizes Git-based repositories to streamline code submission and continuous assessment in laboratory classes. Laboratory & Facilities: He is located in building C-2, room 403, at AGH’s main campus, al. Mickiewicza 30, 30-059 Kraków. The lab supports courses that emphasize practical software development, version control, and collaborative project work.

• WebAssembly
• Formal Verification
• Memory Models
• +3 more

Jean Pichon-Pharabod is a Tenure Track Assistant Professor in the Department of Computer Science at Aarhus University, Denmark, with an office at Åbogade 34 in Aarhus N. His research spans formal verification, programming languages, and computer architecture, focusing on foundational work for secure and reliable systems. His primary research interests include the formal verification of WebAssembly, relaxed memory models for architectures like Arm, and security invariants for virtualized environments. He develops mechanized proofs using frameworks like Iris and Coq to establish robust safety properties for compilers, hypervisors, and low-level systems. His work bridges hardware semantics with programming language theory to address concurrency challenges in modern architectures. Analysis of his 2021-2025 publications reveals a consistent focus on verified compilation (CertiCoq-Wasm), axiomatic semantics for relaxed architectures (AxSL logic), and memory-safe WebAssembly verification (Iris-MSWasm). His research demonstrates strong international collaboration, particularly with Lars Birkedal at Aarhus University, and targets high-impact venues like PACMPL and CPP. Key trends include mechanized separation logics for virtual machines (VMSL) and formal elucidation of hardware-software interfaces for security-critical systems.

Patrick BahrView profile

Associate Professor

• Type Systems
• Compilers
• Functional Programming
• +4 more

Patrick Bahr is an Associate Professor at the IT University of Copenhagen and Co-Head of Education for the Master of Software Design program. His research focuses on developing programming languages and tools to ensure high-assurance software through formal methods. Education : PhD in Computer Science (2012), University of Copenhagen; MSc in Computational Logic (2009), Dresden & Vienna University of Technology; BSc in Computer Science (2008), Dresden University of Technology Patrick's research spans Type Systems , Compilers , and Functional Reactive Programming (FRP) , emphasizing Modal Types to ensure causality and productivity. His work includes Formal Verification of compiler correctness and Domain-specific Languages for enterprise and financial contracts. Recent publications highlight trends in Graph-Based Compilers , Asynchronous FRP , and Guarded Recursion . His methodologies often integrate Haskell and Agda for verified implementations. Key contributions include Sound-By-Construction Type Systems and Monadic Compiler Calculation . Scientific Awards : Best Contribution to RTA 2010 DIKU Paper of the Year 2012 He actively contributes to program committees (e.g., TFP 2026, ICFP 2024) and has led research projects like Guarded Recursive Types funded by the Danish Independent Research Fund (2015-2019). Collaborations span institutions such as the University of Nottingham and Utrecht University.

Shafi GoldwasserView profile

Professor

• Cryptography
• Theoretical Computer Science
• Computational Complexity
• +7 more

Shafi Goldwasser is a prominent computer scientist holding dual appointments as the RSA Professor of Electrical Engineering and Computer Science at the Massachusetts Institute of Technology (MIT) and as a Professor of Computer Science and Applied Mathematics at the Weizmann Institute of Science in Israel. Her groundbreaking work has fundamentally shaped modern cryptography and theoretical computer science, earning her numerous prestigious awards including the ACM A.M. Turing Award in 2012 (shared with Silvio Micali). Dr. Goldwasser received her B.S. in Mathematics from Carnegie Mellon University (1979), followed by an M.S. (1981) and Ph.D. (1984) in Electrical Engineering and Computer Science from the University of California at Berkeley. Her academic career at MIT began with a Bantrel Postdoctoral Fellowship in 1983, followed by positions as Assistant Professor (1983-1987), Associate Professor (1987-1992), and Professor (1992-present). She also serves as Co-Leader of MIT's Cryptography and Information Security Group (1995-present) and has held a parallel appointment at the Weizmann Institute since 1993. Goldwasser's research has revolutionized theoretical computer science and cryptography through several landmark contributions. She pioneered the concept of zero-knowledge proofs, which allow one to prove the validity of a statement without revealing any information beyond the statement's truth. Her work with Micali on probabilistic encryption established the now-standard definitions of security for encryption and digital signatures. Goldwasser also made fundamental contributions to interactive proofs, multi-prover systems, probabilistically checkable proofs (PCPs), and property testing. Her research has not only transformed cryptography into a rigorous mathematical science but has also had profound implications for computational complexity theory. Analysis of her publication record reveals consistent innovation across decades, with major contributions spanning from foundational work in the 1980s (zero-knowledge proofs, probabilistic encryption) through to contemporary research on delegated computation, code obfuscation, and side-channel attack resistance. Her work consistently bridges theoretical computer science and practical cryptographic applications. ACM A.M. Turing Award (2012) ACM Athena Lecturer Award (2008) Two SIGACT Gödel Prizes (1993, 2001) ACM Grace Murray Hopper Award (1996) RSA Award in Mathematics (1998) Franklin Institute Benjamin Franklin Medal (2010) IEEE Emanuel R. Piore Award (2011) Memberships in all three major US National Academies As an advisor, Goldwasser has mentored numerous graduate students, with Johan Håstad being noted as her first exceptional doctoral student. Her research group at MIT has been instrumental in advancing the field of cryptography and theoretical computer science. Recent work has focused on delegated computation, code obfuscation, and protection against side-channel attacks, addressing emerging challenges in cloud computing and information security. Outside of her academic pursuits, Goldwasser is known to practice "Playback Theater," an improvisational interactive group experience, reflecting her interest in creative expression beyond computer science.

Ashutosh GuptaView profile

Associate Professor

• Formal Verification
• Software Verification
• Model Checking
• +7 more

Ashutosh Gupta is an Associate Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology Bombay, where he has been a faculty member since 2018. His research focuses on formal methods for software verification, particularly in the areas of model checking, constraint solving, and automated reasoning for both sequential and concurrent programs. He teaches advanced courses including Automated Reasoning (CS433), Analysis of Concurrent Programs (CS766), and Logic for Computer Science (CS228). Dr. Gupta received his Ph.D. in Computer Science from Technical University of Munich (TUM) in 2011, with affiliations during his doctoral studies at TUM, Max Planck Institute for Software Systems (MPI-SWS), and École Polytechnique Fédérale de Lausanne (EPFL). Prior to joining IIT Bombay, he served as a faculty member at Tata Institute of Fundamental Research (TIFR) in Mumbai and completed post-doctoral research in the Henzinger group at IST Austria. His research interests span formal verification of sequential and concurrent software, modeling of biological systems, and constraint solving including constraint logic programming, decision procedures, and automated theorem proving. He has developed several verification tools including VAJRA, HSF, and InvGen. His work bridges theoretical foundations with practical applications, particularly in verifying safety-critical systems and biological processes. Dr. Gupta's publication record shows a consistent trajectory of high-impact research in top venues like POPL, CAV, TACAS, and AAAI. His recent work has expanded into neural network verification, reinforcement learning verification for medical devices, and applying formal methods to biological systems, demonstrating both depth in core verification techniques and breadth in application domains. Best Paper Award at TACAS 2015 Best Paper Award at TACAS 2009 Dr. Gupta actively mentors numerous students through course projects, research presentations, and specialized workshops like SATfest. He has supervised students working on SAT/SMT solvers, verification of concurrent programs, and applications of formal methods to biological systems. His teaching philosophy emphasizes hands-on experience with verification tools and encourages students to engage with cutting-edge research through reading and presenting recent conference papers. He maintains active research collaborations with institutions including TUM, MPI-SWS, EPFL, IST Austria, and TIFR, reflecting his continued integration into the international formal methods research community.

Chandrakana NandiView profile

Assistant Professor

• Formal Verification
• Smart Contracts
• DeFi Applications
• +7 more

Chandrakana Nandi is the Director of US R&D at Certora and an affiliate assistant professor at the University of Washington, Seattle . Her work bridges formal verification, computational fabrication, and programming language design. Education : PhD in Computer Science from University of Washington (2021), MS in Computer Science (2014), BS in Computer Science (2012). Research Interests focus on: Automated formal verification of DeFi applications and smart contracts. Equality saturation for program synthesis, verification, and compiler optimizations. Programming languages and compilers for computational fabrication and 3D modeling. Publication Trends highlight her contributions to: Formal verification tools for real-world programs (WASM, G-code). Equality saturation applications in synthesis, optimization, and rule inference. Domain-specific languages like LambdaCAD, Taxon, and Carpentry Compiler. Scientific Awards : Distinguished Paper Award (OOPSLA 2021). Distinguished Paper Award and Sigplan Research Highlight (POPL 2021). Contact : chandra@certora.com . Her CV is available here .

• Operating Systems
• Computer Architecture
• Virtualization
• +3 more

Prof. Redha Gouicem holds the Chair of Operating Systems at RWTH Aachen University. His research focuses on operating system design, virtualization, and multicore scheduling, with an emphasis on formal verification and performance optimization. Professorship: Operating Systems Location: RWTH Aachen University, Germany Research interests include: Multicore scheduling algorithms Binary translation and virtualization Formal verification of OS components CPU frequency scaling and performance optimization Comparison of scheduling models in Unix/Linux Domain-specific languages for scheduler development Recent work explores hypervisor-agnostic guest overlays, weak memory model translation, and provably correct multicore schedulers. His publications demonstrate technical depth in system software design and concurrency management. Current affiliations: RWTH Aachen University Chair of Operating Systems

• Bayesian Statistics
• Category Theory
• Compiler Construction
• +4 more

Matthijs Vákár is an Assistant Professor at the Department of Information and Computing Sciences , Utrecht University , focusing on the software foundations of machine learning . He actively develops the Stan language , a state-of-the-art probabilistic programming language. Areas of Expertise: Bayesian Statistics, Category Theory, Compiler Construction, Machine Learning, Programming Languages. Research Themes: Probabilistic programming languages, differential programming languages, separation of modeling from algorithmic tasks, automatic differentiation in ML-family languages. His research bridges theoretical computer science and practical machine learning, emphasizing logical relations, monoidal structures, and efficient compiler designs for differentiable programming. His recent publications explore correctness proofs, category-theoretic models, and optimization techniques in automatic differentiation. Scientific Awards: ERC Starting Grant NWO Veni Fellowship Marie Sklodowska-Curie Fellowship Academic Journey: PhD from the University of Oxford (dependent types and computational effects), MSc in Pure Mathematics (University of Cambridge), and BScs in Mathematics and Physics (Utrecht University). Prior roles include postdoctoral research at Columbia University and the University of Oxford. Industrial Experience: Build systems at Microsoft Research, NLP at Linguamatics, and compiler design for Stan.

• Cybersecurity
• Formal Verification
• Software Engineering for Distributed Systems
• +2 more

Roberto Guanciale is a Lecturer at KTH Royal Institute of Technology , affiliated with the Department of Theoretical Computer Science under the School of Electrical Engineering and Computer Science. He teaches and examines courses such as Cybersecurity Overview , Software Security , Applied Cryptography , and Degree Projects focusing on cybersecurity, communication systems, and distributed software engineering. His research interests lie in cybersecurity , formal verification , and software engineering for distributed systems . His recent publications address formal methods for securing P4 programs, symbolic execution for binary verification, and flow security in microarchitectures. These works emphasize rigorous mathematical approaches to network and hardware security. Teaching Roles: Cybersecurity Overview Course (DD2391) - Course Manager The Role of the Cybersecurity Engineer (DD2303) - Teacher Software Security (DD2460) - Teacher Project in Cybersecurity (DD2394) - Examiner and Course Coordinator