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

Holger H. Hoosمشاهده پروفایل

استاد

• Algorithmics
• Bioinformatics
• Computational Intelligence
• +۹ مورد دیگر

Holger H. Hoos is a Professor at the University of British Columbia's Computer Science Department, affiliated with the Institute for Computational Intelligence and Cognitive Systems (ICICS) and the Peter-Wall Institute for Advanced Studies. As of 2017, his primary affiliation shifted to Leiden University (Netherlands), though he remains connected to UBC. His research focuses on algorithmics, bioinformatics, computational intelligence, and computer music, with significant contributions to stochastic local search, empirical algorithmics, and SAT solving. Education: Ph.D. (Dr.rer.nat) in Computer Science from TU Darmstadt (1998), postdoctoral fellow at UBC. He has led the BETA Lab and SALIERI Project, exploring biomolecular structure prediction and music algorithms. Research interests span stochastic algorithms, RNA structure prediction, automated algorithm configuration, and interdisciplinary applications like flow cytometry analysis. His work bridges theoretical foundations with empirical methods, emphasizing practical problem-solving. Awards include the AAAI Fellowship, multiple best paper awards (GECCO 2020, IJCAI-JAIR 2010), and leadership roles in conferences like AAAI and LION. He has advised over 30 students, contributing to impactful projects in bioinformatics and AI. Labs/Teams: Founder of the BETA Lab (Bioinformatics, Theoretical and Empirical Algorithms), member of the Laboratory for Computational Intelligence (LCI), and collaborator on SALIERI (Computer Music).

Joan Espasa Arxerمشاهده پروفایل

مدرس

• Automated Planning
• Artificial Intelligence
• Constraint Programming
• +۵ مورد دیگر

Dr Joan Espasa Arxer is a Lecturer in the School of Computer Science at the University of St Andrews, specializing in the AI group. His research focuses on Automated Planning, Constraint Programming, and applications of logic in computer science. He holds a position in the Department of Computer Science and teaches courses such as CS4402 - Constraint Programming and CS4303 - Videogames, while supervising projects across various academic levels. Research interests include Classical and Numeric AI Planning, Boolean Satisfiability (SAT), Satisfiability Modulo Theories (SMT), Planning as Satisfiability, Constraint Programming, and Automated reformulation of models. His work addresses challenges in planning domain modeling, benchmark instance generation, and cross-paradigm problem solving. Recent publications explore lifted planning with constraints, international planning competitions, and modeling pipelines in AI. He collaborates on tools like the 2023 International Planning Competition dataset and frameworks for generating benchmark instances. Advises PhD students Mustafa Abdelwahed and Carla Davesa Sureda. Engages in community outreach through events like 'Doors Open @ Computer Science' and contributes to open-source tools for planning and constraint satisfaction.

• Formal Verification
• Automated Reasoning
• SAT and SMT Solving
• +۷ مورد دیگر

Bernd Becker is a Professor in the Department of Computer Science at the Faculty of Engineering, University of Freiburg, Germany. He has been actively publishing in the fields of formal methods, hardware verification, and automated reasoning since the 1980s, with a sustained record of high-impact publications up to 2025. His research interests span formal verification, SAT and SMT solving, hardware testing, probabilistic systems, and embedded systems security. His work bridges theoretical advances in automated reasoning with practical applications in processor design, RISC-V verification, and safety-critical systems. The recent articles highlight a strong focus on applying formal methods to emerging challenges in hardware and AI, including POMDPs for robot planning, RISC-V security, GPU verification, and energy-efficient monitoring. There is a clear trend toward integrating symbolic computation with machine learning and probabilistic reasoning. Bernd Becker has collaborated extensively with researchers such as Ralf Wimmer, Ilia Polian, and Matthias Sauer, indicating leadership in a large, interdisciplinary research group. His work has been supported by numerous grants, though specific details are not listed in the source text. He has contributed to major conferences such as DATE, FMCAD, and SAT, and has mentored several students and researchers, though specific names are not provided. He is involved in projects related to secure scan networks, physical unclonable functions, and smart home systems.

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

مدرس ارشد

• Automated Termination and Complexity Analysis
• Program Equivalence
• Verification
• +۴ مورد دیگر

Carsten Fuhs is a Senior Lecturer at the School of Computing and Mathematical Sciences, Birkbeck, University of London, where he leads the Logical Methods research group (since 2023). His research focuses on automated reasoning for program analysis, including termination/complexity analysis (via the AProVE tool), program equivalence, verification, term rewriting, and SAT solving. He contributes to the SAT4J library and has benchmarked SAT encodings for international competitions. Fuhs's work bridges theoretical foundations and practical tools, with recent emphasis on higher-order rewriting, parallel complexity, and equivalence checking. His publications consistently appear in premier venues (e.g., ESOP, IJCAR, JAR), demonstrating innovations in automating program analysis. He holds significant service roles: Trustee for CADE, Executive Committee member for ACM SIGLOG, Publicity Chair for FSCD, and Co-Chair of IFIP WG 1.6 on Rewriting. He organized the 10th S-REPLS workshop and lectures at international schools (e.g., ISR, SAT/SMT/AR). At Birkbeck, he teaches core programming courses (e.g., Java, Software Programming I/II) and previously taught Compilers at UCL and Term Rewriting at RWTH Aachen.

• Formal Methods
• Model Checking
• Satisfiability (SAT) Solving
• +۴ مورد دیگر

Tommi Junttila serves as a Senior University Lecturer in the Department of Computer Science at Aalto University, Finland, where he conducts cutting-edge research at the intersection of formal methods and computational logic. His academic profile demonstrates sustained contributions to theoretical computer science with practical applications in system verification and blockchain technology. His research program centers on advancing formal verification techniques, with core expertise in: Symmetry reduction algorithms for state space explosion SAT/SMT solving with specialized parity and XOR reasoning Bounded model checking of timed and asynchronous systems Blockchain protocol verification (notably DeFi lending pools) Canonical labeling tools for graph automorphism detection Recent work shows increasing focus on decentralized finance applications while maintaining foundational contributions to solver technology. Analysis of his publication trajectory (2011-2022) reveals consistent innovation in SAT solving methodologies, with symmetry reduction and parity reasoning forming persistent research threads. His 2022 work on DeFi lending pools represents a strategic expansion into blockchain verification, leveraging established formal methods expertise for emerging financial technologies. Tool development (bliss, PySMT) demonstrates commitment to practical research impact. No scientific awards were documented in the source materials. Similarly, no information regarding student supervision, grant funding, or laboratory affiliations was present in the provided text. His independent tool development (including bliss for graph canonical labeling and PySMT for SMT solver interfaces) indicates significant technical leadership within the formal methods community.

• Automated Reasoning
• Formal Methods
• Program Verification
• +۳ مورد دیگر

Laura Kovacs is a Professor at TU Wien's Research Area Formal Methods in Systems Engineering. Her work focuses on automated reasoning, symbolic computation, and formal verification of (probabilistic) programs. She leads projects like Automated Reasoning with Theories and Induction and Effective Formal Methods for Smart-Contract Certification . Key research areas: Automated Reasoning, Formal Methods, SMT Solving Projects: Game-Theoretic Security, Probabilistic Loop Analysis Recent publications emphasize SAT-based subsumption, induction in saturation, and algebraic loop reasoning. Her team includes researchers like Marcel Moosbrugger and Sophie Rain. She contributes to tools like Vampire and Z3 for symbolic attackers and finite field reasoning.

• Artificial Intelligence
• Knowledge Representation
• Constraint Answer Set Programming
• +۴ مورد دیگر

Dr. Yuliya Lierler is a Professor in the Department of Computer Science at the University of Nebraska Omaha's College of Information Science & Technology. She has been a faculty member since 2012, reaching the rank of full professor, and was appointed to the Cheryl Prewett Diamond Professorship in 2020. Her work focuses on artificial intelligence, particularly in knowledge representation, automated reasoning, and declarative problem solving. PhD in Computer Science (University of Texas at Austin, 2010) Dr. Lierler's research bridges logic programming with practical AI applications, including natural language understanding, constraint satisfaction, and SMT-based solvers. She is a co-director of the NLPKR lab and has authored over 70 peer-reviewed publications in venues like Artificial Intelligence Journal and AAAI. Her contributions include open-access textbooks and tools like text2alm for semantic information extraction. Her recent publications explore advancements in answer set programming (ASP) semantics, automated reasoning frameworks, and hybrid knowledge representation systems. She has served as program co-chair for major conferences like ICLP (2022) and PADL (2017), and received awards such as the IS&T Outstanding Research Award (2024). Dr. Lierler also mentors students and leads initiatives in teaching innovation through online education and professional development programs. Mentor of the Year Award, Aksarben Foundation (2025) IS&T Outstanding Research and Creativity Award (2024) Best Student Paper Award (with Amelia Harrison, 2016) Dr. Lierler contributes to academic service through leadership roles in international conferences and program committees. Her lab, NLPKR, focuses on integrating natural language processing with formal logic, while her teaching emphasizes formal methods and AI foundations.

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

Hans-Jörg Schurr is a Research Fellow at the University of Iowa , working on the award-winning SMT solver cvc5 and developing the Eunoia language for SMT proof certificates. He previously earned his PhD at Inria Nancy Grand Est under the supervision of Pascal Fontaine, Jasmin Blanchette, and Stephan Merz. Research Interests : SMT solvers, formal proof certification, expressive type systems, quantifier instantiation, strategy scheduling. Teaching : Taught Programming Language Concepts and Logic in Computer Science at University of Iowa; led software engineering projects and REST API courses at Polytech Nancy. Leadership : Lead developer of veriT and schedgen , co-maintainer of the SMT-LIB benchmark library. Scientific Contributions span proof reconstruction pipelines in Isabelle/HOL, novel SMT proof formats like Alethe and Eunoia, and empirical strategy optimization via linear programming. His work focuses on making SMT solvers more useful through formal methods and type systems. Scientific Awards : Best Paper by a Junior Researcher (2021) Thank-a-Teacher Letter (2023) Recognized by graduating class of 2023 Service : Participated in program committees for SMT, SBMF, and artifact evaluation committees for ICFP and TACAS. Reviewed for journals like Science of Computer Programming and International Journal on Software Tools for Technology Transfer .

Marcello M. Bersaniمشاهده پروفایل

دانشیار

• Formal Methods
• Robotics
• Digital Twins
• +۴ مورد دیگر

Marcello M. Bersani is an Associate Professor at the DeepSE Lab within the Department of Electronics, Information and Bioengineering at Politecnico di Milano . His research focuses on Formal Methods applied to robotic systems and Digital Twins, with a particular emphasis on temporal logics and decision procedures based on SAT/SMT techniques.

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

استاد

• SAT/SMT Solvers
• Automated Reasoning
• Software Verification
• +۲ مورد دیگر

Vijay Ganesh is Professor of Computer Science at Georgia Tech and Associate Director of the IDEaS Institute. His research develops foundational methods for SAT/SMT solving and AI verification. Research areas: Hybrid machine learning and reasoning systems Automated software verification Computational complexity of solvers Awards include: ACM Test of Time Award Google Faculty Research Awards IBM Faculty Award He leads projects including MapleSAT solver and Z3Alpha verification framework.

Neeldhara Misraمشاهده پروفایل

دانشیار

• Design and analysis of algorithms
• Computational social choice
• Parameterized complexity
• +۵ مورد دیگر

Neeldhara Misra is an Associate Professor in the Department of Computer Science & Engineering at the Indian Institute of Technology Gandhinagar (IITGN). She holds the Smt. Amba and Sri. V S Sastry Chair position. Prior to this, she served as an Assistant Professor at IITGN (2015–2021), and held an INSPIRE Faculty Fellowship at the Indian Institute of Science (2013–2015). Her research focuses on algorithm design, computational social choice, extremal combinatorics, and combinatorial game theory. Education : BSc in Mathematics from Mount Carmel College, Bangalore (2007) PhD in Theoretical Computer Science from The Institute of Mathematical Sciences, Chennai (2012) Research Interests : Her work spans parameterized complexity, algorithm design for combinatorial problems, and applications in social choice theory. Recent contributions include studies on equitable fair division, eternal vertex cover numbers in graphs, and efficient algorithms for graph problems like perfect matching cuts. Professional Activities : She has actively contributed to organizing conferences such as FSTTCS, IPEC, and AAMAS. Her work has been recognized with awards like the NASI Platinum Jubilee Young Scientist Award (2023). Awards : NASI Platinum Jubilee Young Scientist Award (2023) Grants & Advising : Details on grants or advising are not explicitly listed in the provided texts, though her involvement in interdisciplinary research and academic service is notable.

• Answer-Set Programming (ASP)
• Explainable AI
• Logic in Artificial Intelligence
• +۳ مورد دیگر

Tobias Geibinger is a PreDoc Researcher at the Institute of Logic and Computation of Vienna University of Technology , supported by a DOC Fellowship from the Austrian Academy of Sciences. His work focuses on explainability in Answer-Set Programming (ASP), particularly for advanced language features and hybrid ASP systems. Education: BSc, Dipl.-Ing. (Master's equivalent) in Computer Science Projects: CD Laboratory for AI and Optimization (2017–2025), KIRAS-PrEMI (2019–2022), ARTIS (2017–2025) His research combines logic programming with constraint programming and hybrid methods to solve industrial scheduling problems. This includes automated test laboratory scheduling, photolithography job scheduling, and pandemic-era physician scheduling. Recent work investigates neurosymbolic integration and contrastive explanation frameworks. Selected publications analyze ASP optimization techniques for parallel machine scheduling, large-neighborhood search strategies, and nonmonotonic paraconsistent logics. These contributions align with broader trends in declarative AI and logic-based optimization. Scientific Recognition: ASAI Master Thesis Prize (2023)

• Formal Verification
• Programming Languages
• Term Rewriting Systems
• +۵ مورد دیگر

Ștefan Ciobaca is a researcher at the Faculty of Computer Science of the Alexandru Ioan Cuza University of Iasi , Romania. His work focuses on formal verification, programming language theory, and security protocols, with significant contributions to reachability logic and term rewriting systems. He actively mentors students in Dafny and F* verification techniques and develops tools for program equivalence proofs. Research Interests : Formal verification of cryptographic protocols, reachability logic, program equivalence, term rewriting systems, static analysis tools, and unification modulo builtins. Key Contributions : Developed the AKiSS tool for security protocol verification and contributed to the K Framework for programming language semantics. Students : Supervised multiple BSc/MSc theses on algorithm verification using Dafny and F*, including projects on SAT solvers, string algorithms, and data structure correctness. Collaborations : Partnered with Bitdefender on static analysis tool development and participated in international conferences like POPL, ICFP, and IJCAR. His recent work includes verifying image compression algorithms in Dafny and developing educational tools for logic-based program verification.

Marijn Heuleمشاهده پروفایل

دانشیار

• Satisfiability (SAT) Solving
• Formal Verification
• Combinatorial Mathematics
• +۵ مورد دیگر

Marijn Heule is an Associate Professor in the Computer Science Department at Carnegie Mellon University. He received his PhD from Delft University of Technology in the Netherlands. His academic career has been focused on advancing the theory and practice of satisfiability (SAT) solving and its applications. Dr. Heule's research primarily centers on solving hard combinatorial problems in formal verification, number theory, and extremal combinatorics. His work has made significant contributions to both theoretical foundations and practical implementations of SAT solvers. He has developed award-winning SAT solvers, and his preprocessing techniques are incorporated into state-of-the-art SAT solvers used worldwide. His current research focuses on two major challenges: exploiting high-performance computing for SAT solving and validating results from SAT solvers and related tools. Dr. Heule pioneered the "cube-and-conquer" paradigm, a novel parallel SAT solving approach that enables linear time speedups on many hard problems. His first publication on this topic won the best paper award at HVC 2011. He also designed a new proof format with a corresponding fast proof checker for SAT and QBF solvers. This proof logging format has been mandatory for SAT Competitions since 2013, significantly increasing confidence in tool correctness. His work on the Boolean Pythagorean Triples problem, which produced a 200 TB proof that was validated, demonstrated that proof logging and verification is feasible even for the most complex problems. Dr. Heule is one of the editors of the 900+ page "Handbook of Satisfiability," which has become a standard reference in the SAT community. He serves as an Associate Editor of the Journal on Satisfiability, Boolean Modeling and Computation and previously co-chaired the SAT 2015 conference in Austin. Best paper award at HVC 2011 for cube-and-conquer publication Multiple best paper awards/nominations at major conferences including IJCAR, SAT, TACAS Work featured in New York Times, Quanta Magazine, Nature, and other major media outlets Dr. Heule has advised several PhD students including Emre Yolcu, Joseph Reeves, Bernardo Subercaseaux, Cayden Codel, James Gallicchio, and Amar Shah. He has developed important software tools including DRAT-trim (a proof checking utility), QRAT-trim, and implementations of the cube-and-conquer paradigm that have become standard in the SAT solving community.

Ashutosh Guptaمشاهده پروفایل

دانشیار

• Formal Verification
• Software Verification
• Model Checking
• +۷ مورد دیگر

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.