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

• Embedded Systems
• Synchronous Languages
• Theorem Proving
• +۸ مورد دیگر

Timothy Bourke is a Researcher at Inria in the PARKAS team , affiliated with the Informatics Department of École normale supérieure (ENS) . He also serves as an Adjunct Professor at the Informatics Department of École Polytechnique , contributing to both institutions' academic and research missions. Research Focus: His work centers on rigorous approaches to modeling, programming, and verifying embedded control systems. This includes developing and analyzing Vélus (Verified Lustre) and Zélus (synchrony + ODEs) , integrating formal methods with practical applications like robotic wheelchair control systems, infrared sensors, microkernel operating systems, microprinter components, and wireless routing protocols. Academic Service: Active in program committees for conferences including DAC , ECRTS , EMSOFT , iFM , JFLA , and SETTA , including chairs/co-chairs at ESOFT 2019 , JFLA 2022-2023 , and SETTA 2024 . Regular reviewer for journals like ACM Transactions on Embedded Computing Systems and Real-Time Systems . Students: Advised Guillaume Baudart (2013–2017), Lélio Brun (2016–2020), Paul Jeanmaire (2020–2024), and Basile Pesin (2020–2023). Labs/Teams: Core member of the PARKAS team at Inria, focusing on embedded systems and synchronous language design. His technical contributions include software tools like Muttlight , Sundials/ML , and Urpal for timed trace inclusion testing. He also teaches courses such as L3 at ENS , MPRI INF559 , and CSE205 at École Polytechnique .

Julie Caillerمشاهده پروفایل

دانشیار

• Automated Deduction
• Theoretical Computer Science
• Formal Methods
• +۶ مورد دیگر

Julie Cailler is an Associate Professor at the University of Lorraine, affiliated with CNRS, Inria, and LORIA in Nancy, France. She is a member of the VeriDis Team and focuses on automated deduction, interactive proof systems, and logic in computer science. PhD in Theoretical Computer Science from the University of Montpellier (2023) Former Associate Professor at the University of Regensburg Her research interests include: Designing concurrent and parallel decision procedures for first-order logic Integration of automated and interactive theorem proving Proof system interoperability and formal verification Recent publications highlight her work on: SC-TPTP format extensions for sequent-based proofs (CADE-30, 2025) Graph Neural Networks for word equation solving (ATVA 2024, 2025) Deskolemization strategies in first-order logic (LPAR 25, 2024) Scientific recognition: Woody Bledsoe Award (2022) Best Newcomer Prover (CASCJ11, 2022) She supervises students in projects related to: Automated theorem prover development Logic programming and deduction modulo theory Formal verification and proof tool integration Julie is actively involved in academic service as: Co-head of GT LVP (Languages and Program Verification) working group PC member for major conferences like FMCAD, FSTTCS, and ITP

Paige Randall Northمشاهده پروفایل

استادیار

• Category Theory
• Homotopy Theory
• Functional Programming
• +۳ مورد دیگر

Paige Randall North is an Assistant Professor at Utrecht University, holding dual appointments in Mathematics and Information and Computing Sciences. She is also an Honorary Research Fellow at the University of Birmingham and a Guest Researcher at Delft University of Technology. Her research focuses on applying category theory and topology to computer science, particularly in functional programming and homotopy theory. North earned her PhD in Mathematics from the University of Cambridge (supervised by Martin Hyland) and a BS from the University of Chicago. She has held postdoctoral positions at the University of Pennsylvania and Ohio State University. Her research explores connections between type theory and higher category theory, including the univalence principle and categorical diffusion. Recent activities include organizing conferences like TYPES and DutchCATS, serving on program committees for LICS and POPL, and teaching advanced courses on homotopy type theory and interactive theorem provers. Funding has come from the AFOSR (2021-2024). Her work emphasizes formalization in proof assistants like UniMath and Coq, with contributions to categorical semantics and bicategorical type theory.

Alastair F. Donaldsonمشاهده پروفایل

استاد

• Programming Languages
• Compilers
• Verification
• +۲ مورد دیگر

Alastair F. Donaldson is a Professor in the Department of Computing at Imperial College London's Faculty of Engineering, where he leads the Multicore Programming Group. He also works as a Software Engineer at Google in the Android Graphics Team. Previously, he served as Director of GraphicsFuzz, an Imperial College spinout company acquired by Google in 2018. His research spans programming languages, compilers, verification, and testing, with a particular focus on randomized and fuzz testing techniques for compilers and program analyzers. Donaldson has developed several influential testing frameworks including GraphicsFuzz, RustSmith, and GrayC, which have significantly advanced compiler testing methodologies. Analysis of his recent publications reveals a strong trend toward practical applications of compiler testing techniques across diverse domains including GPU programming, verification-aware languages, and memory models. His work increasingly incorporates continuous integration practices and focuses on addressing real-world challenges in compiler development and verification. Donaldson maintains active involvement in the programming languages research community, serving on program committees for major conferences including PLDI, POPL, ASPLOS, and SPLASH. He has contributed significantly to advancing compiler testing methodologies and has mentored numerous researchers through PLMW (Programming Languages Mentoring Workshop). He leads the Multicore Programming Group at Imperial College London, which focuses on challenges in parallel and concurrent programming. His work bridges theoretical computer science with practical software engineering challenges, particularly in the areas of compiler correctness and verification.

Michael H. Borkowskiمشاهده پروفایل

استاد آموزشی

• Software Verification
• Type Theory
• Interactive Theorem Provers
• +۳ مورد دیگر

Michael H. Borkowski is an Assistant Teaching Professor in the Department of Computer Science at Purdue University. He earned his Ph.D. from the University of California, San Diego (UCSD), specializing in software verification, type theory, and interactive theorem provers. His research focuses on developing techniques to ensure software correctness and performance through formal methods. Ph.D., UCSD Computer Science (2024) M.S., UCSD Computer Science (2019) B.A., Amherst College Computer Science (2016) His research interests include refinement types, functional programming, and mechanizing proofs. Recent work emphasizes software verification tools (e.g., the 2024 POPL publication on refinement types). Earlier contributions span plant biology and applied mathematics, including studies on auxin gradients and wood grain modeling. Notable awards include the Computer Science Prize and Phi Beta Kappa from Amherst College. Teaching roles include courses at UCSD (e.g., CSE 20 Discrete Mathematics) and Purdue. He was affiliated with UCSD’s ProgSys Group during his Ph.D.

Louis Salvailمشاهده پروفایل

استاد

• Quantum Computing
• Cryptography
• Quantum Cryptography
• +۴ مورد دیگر

Louis Salvail is a Full Professor at the University of Montréal’s Department of Computer Science and Operations Research, affiliated with the Laboratory for Theoretical and Quantum Computing (LITQ). He joined the university in 2008 after working at Aarhus University from 1998 to 2008, where he contributed to classical cryptography foundations. His primary research interests are quantum-classical cryptography and quantum information theory, with a focus on theoretical problems. He teaches courses like Cryptology and Quantum Computing. Research projects include leadership on quantum cryptography protocols and collaborations in quantum networks. Notable grants include those from NSERC (Canada) and FQRNT, focusing on quantum cryptography foundations and quantum communication technologies. He has advised numerous PhD and Master’s students on topics like quantum key distribution protocols and cryptographic security. Salvail holds a 1998 PhD from Université de Montréal under Gilles Brassard and Claude Crépeau.

Hongjin Liangمشاهده پروفایل

دانشیار

• Programming Languages
• Formal Verification
• Concurrency Theory
• +۳ مورد دیگر

Hongjin Liang is an Associate Professor at the School of Computer Science , Nanjing University , China. He is an active researcher and educator in the fields of programming languages and formal verification, with a strong focus on concurrency theory, mechanized proofs, and memory models. Education: PhD in Computer Science (May 2014), dissertation titled Refinement Verification of Concurrent Programs and Its Applications . Research Interests: His research spans formal verification , concurrent programming , memory models , and mechanized reasoning . He is particularly known for his work on verifying concurrent data structures, program logics for concurrency, and certified compilation. He is a member of the PLaX research group . Publications and Impact: Liang has published extensively in top-tier venues such as POPL, PLDI, ESOP, TOPLAS, and CSL-LICS. His work often involves formalizing and verifying complex concurrent systems using interactive theorem provers like Rocq/Coq. Notable contributions include verifying compiler optimizations under weak memory models and developing program logics for randomized concurrent programs. Scientific Awards: Distinguished Paper Award , PLDI 2019 for "Towards Certified Separate Compilation for Concurrent Programs" Teaching and Advising: He teaches undergraduate and graduate courses including Formal Semantics of Programming Languages , Concurrency: Algorithms and Theories , and Compiler Design . He has supervised graduate students and served on numerous program committees for international conferences. Affiliations: He is affiliated with the PLaX research group at Nanjing University and has collaborated with researchers such as Xinyu Feng, Zhong Shao, and Jan Hoffmann.

A.E. Zaidmanمشاهده پروفایل

استاد

• Software Testing
• Test Amplification
• Mutation Testing
• +۶ مورد دیگر

A.E. Zaidman is a Professor in the Software Technology department at Delft University of Technology's Faculty of Electrical Engineering, Mathematics and Computer Science. His research focuses on software testing, code quality, and developer tooling, with recent emphasis on socio-technical factors, environmental impacts of testing, and GitHub Actions workflows. Key Research Areas Test amplification (developer interactions with automated testing) Code smell detection and its impact on software quality Empirical studies in open-source software testing AI/ML applications in test generation and analysis Scientific Awards Best Artifact Award (2022) Best Emerging Results Paper Award (2018) Best ERA paper award (2015) Best tool demo paper award (2017) ICPC 2009 Best Paper Award Recent Publications 2025: Systematic mapping of qualitative software testing methods 2025: Industrial language engineering case studies using Spoofax 2024: Environmental impact analysis of Java testing 2024: GitHub Actions workflow smell investigations

Albert Qiaochu Jiangمشاهده پروفایل

پژوهشگر ارشد

• Machine Learning
• Theorem Proving
• Artificial Intelligence
• +۳ مورد دیگر

Albert Qiaochu Jiang serves as a Visiting Research Fellow at the Department of Computer Science and Technology, University of Cambridge. His research integrates machine learning with formal theorem proving, focusing on neural theorem provers and mathematical reasoning systems. He leads the reasoning team at Mistral AI while maintaining academic supervision at Cambridge. His research interests center on machine learning for theorem proving , with specific expertise in neural-symbolic integration, autoformalization, and large language models for mathematical reasoning. His work bridges artificial intelligence with formal verification, developing systems that enhance automated reasoning capabilities through neural networks. Current projects involve improving premise selection for theorem provers, multilingual mathematical formalization, and creating efficient architectures for mathematical language models. Analysis of his recent publications reveals a strong focus on advancing neural theorem proving through innovative architectures like Target-Based Automated Conjecturing and Magistral. His research trajectory shows increasing sophistication in integrating language models with formal verification systems, with significant contributions to datasets like Numinamath and frameworks like Llemma. Key trends include optimizing compute efficiency in proof generation, enhancing multilingual mathematical reasoning, and developing interactive human-AI collaboration systems for formal mathematics. While no scientific awards are currently documented in available sources, his research output demonstrates significant impact in the intersection of AI and formal methods. As leader of Mistral AI's reasoning team, Jiang directs research on neural theorem proving systems while contributing to academic supervision at Cambridge. His work involves substantial industrial-academic collaboration, leveraging resources from both institutional contexts to advance mathematical AI. Current projects focus on creating practical systems for mathematical automation with real-world verification applications. His research operates at the intersection of academia and industry through Mistral AI's reasoning team, where he develops neural theorem proving systems with practical applications in formal verification. This dual affiliation enables rapid translation of theoretical advances into deployable tools for mathematical automation.

• Dependent Type Theory
• Verification
• Interactive Theorem Proving
• +۵ مورد دیگر

Talia Ringer is an Assistant Professor at the University of Illinois Urbana-Champaign, affiliated with the Grainger College of Engineering and the Siebel School of Computing and Data Science. Her research focuses on proof engineering, formal verification, and bridging neural and symbolic proof automation. She holds a PhD in Computer Science from the University of Washington and a BS in Mathematics and Computer Science from the University of Maryland. Prior to academia, she worked at Amazon as a software engineer. Ringer is known for founding initiatives like SIGPLAN-M and the Computing Connections Fellowship, fostering inclusivity in computer science research. She has received prestigious awards including the 2023 ACM SIGPLAN Distinguished Service Award and the DARPA Young Faculty Award. Education: PhD, University of Washington (2021); BS, University of Maryland (2012) Research Areas: Dependent Type Theory, Verification, Interactive Theorem Proving, Proof Automation, Formal Methods Awards: ACM SIGPLAN Distinguished Service Award (2023), ESEC/FSE Distinguished Paper Award (2023), DARPA Young Faculty Award (2023) Her work emphasizes making formal verification accessible to programmers through tools like Proof Repair and Baldur , while advocating for ethical AI research and LGBTQ+ inclusivity. She advises a diverse team of graduate and undergraduate students in the Illinois Theorem Provers (ITP) lab, exploring topics including proof repair, reinforcement learning for proofs, and quotient type equivalences.

• Software Engineering
• Formal Methods
• Model-Driven Engineering
• +۳ مورد دیگر

Chen-Wei Wang is an Associate Professor (Teaching Stream) in the Electrical Engineering & Computer Science (EECS) department at York University's Lassonde School of Engineering. He holds a DPhil in Computer Science from the University of Oxford, specializing in Software Engineering. His career includes post-doctoral research at McMaster Centre for Software Certification and York University Software Engineering Lab, focusing on certification of safety-critical systems. He previously taught at SUNY Korea and joined York University in 2017, where he coordinates experiential labs and emphasizes pedagogical innovation. He became an Eng. L. (Engineering Licensee) in 2020 and received tenure in 2022. Education: B.A. (summa cum laude) in Computer Science from York University (2006); DPhil in Computer Science from Oxford (2011). Research interests span formal verification of software systems, model-driven engineering, and computing education. Notable collaborations include work with Ontario Power Generations and Systemware Innovation. Research focuses on automated verification, real-time systems, and pedagogical tools. His publications emphasize educational technology integration and formal methods in software engineering. He actively participates in tennis and has a passion for music, having played violin and recently resumed piano lessons. Teaching contributions include foundational courses in programming, software design, and mission-critical systems. Students praise his clear explanations and high standards, despite rigorous assessments. He advocates for quality learning environments and has developed innovative teaching materials using drawing tablets and video capture.

Patrick Massotمشاهده پروفایل

استاد

• Symplectic Geometry
• Contact Geometry
• Formalized Mathematics
• +۵ مورد دیگر

Patrick Massot is a Professor in the Department of Mathematics at the Faculty of Sciences of Orsay, University of Paris-Saclay, France. His work bridges pure mathematics and formal verification, with a focus on symplectic and contact geometry, and the formalization of advanced mathematical theories using the Lean proof assistant. His research interests include symplectic geometry , contact geometry , formalized mathematics , and differential topology . He has contributed significantly to the formalization of perfectoid spaces, the h-principle, and sphere eversion. His recent work emphasizes the educational use of proof assistants in teaching undergraduate mathematics. The most recent publications reflect a strong trend toward formal verification in mathematics, combining geometric intuition with rigorous computational proof. These works span topics such as convex integration, holonomic approximation, and the use of Lean for pedagogy. The underlying themes include flexibility in geometry, foundational rigor, and interdisciplinary collaboration between mathematics and computer science. Program Committee Member, CPP 2025 Author, Formalising the h-principle and sphere eversion (CPP 2023) Patrick Massot has advised no publicly listed students, and no specific grants are mentioned. However, his collaborative work with prominent mathematicians (e.g., Buzzard, Commelin, Giroux, Etnyre) suggests active research funding and participation in major projects such as the Liquid Tensor Experiment. He leads a formalized mathematics working group and was involved in a 2015–2016 working group on sheaf theory applied to Lagrangian submanifolds. These groups serve as hubs for collaborative research in formalization and geometric topology.

Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglioمشاهده پروفایل

مدرس

• Formalized Mathematics
• Algebraic Number Theory
• Proof Assistants
• +۶ مورد دیگر

Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio is a Lecturer (Maître de Conférences) in Pure Mathematics at Université Jean Monnet Saint-Étienne, France. He is actively engaged in research at the intersection of formal mathematics and algebraic number theory, particularly through the Lean theorem prover. His research interests include: Formalized Mathematics Algebraic Number Theory Proof Assistants Lean Theorem Prover Number Theory Functional Analysis The recent publication in CPP 2024 on the formalization of complete discrete valuation rings and local fields reflects a strong trend in using interactive theorem proving to rigorously verify foundational results in algebraic number theory. His work contributes to the growing mathlib4 library, emphasizing correctness and formal verification in advanced mathematics. He has no listed scientific awards in the provided sources. Filippo is actively involved in academic service and education, notably organizing and teaching in the Lean Master’s program in Lyon (2024–2025), as shown by his public teaching repository. He contributes regularly to the Lean 4 and mathlib4 projects on GitHub, demonstrating strong engagement with the formal methods community. There is no mention of research grants in the provided texts. He is associated with the formal mathematics community through GitHub and conference participation (CPP, POPL), contributing to open-source developments in theorem proving and formalized algebra.

Delphine Demangeمشاهده پروفایل

دانشیار

• Programming languages implementation
• Compiler verification
• Formal semantics
• +۳ مورد دیگر

Delphine Demange is an Associate Professor in Computer Science at the University of Rennes, affiliated with Inria, CNRS, and IRISA. She works in the Epicure research group (formerly Celtique) and focuses on formal semantics, compiler verification, program transformations, static analysis, computer-aided verification, and language-based security. Her career spans roles at the University of Pennsylvania as a postdoctoral researcher and a PhD at ENS Cachan-Brittany Extension under Thomas Jensen and David Pichardie. Her research interests center on formal methods for programming languages , particularly through compiler verification , static analysis , and language-based security . She has mechanized semantics for dataflow circuits and SSA-based optimizations, bridging theoretical rigor with practical compiler correctness. Her work often leverages interactive theorem provers like Coq to ensure robustness. Delphine’s recent publications (2025–2010) highlight her expertise in formal verification of compilers, dataflow analysis , and concurrent systems . Notable trends include mechanized semantics for gated SSA and dataflow circuits , verified intermittent computing models, and concurrent garbage collectors using rely-guarantee methodologies. Scientific Awards: EAPLS Best PhD Dissertation Award (2012) Gilles Kahn PhD Thesis Award (2013) Teaching: She has taught undergraduate and master’s courses including Java programming, algorithmics, deductive verification with Why3, compilation, and software security. Her pedagogical contributions span functional programming, semantics, and logic. Professional Service: Delphine has served on steering committees for CC (2021–2024), co-chaired JFLA 2024 and 2023, and participated in program committees for conferences like CGO, OOPSLA, and POPL.

• Blockchain
• Cybersecurity
• Distributed Systems
• +۵ مورد دیگر

Roberto Zunino is an Associate Professor in the Department of Mathematics at the University of Trento, specializing in blockchain technologies, formal methods, and distributed systems. His research bridges theoretical computer science with practical cryptographic applications, particularly in Bitcoin and smart contract ecosystems. His research interests focus on blockchain security , smart contract formalization , and probabilistic verification . Key areas include MEV (Maximal Extractable Value) theory, UTXO-based smart contracts, and computationally sound tokenization. His work combines rigorous mathematical modeling with real-world protocol analysis, emphasizing security guarantees through formal methods. Recent publications demonstrate a strong trend toward theoretical foundations of blockchain economics and security. His 15 most recent papers (2020-2025) analyze MEV formalization, Bitcoin contract liquidity, UTXO scalability, and smart contract language design, revealing deep integration of type theory, game theory, and cryptographic primitives. Zunino actively teaches courses including Informatics , Interactive Theorem Proving (using Lean 4), and Computer Tools for Mathematics . His educational focus emphasizes formal verification, imperative programming foundations, and mathematical logic applications in computer science.