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

Thomas Nollمشاهده پروفایل

دانشیار

• Static Program Analysis
• Quantum Software Compilation
• Reliability Engineering
• +۱ مورد دیگر

Dr. Thomas Noll is an Associate Professor at the Department of Computer Science, RWTH Aachen University. He is a member of the Software Modeling and Verification Group (MOVES) led by Prof. Joost-Pieter Katoen. Research Interests Static Program Analysis for Software Optimization and Verification Compilation of Quantum Software Reliability, Safety, and Security of Hardware/Software Systems Formal Verification of Artificial Neural Networks He has supervised over 30 bachelor's and master's theses at RWTH Aachen University from 2002 to 2024, including topics on probabilistic model checking, neural network verification, and program analysis. His administrative roles include Examination Board membership for Computer Science (since 2012), QVM funds management (since 2024), and student advising across multiple disciplines. He has participated in over 40 program committees and organized 8 conferences/workshops since 2004, focusing on formal verification and software engineering applications.

Enrico Tronciمشاهده پروفایل

استاد

• Model Checking
• Cyber-Physical Systems
• Software Engineering
• +۷ مورد دیگر

Enrico Tronci is a Full Professor in the Department of Computer Science at Università degli Studi di Roma La Sapienza , Italy. His research focuses on model checking, formal verification, and synthesis of cyber-physical systems, with applications to mission-critical and safety-critical domains such as space systems, smart grids, and healthcare. He leads the Model Checking Lab (MCLab) and has coordinated numerous national and international research projects funded by organizations including the European Community (EC), European Space Agency (ESA), and Italian Ministry of University and Research (MUR). Research Highlights : Automatic control software synthesis from closed-loop specifications Model checking algorithms for hybrid and stochastic systems Technology transfer in sectors like energy, transportation, and aerospace Teaching : Undergraduate: Software Engineering (Fall 2024) Graduate: Automatic Verification of Intelligent Systems (Fall 2024), Verification and Validation of Intelligent Systems (Spring 2025) Scientific Awards : Recipient of the IBM-Italia 1987 prize for best thesis in Artificial Intelligence Publications Trends : 2024: Scaling up model checking for cyber-physical systems via HPC 2023: Hormonal impact on behavior and fault-tolerant sensor deployments 2021-2022: In silico clinical trials, smart grid management, and scenario enumeration 2020: AI-guided diabetes patient modeling and forensic psychiatry applications Software Tools : QKS (Quantized Kontrol Synthesizer) NashMV (MAD systems verification) CMurphi (Hybrid systems model checker) FHP-Murphi (Probabilistic verification) BSP (Boolean symbolic programming)

• Software Engineering
• Formal Methods
• Autonomous Systems
• +۳ مورد دیگر

Eduard Baranov is a Visiting Lecturer and Research Assistant at the Université catholique de Louvain, affiliated with the Louvain Polytechnic School (EPL) through the Computer Engineering Center (INGI) under the Institute of Information and Communication Technologies, Electronics and Applied Mathematics (ICTEAM). His work bridges academic research with industrial applications. Research Interests : Software engineering, formal methods, cybersecurity, autonomous systems, and model checking. His focus spans scalable coverage estimation, secure healthcare systems, and statistical validation of privacy protocols. Publications : Recent work includes t-wise coverage algorithms for software testing, formal verification of multi-agent autonomous systems, and privacy-preserving frameworks aligned with GDPR standards. His research often integrates symbolic execution and statistical model checking. Collaborations : Collaborates with researchers like Axel Legay, Kuldeep S. Meel, and Thomas Given-Wilson, contributing to journals such as IEEE Transactions on Software Engineering and ACM Transactions on Software Engineering and Methodology. Contact : Email: eduard.baranov@uclouvain.be | Office: INGI - Réaumur, L5.02.01, Place Sainte Barbe 2, 1348 Louvain-la-Neuve.

Sandeep K. Shuklaمشاهده پروفایل

استاد

• Formal Methods
• Formal Verification
• Model Driven Engineering
• +۸ مورد دیگر

Sandeep K. Shukla is a Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology Kanpur (IIT Kanpur), where he conducts cutting-edge research in formal methods, embedded systems, and cyber security. Previously, he served as Professor at Virginia Tech and held various academic positions including Associate Professor and Assistant Professor at the same institution. Dr. Shukla received his educational foundation from prestigious institutions: PhD in Computer Science from State University of New York at Albany (1997) M.S. in Computer Science from State University of New York at Albany (1995) B.E. in Computer Science and Engineering from Jadavpur University, Kolkata (1991) His research interests span multiple domains within computer science and engineering, with a strong focus on formal verification techniques for system design. Dr. Shukla specializes in applying formal methods to critical infrastructure systems, embedded hardware and software design, and smart grid technologies. His work bridges theoretical computer science with practical engineering applications, particularly in safety-critical domains where reliability is paramount. He has pioneered approaches in model-driven engineering and software synthesis that have influenced industry standards and practices. Dr. Shukla's publication record demonstrates a consistent trajectory of innovation in system-level design methodologies. His work shows a clear progression from foundational research in formal verification to practical applications in critical infrastructure systems. The publications reveal expertise across computer science subfields including embedded systems design, formal methods, hardware-software co-design, and cyber-physical systems. His more recent work focuses on integrating different computational models for complex system design, particularly addressing challenges in smart grid and critical infrastructure security. Dr. Shukla has received numerous prestigious awards recognizing his contributions to the field: IEEE Fellow (2014) for "contributions to applied probabilistic model-checking for system design" ACM Distinguished Scientist (2013) Humboldt Bessel Award (2008) Presidential Early Career Award for Scientists and Engineers (2003) National Science Foundation CAREER Award (2002) Throughout his career, Dr. Shukla has mentored numerous graduate students and secured significant research funding from various sources including the National Science Foundation, US Air Force, and other government agencies. His work on reliability-driven nano-computing led to the development of the NANOPRISM tool, and his contributions to system-level design languages influenced new kernels of the SystemC language. He has collaborated extensively with international research groups, including projects funded by US AFOSR to collaborate with INRIA and the University of Kaiserslautern. Dr. Shukla is actively involved with research centers including the Center for Developing Intelligent Systems (CDIS) at IIT Kanpur. His work integrates multiple research teams focusing on formal methods applications to critical infrastructure systems, with particular emphasis on smart grid security and embedded system reliability. His research group maintains strong industry connections, particularly with technology companies working on embedded systems and security solutions.

• Theoretical Computer Science
• Formal Verification
• Game Theory
• +۷ مورد دیگر

Professor Sven Schewe is affiliated with the University of Liverpool, focusing on finite games of infinite duration and automata over infinite structures. He emphasizes collaborative research and teaching, though admits to challenges in maintaining web pages. EPSRC grant (2017-2021) for Parity Games EPSRC grant (2015-2019) for Energy Efficient Control DST (UK) grant (2018-2020) for AI Test Metrics EU grant (2017-2019) for Parametrised Verification Leverhulme Trust grant (2011-2012) for Probabilistic Systems EPSRC grant (2010-2013) for Markov Decision Processes His research spans formal verification, game theory, probabilistic systems, and secure computation. Key publications include work on parity games, adversarial training, and multi-party querying. He serves as a reviewer for major conferences and journals, including ACM Transactions on Computational Logic and IEEE Symposiums. Scientific awards include the Dr. Eduard Martin Preis (2009) and the GI Dissertation Award (2009). He supervises theses on topics like semantic testing for neural networks, symbolic discrete control, and power grid frameworks. As PhD Admission Tutor for Computer Science, he contributes to academic governance. His recent articles highlight collaborations in AI security, chemical space exploration, and automata theory.

• Modular development of specification languages
• Algorithms for models of computation
• Coalgebra
• +۴ مورد دیگر

Alexandra Silva is a Professor of Computer Science at Cornell University with prior affiliations as a Royal Society Wolfson Fellow and Professor of Algebra, Semantics, and Computation at University College London . She leads a research group focusing on the modular development of specification languages and algorithms for models of computation, emphasizing coalgebra as a unifying mathematical framework. Research Interests Her work spans foundational and applied areas in theoretical computer science, including: Coalgebraic methods for formal verification Automata theory and learning algorithms Probabilistic programming and semantics Programming language design (e.g., NetKAT, Kleene Algebra with Tests) Concurrency theory and distributed systems Algebraic structures in computation Recent publications address network verification (StacKAT), symbolic automata learning, probabilistic regular expressions, and outcome logic for correctness/incorrectness reasoning. She is actively involved in organizing academic events like OPLSS 2025 and co-authoring foundational works in Formal Aspects of Computing and Theoretical Computer Science . Scientific Awards Distinguished Paper Award (ACM SIGPLAN POPL, 2020) Best Paper Award (RTA, 2015) She teaches courses on Kleene Algebra with Tests (KAT) and verification at summer schools like Marktoberdorf 2025 , and her research includes collaborations on probabilistic network verification (ProbNV) and stochastic system modeling.

Soham Chakrabortyمشاهده پروفایل

استادیار

• Programming Languages
• Compilers
• Computer Architecture
• +۳ مورد دیگر

Soham Chakraborty is an Assistant Professor at the Programming Languages Group, TU Delft since 2021. He previously served as an Assistant Professor at the CSE Department, IIT Delhi before joining TU Delft. His academic journey includes a PhD from Max Planck Institute for Software Systems (MPI-SWS) in 2019 and a Master's degree from CSE Department, IIT Kharagpur in 2008. Affiliation: TU Delft, IIT Delhi, MPI-SWS Research Interests: Programming Languages, Compilers, Architecture, Verification, Concurrency His research focuses on formal semantics, compiler correctness, architecture-to-architecture translation, and verification of weak memory models. He has contributed to major conferences including POPL, PLDI, CGO, and ASPLOS. His work addresses challenges in heterogeneous concurrency, relaxed memory concurrency, and binary translation for weak memory architectures. Recent works include How Hard is Weak-Memory Testing? (POPL'24) and Toast: A Heterogeneous Memory Management System (PACT'24). He also received the Distinguished Paper Award at DATE'25 and Distinguished Artifact Award at PODC'22 . Teaching: Courses like Concepts of Programming Languages (CS2120), Parallel and Concurrent Programming (CS4555), Compiler Construction (CS4555), Analysis of Concurrent and Distributed Programs (CS4405), Software Fundamentals (Rust), and Seminar Programming Languages (COL 380) Students: PhD student Dennis Sprokholt, MSc students Michal Raczkiewicz, Alexandru Dumitriu, Huixuan Wu, and alumni including Pieter van den Ham, Mingyu Gao, Jeroen Kloppenburg, and others. Service: Served on program committees for POPL, PLDI, CGO, VMCAI, APLAS, and Eurosys workshops.

Thomas W. Repsمشاهده پروفایل

استاد

• Program Analysis
• Abstract Interpretation
• Model Checking
• +۴ مورد دیگر

Thomas W. Reps is the J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair Emeritus at the University of Wisconsin-Madison , where he has been a faculty member since 1985. He is also President of GrammaTech, Inc., and a co-founder of the company. Education: Ph.D. in Computer Science from Cornell University (1982), winner of the 1983 ACM Doctoral Dissertation Award. Reps’s research spans program analysis , abstract interpretation , model checking , and computer security . His recent work focuses on quantum computing verification , probabilistic program analysis , and symbolic methods for static analysis . His publications (over 225) include foundational contributions to program slicing (1988 paper with Horwitz and Binkley, cited >1,780 times), machine-code analysis (ETAPS Best-Paper Awards in 2004 and 2008), and programming environments (co-author of The Synthesizer Generator ). Key awards include the ACM SIGPLAN Programming Languages Achievement Award (2017) , Guggenheim and Packard Fellowships , and ACM Fellow (2005) . Students: Mentored award-winning graduates like Akash Lal (SIGPLAN Outstanding Dissertation) and Venkatesh Srinivasan (Outstanding Graduate Student Research Award).

Yizhou Zhangمشاهده پروفایل

استادیار

• Programming Languages
• Probabilistic Programming
• Compiler Design
• +۴ مورد دیگر

Yizhou Zhang is an Assistant Professor at the Cheriton School of Computer Science, University of Waterloo. He specializes in programming language design and implementation, focusing on balancing expressive power with strong guarantees through language abstractions and compiler verification. Designing modular, type-safe language systems Probabilistic programming and inference optimization Algebraic effects and control flow management His recent publications explore lexical effect handlers, certified compiler frameworks, and nested polymorphism models. Awards include the ACM SIGPLAN Distinguished Paper Award (2023) for his work on probabilistic program compilation. Current advisees include PhD candidates Cong Ma, Zhaoyi Ge, Jianlin Li, and Ende Jin. He has served on program committees for POPL, PLDI, and OOPSLA conferences.

Marc Pouzetمشاهده پروفایل

استاد

• Programming Languages
• Synchronous Systems
• Reactive Systems
• +۳ مورد دیگر

Marc Pouzet is a Professor at École Normale Supérieure (ENS) in the Department of Computer Science (DIENS), where he serves as Director of CS studies. He leads the INRIA project-team PARKAS and was a Junior Member of the Institut Universitaire de France (2007–2012). His research centers on synchronous programming languages for safety-critical embedded systems, with contributions to real-time software verification, hybrid systems modeling, and probabilistic reactive programming. Research Focus Pouzet's work bridges theory and practice in: Synchronous Languages : Design/extensions of Lustre, Lucid Synchrone, and Zelus for embedded control Formal Methods : Mechanized semantics (Coq) and verified compilers (Vélus) for correctness guarantees Hybrid Systems : Integrating ODEs with discrete logic (ProbZelus for probabilistic inference) Real-time Systems : Scheduling, latency constraints, and memory-safe compilation Awards & Leadership Inria–Académie des sciences Innovation Award (2016) Program committees: EMSOFT, PLDI, POPL, ECRTS Associate Editor: EURASIP Journal on Embedded Systems Advising & Projects Supervised 19+ PhD students on topics spanning compiler verification (Bourke, Pesin), probabilistic languages (Baudart), and hybrid systems (Pauget). Leads development of open-source tools: Zelus (synchronous language with ODEs) Vélus (verified Lustre compiler) ReactiveML (reactive extension of OCaml)

Laure Petrucciمشاهده پروفایل

استاد

• Formal Methods
• Concurrent Systems
• Petri Nets
• +۳ مورد دیگر

Laure Petrucci is a Professor at Sorbonne Paris Nord University, affiliated with the Networks and Telecommunications Department and the LoVe (Logic and Verification) team at LIPN (Paris Nord Computer Science Laboratory, CNRS UMR 7030). She also serves as Deputy Scientific Director of CNRS for Normandy. Her research specializes in formal verification of concurrent systems using Petri nets and parameterized models, with a focus on combating state-space explosion through distributed algorithms. Her work spans formal methods , distributed systems , and model checking , emphasizing practical applications in network verification and synthesis. Recent publications explore controller synthesis for timed games, probabilistic model checking, and SMT-based analysis of Petri nets, reflecting a consistent focus on scalable verification techniques. She teaches undergraduate and master's courses in networks, databases, and programming at IUT Villetaneuse (France) and the University of Science and Technology of Hanoi (Vietnam).

Andrzej Murawskiمشاهده پروفایل

استاد

• Programming Languages
• Automata Theory
• Software Verification
• +۹ مورد دیگر

Professor Andrzej Murawski is a Tutorial Fellow at Worcester College , affiliated with the University of Oxford Department of Computer Science . His research spans the semantics of programming languages , automata theory , and software verification , integrating game semantics and probabilistic computation for modeling complex systems. Education: D.Phil., University of Oxford (2001) His work addresses higher-order recursion , concurrent programs , and probabilistic verification , including differential privacy and machine learning applications. Recent publications focus on reachability analysis , contextual equivalence , and automata over infinite alphabets . Key activities include organizing SIGLOG (Vice-Chair), editing SIGLOG News , and serving on LICS , POPL , and CONCUR program committees. Awards include the POPL 2025 Distinguished Paper Award . Students : Current advisees include Benedict Bunting and Haoxuan Yin; past students include Fabian Zaiser and David Hopkins.

• Concurrency Theory
• Process Algebra
• Trustworthy Systems
• +۷ مورد دیگر

Alessandro Aldini is an Associate Professor in the Section of Informatics and Mathematics within the Department of Pure and Applied Sciences (DiSPeA) at the University of Urbino Carlo Bo. His academic work focuses on theoretical computer science with applications to security and verification of complex systems. His research interests span several key areas: Design and verification of concurrent and distributed computer, network, and software systems Trust models and trustworthy systems Concurrency theory and (nondeterministic, probabilistic, and Markovian) process algebra Exact and approximate behavioral equivalences and equivalence checking Exact and approximate noninterference approach to information flow analysis Modal logics and model checking Security, dependability, and performability analysis Professor Aldini serves as the UNIURB research unit leader for the PRIN project AsCoT-SCE (Assessing Compliance of IoT API for Security Critical Environments) and participates in other significant research initiatives including DeKLA (Developing Kleene Logics and their Applications) and NiRvAna (Noninterference and Reversibility Analysis in Private Blockchains). He is actively involved in the academic community through the Italian Chapter of the EATCS and IFIP WG 11.14 Secure Engineering. His teaching responsibilities include Programming Languages and Software Verification and Cybersecurity courses across multiple Informatics degree programs. Professor Aldini has supervised numerous PhD students and postdoctoral researchers. His academic contributions include the book "A Process Algebraic Approach to Software Architecture Design" and his PhD thesis "Security and Performance Analyses in Distributed Systems."

Matteo Camilliمشاهده پروفایل

دانشیار

• Software Engineering
• Software verification
• Automated testing
• +۴ مورد دیگر

Matteo Camilli is an Associate Professor in the Department of Electronics, Information and Bioengineering (DEIB) at Politecnico di Milano, Italy, where he leads research in software engineering and verification. His academic journey includes positions as Assistant Professor at Free University of Bozen-Bolzano and postdoctoral research at the University of Milan and University of Bergamo. His educational background includes a PhD in Computer Science (2015), MSc in Computer Science (2012), and BSc in Computer Science (2009), all from the University of Milan. His doctoral research focused on combining advanced abstraction techniques and big data approaches to address state explosion problems in formal verification. Camilli's research primarily centers on software verification, testing, and methods to improve dependability of autonomous, cyber-physical, service-based, and ML-enabled critical systems. His work spans formal methods, model-based testing, uncertainty quantification, and design-time/runtime verification with applications to complex distributed systems. His recent publications reflect a growing focus on explainable self-adaptation, quality assurance for LLM-based systems, and managing uncertainty in adaptive systems. His publication record includes papers in top journals (TOSEM, TAAS, JSS, EMSE) and conferences (ICSE, ISSRE, ICST, ICSA). He serves on program committees for prestigious conferences including ICSE, ICSA, ICST, and ECSA, and is on the steering committee for the International Workshop on Formal Approaches for Advanced Computing Systems (FAACS). Camilli actively contributes to the academic community through conference organization, including serving as Program Committee Member for numerous conferences and as Program Co-Chair for the Software Architecture track at ACM SAC. He also serves as guest editor for special issues on automated testing and dependable AI systems. His teaching portfolio at Politecnico di Milano includes Software Engineering 2, Software Engineering for Automation, and Distributed Software Development. Previously at Free University of Bozen-Bolzano, he taught Systems Engineering and Verification and Reliability for Dependable Systems.

Tevfik Bultanمشاهده پروفایل

استاد

• software verification
• program analysis
• software engineering
• +۱ مورد دیگر

Tevfik Bultan is a Professor and Chair of the Department of Computer Science at the University of California, Santa Barbara. His research focuses on software verification, program analysis, software engineering, and computer security. He directs the Verification Laboratory (VLab) and has authored over 100 refereed publications. Education Ph.D. in Computer Science, University of Maryland, College Park (1998) M.S. in Computer Engineering, Bilkent University (1992) B.S. in Electrical Engineering, Middle East Technical University (1989) Research Focus Bultan's work spans automated verification techniques, security vulnerability detection, quantitative program analysis, and symbolic execution. His lab develops tools for analyzing software systems with applications in cloud security, network protocols, and embedded systems. Awards and Honors ACM Distinguished Scientist (2016) NSF CAREER Award (2000) UCSB Outstanding Graduate Mentor Award (2016) ACM SIGSOFT Distinguished Paper Awards (2005, 2014) NATO Science Fellowship (1993) Professional Activities He has chaired program committees for top conferences including ICSE, FSE, and ASE. Currently serves as associate editor for ACM TOSEM and on steering committees for ISSTA, ASE, and ICSE. Regularly advises PhD students and postdoctoral researchers in verification and security. Laboratory Leads the Verification Laboratory (VLab) focusing on automated reasoning techniques for software systems. Current projects include symbolic analysis for vulnerability detection, quantitative information flow, and security policy verification.