I work in the area of formal methods, developing theory, algorithms
and computational tools that help in building verifiably correct
hardware, software and intelligent systems. Such systems increasingly
pervade our lives, yet their growing complexity makes it humanly
impossible to reason about all corner case behaviours. Mathematically
provable guarantees are therefore crucial to ensure that the systems
we increasingly trust our lives on are indeed trustworthy.
My research focuses on (i)
formal verification, wherein we provide a formal proof that
a system satisfies a property or demonstrate its violation,
(ii) rigorous analysis of system models to extract meaningful
information, and (iii) automated synthesis of systems from
specifications, with the guarantee that the synthesized system satisfies
I have applied formal methods to reason about software, hardware,
machine learning and biological systems. The gap between theory and
practice of formal methods concerns me deeply and I have consciously
tried to bridge this gap in my work.
"Algorithms for Boolean Functional Synthesis"
"Knowledge Compilation for Boolean Functional Synthesis"
"Counterexample Guided Repair in Boolean Functional Synthesis"
"Scaling Discrete Integration and Sampling: Foundations and
Challenges", tutorial co-presented with Kuldeep S. Meel
"Discrete Sampling and Counting for the AI Practitioner",
tutorial co-presented with Kuldeep S. Meel and Moshe Y. Vardi
"Discrete Sampling and Integration in High Dimensional
Spaces", tutorial co-presented with Kuldeep S. Meel and Moshe
Y. Vardi at
Selected recent publications
[For a complete listing of publications, see here ]
S. Akshay, S. Chakraborty and S. Jain, "Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis", in Proc. of International Conference on Computer-Aided Verification (CAV), pg 367--389, Jul 2023 [PDF]
S. Chakraborty, A. Gupta and D. Uadkat, "Full Program Induction: Verifying Array Programs sans Loop Invariants", in International Journal on Software Tools for Technology Transfer, Vol 24(5), pages 843--888, 2022 (published online Sep 2022 at Springer SharedIt) [PDF of pre-print]
S. Akshay and S. Chakraborty, "Synthesizing Skolem functions: A
view from theory and practice", in Handbook of
Logical Thought in India, eds. Sundar Sarukkai and Mihir
K. Chakraborty, Springer, Jule 2022 [PDF of chapter preprint](The published chapter can be found on Springer Link).
S. Chakraborty and S. Akshay, "On Synthesizing Computable Skolem Functions for First
Order Logic", in Proc. of International Conference on Mathematical Foundations of
Computer Science, pages 30:1-30:15, Aug 2022 [PDF]
H. Torfah, S. Shah, S. Chakraborty, S. Akshay and S. Seshia,
"Synthesizing Pareto-optimal Interpretations for Black-Box Models",
in Proc. of International Conference on Formal Methods
in Computer-Aided Design (FMCAD), pages 153-162, Oct 2021[PDF of extended version
S. Akshay, S. Chakraborty, S. Goel, S. Kulal and S. Shah, "Boolean Functional Synthesis: Hardness and Practical Algorithms", in
Formal Methods in System Design, Vol 57(1), pages 53--86, 2021 (published online Oct 2020 at Springer SharedIt) [PDF of pre-print]