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

Kuldeep S. Meelمشاهده پروفایل

دانشیار

• Automated Reasoning
• Formal Methods
• Artificial Intelligence
• +۶ مورد دیگر

Kuldeep S. Meel is the Stephen Fleming Early-Career Associate Professor at the School of Computer Science, Georgia Institute of Technology, and an Associate Professor at the University of Toronto (on leave). He previously held a NUS Presidential Young Professorship at the National University of Singapore. His research focuses on automated reasoning, aiming to enable computing systems to handle uncertain real-world environments through scalable techniques integrating randomized algorithms, statistical inference, formal methods, distribution testing, and software engineering. Core research areas: Automated Reasoning, Formal Methods, Approximate Model Counting, Probabilistic Inference, Constraint Solving His research group has achieved significant recognition in both individual awards and publications. Key trends in his recent work include advancing model counting algorithms, developing frameworks for probabilistic explanations, and improving scalability in formal verification and constraint satisfaction. His tools have consistently ranked top in international competitions, demonstrating practical impact in automated reasoning. 2019 NRF Fellowship for AI 2022 ACP Early Career Researcher Award 2020 IEEE Intelligent Systems AI's 10 to Watch Top placements in Model Counting, SAT, and CAV competitions He mentors a diverse group of PhD and Master's students and collaborates with institutions worldwide. His group's publications span premier conferences in AI, formal methods, and design automation, reflecting interdisciplinary contributions to theoretical and applied computer science.

• Theorem Proving
• Automated Reasoning
• Formal Methods
• +۱۴ مورد دیگر

Jasmin Blanchette is a Professor of Theoretical Computer Science and Theorem Proving at the Institute for Informatics, Ludwig-Maximilians-Universität München (LMU), where he also serves as Dean of Studies for Computer Science since January 2024. He is additionally affiliated as a guest researcher with the VeriDis group at Loria in Nancy, France. His research lies at the intersection of automated and interactive theorem proving, with a focus on higher-order logic and proof automation. Key projects include the development of tools like Sledgehammer, Nitpick, and Zipperposition, and foundational work on (co)datatypes and higher-order superposition. His recent publications reflect a strong trend in formalizing and verifying automated reasoning techniques, especially in higher-order logic, with applications in proof automation, SMT solving, and logical verification. Articles frequently appear in top venues such as CADE, ITP, and the Journal of Automated Reasoning. CADE 2023 Best Paper Award for 'Verified given clause procedures' FroCoS 2023 Best Paper Award (with Visa Nummelin and Sander Dahmen) IPA Dissertation Award (awarded to his student Petar Vukmirović) Dutch 'cum laude' distinction (awarded to his student Anne Baanen) Dutch Prize for ICT Research 2022 Blanchette has advised numerous PhD and postdoctoral researchers, many of whom are now active contributors to the formal methods community. He has received significant research grants through projects like Matryoshka and Nekoka. He is also the editor-in-chief of the Journal of Automated Reasoning and plays a central role in organizing key conferences such as ITP, CADE, and CPP. He leads an active research group at LMU, consisting of postdocs and PhD students working on topics such as higher-order superposition, formalization of voting systems, categorical logic, and proof search heuristics. The team collaborates closely with international groups, including those at Inria and TU Wien.

Vijay Ganeshمشاهده پروفایل

استاد

• SAT/SMT Solvers
• Artificial Intelligence
• Formal Methods
• +۵ مورد دیگر

Dr. Vijay Ganesh is a Professor of Computer Science at Georgia Institute of Technology, where he also serves as Associate Director of the IDEaS Institute and is affiliated with Tech AI. Previously, he held roles as Associate Professor (2018–2023) and Assistant Professor (2012–2018) at the University of Waterloo, and Research Scientist at MIT (2007–2012). He earned his PhD from Stanford University in 2007. His research focuses on SAT/SMT solvers and their applications in AI, software engineering, security, mathematics, and physics. Notable contributions include developing solvers like MapleSAT, Z3str4, and AlphaZ3, and exploring machine learning-augmented reasoning. He has led projects in logic for AI, proof complexity, and security of blockchain technologies. His awards include ACM Impact Paper (2019), ACM Test of Time (2016), and DATE’s Ten-Year Most Influential Paper (2008). He has advised startups like Quantstamp, a blockchain security firm, and co-directed the Waterloo AI Institute (2021–2023). His teaching includes courses on discrete mathematics, software engineering, and AI. Education: PhD in Computer Science, Stanford University (2007); Master’s in Electrical Engineering, Stanford (2000) Research Interests: SAT/SMT solvers, formal methods, automated testing, AI security, combinatorial mathematics Affiliations: Georgia Tech’s School of Computer Science, IDEaS Institute

• Theoretical Computer Science
• Theorem Proving
• Automated Reasoning
• +۲۶ مورد دیگر

Jasmin Blanchette is a Professor of Theoretical Computer Science and Theorem Proving at Ludwig-Maximilians-Universität München (LMU), where he also serves as the Dean of Studies for Computer Science since January 22, 2024. He is affiliated with the Institute for Informatics and leads the Theoretische Informatik und Theorembeweisen research unit. Additionally, he is a guest researcher in the VeriDis group at Loria, Nancy. Research Interests: His research centers on strengthening proof automation for general-purpose logics and enhancing the usability of proof assistants. He combines automatic and interactive methods, bridging human and artificial intelligence in formal verification. His work spans higher-order logic, automated and interactive theorem proving, formalization of mathematical results, and foundational mechanisms for (co)datatypes and (co)recursive functions. Key projects include Sledgehammer, Nitpick, Matryoshka, Nekoka, IsaFoL, and Lean Forward. Publication Trends: His recent publications (2023–2025) show a strong focus on higher-order automated reasoning, superposition calculus, proof automation in Isabelle/HOL, and formalization of logical and mathematical concepts. There is a consistent emphasis on verification, efficiency, and integration of SAT/SMT techniques into higher-order provers. Scientific Awards: FroCoS 2023 Best Paper Award (with Visa Nummelin and Sander Dahmen) CADE 2023 Best Paper Award for 'Verified given clause procedures' (with Qi Qiu and Sophie Tourret) IPA Dissertation Award (awarded to student Petar Vukmirović) Dutch Prize for ICT Research 2022 Advising and Grants: He supervises a large team of postdocs and PhD students at LMU and co-supervises students at other institutions. His leadership in major collaborative projects like Matryoshka indicates significant grant funding and collaborative research efforts. He is editor-in-chief of the Journal of Automated Reasoning and serves on numerous steering and program committees, reflecting strong academic leadership and visibility. Labs and Teams: He leads a research group at LMU’s Institute for Informatics, focusing on theorem proving and formal methods. He is also associated with the VeriDis group at Loria, Nancy, and collaborates widely across Europe in the automated reasoning community.

Alexey Ignatievمشاهده پروفایل

مدرس ارشد

• Artificial Intelligence
• Satisfiability Solving
• Automated Reasoning
• +۲ مورد دیگر

Alexey Ignatiev is a Senior Lecturer in Monash University's Department of Data Science & AI. His research develops SAT/SMT-based methods for AI applications including explainable AI, automated software debugging, and neuro-symbolic systems. Key projects: Formal Explainability for Neuro-Symbolic AI (ARC-funded) Hierarchical Abstractions for Neuro-Symbolic Systems Recent publications focus on formal explanation techniques for machine learning models, including defect prediction systems and interpretable rule extraction.

• Formal Methods
• Satisfiability (SAT)
• Satisfiability Modulo Theories (SMT)
• +۱۱ مورد دیگر

Enric Rodríguez Carbonell is a faculty member at the Department of Computer Sciences within the Faculty of Computer Science at Universitat Politècnica de Catalunya (UPC). He is a key member of the LOGPROG - Lògica i Programació research group, focusing on formal methods, automated reasoning, and combinatorial optimization. Research Interests: His work centers on satisfiability (SAT), satisfiability modulo theories (SMT), and their applications in program verification, constraint solving, and optimization. He investigates techniques such as conflict-driven learning, invariant generation, and Max-SMT for proving termination and safety. His research bridges theoretical foundations with practical applications in software analysis and industrial problem-solving. Publication Trends: His recent publications (2020–2024) show a sustained focus on enhancing SAT and SMT solvers, particularly in pseudo-Boolean reasoning, integer linear programming, and multi-conflict analysis. Earlier works established contributions in non-linear arithmetic, termination proofs, and efficient encodings for cardinality constraints, reflecting a long-term commitment to foundational and applied aspects of automated reasoning. Scientific Awards: Best student paper award at SAT 2024 Advising and Grants: Rodríguez Carbonell has contributed to multiple competitive R+D+i projects under Spain’s State Research Plans, indicating active grant involvement. He has co-authored doctoral theses and educational initiatives like Jutge.org, demonstrating engagement in academic supervision and pedagogical innovation. Labs and Teams: He is a core researcher in the LOGPROG group at UPC, which specializes in logic and programming, with strong collaborations across formal methods, verification, and constraint technologies.

Ruzica Piskacمشاهده پروفایل

استاد

• Software Verification
• Security and Applied Cryptography
• Automated Reasoning
• +۴ مورد دیگر

Ruzica Piskac is a Professor of Computer Science at Yale University, where she leads the Rigorous Software Engineering (ROSE) group. She has made significant contributions to the fields of software verification, security, automated reasoning, and code synthesis, focusing on improving software reliability and trustworthiness through formal techniques. Dr. Piskac received her PhD from the Swiss Federal Institute of Technology (EPFL) in 2011, where her dissertation won the Patrick Denantes Prize. Prior to joining Yale, she led an independent research group at the Max Planck Institute for Software Systems in Germany (2012-2013). Her research spans several key areas: symbolic execution for Haskell (G2), privacy-preserving formal methods (PPFM), functional reactive synthesis, verification of configuration files, and analysis of software updates. Her work consistently bridges theoretical formal methods with practical applications in real-world systems. Dr. Piskac's recent publications demonstrate a strong trend toward applying formal verification techniques to emerging challenges including large language models, quantum computing security, legal accountability of automated systems, and cyber-physical systems. Her research increasingly intersects with AI, cryptography, and legal domains while maintaining strong foundations in formal methods. Her scientific achievements have been recognized with numerous prestigious awards: Multiple Amazon Research Awards Yale University's Ackerman Award for Teaching and Mentoring Facebook Communications and Networking Award Microsoft Research Award for the Software Engineering Innovation Foundation (SEIF) Patrick Denantes Prize for her PhD dissertation Dr. Piskac has graduated five PhD students, four of whom have gone on to become assistant professors of computer science. She has served as Program Chair of the 37th International Conference on Computer Aided Verification and is on the Steering Committee of the Formal Methods in Computer-Aided Design conference. She leads the Rigorous Software Engineering (ROSE) group at Yale, which focuses on several key projects including: Symbolic Execution Engine for Haskell (G2) Privacy Preserving Formal Methods (PPFM) Functional Reactive Synthesis Verifications for Configuration Files Analysis of Software Updates and Configuration Files

Alan Huمشاهده پروفایل

استاد

• Formal Verification
• Algorithms
• Computer Architecture
• +۳ مورد دیگر

Alan Hu is a Professor in the Department of Computer Science at the University of British Columbia (UBC), part of the Faculty of Science. His research focuses on formal verification, algorithms, computer architecture, and electronic design automation. He teaches courses such as Intermediate Algorithm Design and Analysis (CPSC 320) and Introduction to Formal Verification and Analysis (CPSC 513). Dr. Hu has received notable awards, including the IEEE Council on Electronic Design Automation Outstanding Service Award and the IBM Faculty Award. His work emphasizes scalable verification techniques, SAT-based algorithms, and optimization in cloud computing and hardware systems. His research spans formal methods for hardware/software systems, including verification of embedded software, cache coherence, and network function virtualization. Notable contributions include advancements in SAT modulo theories, data race detection in heterogeneous systems, and cloud resource allocation frameworks like Cospot. Dr. Hu has been actively involved in teaching and curriculum development, consistently offering courses on algorithms, formal verification, and software design since 2000. His publications reflect a blend of theoretical foundations and practical applications in electronic design, cloud infrastructure, and verification tools. His scientific achievements include innovations in post-silicon validation, emulation-based coverage reduction, and formal analysis for debug trace optimization. He also contributes to the academic community through conference organization and editorial roles in formal verification and computer-aided design.

Zachary Kincaidمشاهده پروفایل

دانشیار

• Program Analysis
• Logic
• Programming Languages
• +۷ مورد دیگر

Zachary Kincaid is an Associate Professor in the Department of Computer Science at Princeton University. His research focuses on program analysis , logic , and programming languages , with emphasis on making analysis compositional and robust . PhD, University of Toronto (2016) BSc, Western University Research Interests Dr. Kincaid develops algebraic program analysis frameworks combining symbolic methods with abstract interpretation. His work addresses challenges in: Compositional analysis of concurrent and recursive programs Termination analysis for loops with complex control flow Non-linear numerical invariant generation Strategy synthesis for logical games Parameterized program verification Publication Trends His research output spans program analysis (2024-2010), formal verification (2018-2010), concurrency (2016-2010), and automated synthesis (2013-2012). Recent work (2024) explores polynomial ideals and nonlinear ranking functions , while foundational contributions include vector addition systems and recurrence-based invariants . Scientific Engagement Dr. Kincaid contributes to the academic community through: Program Committee service (PLDI, POPL, CAV, IJCAI, LICS, FMCAD, ESOP, etc.) Co-developing the Duet analyzer for unbounded concurrency Collaborative work with leading researchers (Tom Reps, Azadeh Farzan, Jason Breck) Advising & Grants He advises PhD students and leads research funded by the ONR grant N00014-19-1-2318 . Current advisees include Jake Silverman and Shaowei Zhu, while former student Charlie Murphy (PhD 2023) now holds a postdoctoral position at University of Wisconsin-Madison. Labs & Teams Dr. Kincaid co-developed the Duet program analyzer and contributes to tools like Srk and SimSat . His work integrates SMT solvers (MathSAT, Z3) and mathematical frameworks (rational vector addition systems, recurrence relations) for robust program analysis.

Philipp Wendlerمشاهده پروفایل

مدرس

• Software Verification
• Formal Methods
• Program Analysis
• +۵ مورد دیگر

Philipp Wendler is an academic lecturer in the Department of Computer Science at Ludwig-Maximilians-Universität München (LMU Munich). He is affiliated with the Software and Computational Systems Lab and actively involved in research, teaching, and open-source tool development. As an employee representative in the steering committee of the Institute of Informatics, he contributes to institutional governance. His research focuses on software verification, formal methods, and program analysis. Key projects include CPAchecker (a configurable verification framework) and BenchExec (a benchmarking tool). His work emphasizes practical applications in automated testing, energy-efficient algorithms, and reproducible benchmarking. Publications span topics like interpolation-based model checking, energy measurement tools, and strategies for software verification competitions. He has contributed to advancing predicate analysis, k-induction, and refinement selection techniques. Notable achievements include leading the development of CPAchecker and BenchExec, which are widely used in academic and industrial verification efforts. His research addresses challenges in scalable verification, flaky test analysis, and energy-aware computing.

Wenxi Wangمشاهده پروفایل

استادیار

• Formal Methods
• Machine Learning
• Software Engineering
• +۳ مورد دیگر

Dr. Wenxi Wang is an Assistant Professor in the Department of Computer Science at the University of Virginia, where he leads the Hiprel research group. He completed his PhD at the University of Texas at Austin under the supervision of Sarfraz Khurshid, with close collaborations with Kenneth McMillan and Darko Marinov. His research bridges software engineering, formal methods, and machine learning, focusing on enhancing software security and reliability through innovative techniques. Research Interests: Wang's interdisciplinary work explores: (1) Integration of deep learning (LLMs, GNNs) with automated reasoning tools like SAT/SMT solvers; (2) Enhancement of software verification tools (Verus, Dafny) using LLMs; (3) Improvement of ML model/framework reliability; and (4) Advanced code generation quality through verification. His group develops methods to combine formal methods with machine learning for robust software systems. Recent Publications: Wang's 15 most recent publications (2018-2024) demonstrate consistent focus on ML-formal methods integration, particularly in SAT solving, software verification, and testing. Key trends include GNNs for constraint solving, automated repair of security vulnerabilities, and novel testing methodologies for formal tools. His work appears in top venues including ICLR, ASE, ESEC/FSE, and ICSE. Awards and Honors: George J. Heuer, Jr. Ph.D. Endowed Graduate Fellowship (2023-2024) Rising Stars in EECS (2022) Research Group: Leads the Hiprel Group with 6 members: PhD Students: Zichen Xie (ML for verification), Lize Shao (LLMs for SE) Master's: Chaitanya Shahane (LLMs for testing) Undergraduate: Carter Opperman (SAT solving) Interns: Tianyi Huang (ML for SAT), Mrigank Pawagi (LLMs for protocol verification)

• Computer Science
• Formal Methods
• Programming Languages
• +۱ مورد دیگر

André de Matos Pedro is an Assistant Professor in the Department of Computer Science at the University of Beira Interior. He teaches courses including Teoria da Computação (Theory of Computation), Programação Funcional (Functional Programming), and Segurança e Fiabilidade de Software (Software Security and Reliability). His research focuses on formal methods, runtime verification, and programming language theory. His publication record shows consistent focus on formal verification methods applied to real-time and embedded systems. Recent work emphasizes runtime monitoring frameworks, SAT/SMT-based verification techniques, and applications in safety-critical domains like autopilot systems. The research trajectory demonstrates increasing emphasis on practical applications of temporal logic and co-simulation testing platforms.

Carsten Fuhsمشاهده پروفایل

مدرس ارشد

• Program Analysis
• Termination
• Complexity Bounds
• +۵ مورد دیگر

Carsten Fuhs is a Senior Lecturer at the School of Computing and Mathematical Sciences at Birkbeck, University of London . His research focuses on Program Analysis , Termination , Complexity Bounds , and Term Rewriting , with applications in Verification and SAT Encodings . Research Group Lead of the Logical Methods research group (2023–present) Member of the Board of Trustees for CADE (2023–present) Chair of the Bill McCune PhD Award Expert Committee (2024, 2025) Active in conference organization and program committees (FSCD, IJCAR, LOPSTR, etc.) Research Interests : Carsten Fuhs specializes in automated termination and complexity analysis for term rewriting and programming languages. His work leverages SAT solving and constraint-based methods to develop tools like AProVE for program verification. Key areas include parallel term rewriting , higher-order dependency pairs , and memory safety proofs . Selected Publications Trends : Recent articles emphasize higher-order rewriting (2025), parallel complexity analysis (2024), and modular termination proofs (2022–2024). Earlier work (2014–2017) explores pointer arithmetic verification , separation logic , and integer program complexity . Scientific Awards : Best Paper Award, LOPSTR 2022 Teaching and Mentoring : Carsten Fuhs has lectured on Java programming , compilers , and term rewriting at Birkbeck and international summer schools. He contributes to SAT competitions as a benchmark submitter and organizes regional programming language seminars like S-REPLS 10 (2018).

Danny Bøgsted Poulsenمشاهده پروفایل

دانشیار

• Formal Methods
• Model Checking
• Cyber-Physical Systems
• +۳ مورد دیگر

Danny Bøgsted Poulsen is an Associate Professor at the Department of Computer Science, Aalborg University, affiliated with The Technical Faculty of IT and Design. His research focuses on formal methods, model checking, and cyber-physical systems with applications in security analysis and programming languages. He contributes to projects like BEO-COVID (2020–2020) and IDEA4CPS (2011–2015), which explore decision support tools and foundational cyber-physical systems. His academic background includes advanced work in formal verification and statistical model checking. Key research interests include: Formal methods for string constraints and SMT solvers Statistical analysis of security-critical systems Modelling protocols like DTLS and attack-defense scenarios Applications of formal methods in education and public health Recent work highlights include developing SMTQuery for benchmark analysis, statistical evaluation of bit-flip vulnerabilities, and leveraging large language models for educational feedback. His research outputs span over 36 publications across journals and conferences, with active contributions to UPPAAL tool development and open datasets for reproducibility. Poulsen collaborates internationally on projects involving formal verification of embedded systems and cybersecurity protocols. His work bridges theoretical computer science with practical applications in safety-critical systems.

Jasmin Blanchetteمشاهده پروفایل

استاد

• Theorem Proving
• Formal Verification
• Automated Reasoning
• +۴ مورد دیگر

Prof. Dr. Jasmin Blanchette is a faculty member at the Ludwig Maximilian University of Munich, holding the chair in Theoretical Computer Science and Theorem Proving . She serves as Dean of Studies for Computer Science and collaborates with the VeriDis group at Loria, Nancy. Her research focuses on combining automatic and interactive theorem proving to enhance proof automation for critical systems and mathematical research. Key Research Areas: Higher-order logic, formal verification, superposition calculus, proof assistants (Isabelle/HOL, Lean), definitional mechanisms for (co)datatypes. Recent Articles address advanced topics in higher-order reasoning, SMT integration, and algorithm verification. Scientific Recognition: Co-awarded best papers at FroCoS 2023 and CADE 2023. Supervises a team of postdocs and PhD students working on projects like Matryoshka and Nekoka. Her tools (Sledgehammer, Nitpick) are widely used in formal methods.