Pinaki Chakraborty.

Computer scientist · Formal methods · Logic · Verification

Pinaki Chakraborty

PhD candidate at UCL · PPLVLondon, United Kingdom

I am a PhD candidate in the Programming Principles, Logic and Verification (PPLV) group at University College London, supervised by Professor David Pym. My thesis submission is expected in January 2027.

My research concerns formal semantics, causal and counterfactual reasoning, model checking, and resource-constrained multi-agent systems. I develop modal, substructural, and separation-style logical frameworks for compositional reasoning, with applications to verification and security-oriented systems modelling.

I hold a Master of Technology in Computer Science from the Indian Statistical Institute, awarded with First Division with Distinction. My programming background includes C, C++, Haskell, and Python, with implementation experience in model checking and automated reasoning.

Email ↗ ORCID: 0009-0004-3667-1700 ↗ UCL profile ↗PPLV ↗

Research

My research currently focuses on:

  • Computational logic and verification. Proof theory, model checking, and logical methods for reasoning about systems and security properties.
  • Causality and multi-agent systems. Structural causal models, counterfactual reasoning, and local reasoning about interacting agents.
  • Resource-sensitive reasoning. Separation-style logics, coalition games, and constraints on the feasibility of actions and interventions.

Research experience

PhD Researcher

Jan 2023–Present

University College London · London, United Kingdom

Supervisor: David Pym

  • Developed formal semantics for causal and counterfactual reasoning in multi-agent systems with resource constraints.
  • Designed modal, substructural, and separation-style logical frameworks for compositional reasoning.
  • Studied formal decision problems, including semantic properties, expressiveness, and computational complexity.
  • Applied structural causal models, transition systems, proof-theoretic techniques, model checking, and automated reasoning to verification and security-oriented systems modelling.

Doctoral Researcher

Jan 2021–Jun 2022

Indian Institute of Technology Kanpur · Kanpur, India

Supervisor: Dr Indranil Saha

  • Studied reactive synthesis of controllers for cyber-physical systems.
  • Worked with formal models of reactive systems and controller correctness.

Selected publications

  1. A Resource-Aware Structural Causal Semantics for Feasibility Analysis of Counterfactuals

    Pinaki Chakraborty, David Pym, and Tristan Caulfield · NMR · 2026

  2. Local Causal Reasoning in Multiagent Systems (Extended Abstract)

    Pinaki Chakraborty, Tristan Caulfield, and David Pym · CALM 2025 / Springer · 2026

  3. A Logic for Resource-Sensitive Coalition Games

    Pinaki Chakraborty, Tristan Caulfield, and David Pym · GameSec 2025 / Springer · 2026

Education

University College London

2023–Present

PhD in Computer Science

London, United Kingdom

Supervisor: Prof. David Pym

Expected thesis submission: January 2027.

Indian Institute of Technology Kanpur

2021–2022

Doctoral Study in Computer Science and Engineering

Kanpur, India

Supervisor: Prof. Indranil Saha

Indian Statistical Institute

2020

Master of Technology in Computer Science

Kolkata, India

First Division with Distinction.

Relevant coursework: Automata, Languages and Computation; Logic for Computer Science; Logic and Artificial Intelligence; Distributed Computing; Information Retrieval; Natural Language Processing.

Indian Institute of Engineering Science and Technology, Shibpur

2017

Undergraduate Degree in Information Technology

Howrah, India

Selected projects

Teaching

University College London

Teaching Assistant

  • Software Verification and Validation — Tutorials and student support in software testing, program analysis, and verification. Module lead: Prof. Earl Barr.
  • Machine Vision
  • Algorithms
  • Discrete Mathematics — Conducted tutorials in Lean 4.

Indian Institute of Technology Kanpur

Teaching Assistant

  • Embedded and Cyber-Physical Systems

Technical skills

Programming
C; C++; Haskell; Python.
Formal methods and automated reasoning
Model checking; SAT/SMT solving; theorem proving; formal verification.
Tools
Z3; NuSMV; working knowledge of TLA+ and Infer.
Logic and semantics
Temporal logic; separation logic; transition systems; structural causal models.

Contact

The best way to reach me is pinaki.chakraborty.22@ucl.ac.uk.