FSTTCS 2026
46th IARCS Annual Conference on
Foundations of Software Technology and Theoretical Computer Science
- Main Conference: December 16–18, 2026
- Venue: IIT Delhi
46th IARCS Annual Conference on
Foundations of Software Technology and Theoretical Computer Science
FSTTCS 2026 is the 46th conference on Foundations of Software Technology and Theoretical Computer Science. It is organised by IARCS, the Indian Association for Research in Computing Science, in association with ACM India. It is a forum for presenting original results in foundational aspects of Computer Science and Software Technology. Within Track B, there is a focus on soliciting submissions in the areas of Programming Languages and Practical Verification, in addition to theoretical results.
FSTTCS 2026 will be held in IIT Delhi during December 16–18, 2026. The conference is being organized as an in-person event.
Submissions must be in electronic form via EasyChair using the LIPIcs LaTeX style file available here. Submissions must not exceed 15 pages (excluding bibliography), but may include a clearly marked appendix containing technical details. The appendix will be read only at the discretion of the program committee. Simultaneous submissions to journals or other conferences with published proceedings are disallowed.
Reviewing for FSTTCS 2026 is double-blind. Hence, authors must make a reasonable effort to ensure that their identity is not easily revealed from the submission itself. Specifically, kindly replace your name and affiliation on the first page with the submission number and do not include any acknowledgements in your submission. Also, authors should cite their prior work in a neutral manner (i.e., instead of saying “We showed”, please write “XYZ et al. showed”). Submitting a paper that is available at a public preprint server (such as, arXiv) is admissible. In that case, please do not cite that version of your work in the submission itself. Submissions violating the page limit or the double-blind policy may face desk rejection.
Accepted papers will be published as proceedings of the conference in the Leibniz International Proceedings in Informatics (LIPIcs) as a free, open, electronic archive with access to all. Authors will retain full rights over their work. The accepted papers will be published under a CC-BY license. For an accepted paper to be included in the proceedings, one of the authors must commit to presenting the paper in person at the conference.
Submission link: https://easychair.org/my/conference?conf=fsttcs2026
Alastair Donaldson, Imperial College London
From Formal Methods to Fuzzing and Back
For the first twelve years of my career in computer science I mainly worked on formal methods. I had been drawn to the field as an undergraduate by its promise of a way to build software with strong, mathematically based correctness guarantees. But after many years of struggling to make formal methods scale, I was seduced by randomised testing, also known as fuzzing. Fuzzing is much less principled than formal methods, but it just works: it can be readily applied to very large systems, and it is extremely effective at finding real bugs that developers care about and fix. In this talk I will trace my path from formal methods to fuzzing, by way of the GPUVerify project on verifying GPU kernels and the GraphicsFuzz project on randomised testing of GPU compilers. I will argue that the oracle problem provides an intellectual link between fuzzing and formal methods, describe my continuing, targeted uses of formal methods in the domain of GPU programming language design, and discuss work at the boundary between formal methods and fuzzing. Finally, I will reflect on whether generative AI might be the missing ingredient that allows formal methods to scale, and set out my plans for large-scale formal methods via the Keystone project, through which my collaborators and I aim to find out how much of that promise can be realised in practice.
Alastair Donaldson is a Professor in the Department of Computing at Imperial College London where he leads the FastPL Group, investigating novel techniques and tool support for programming, testing and reasoning about high performance systems and their programming languages. He was Founder and Director of GraphicsFuzz Ltd., a start-up company specialising in metamorphic testing of graphics drivers, which was acquired by Google in 2018, after which he spent time working with Google as a software engineer and then as a Visiting Researcher. He was the recipient of the 2017 BCS Roger Needham Award and an EPSRC Early Career Fellowship, and has published more than 100 articles in the fields of programming languages, formal verification, software testing and parallel programming. Alastair was previously a Visiting Researcher at Microsoft Research Redmond, an EPSRC Postdoctoral Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow, and is a Fellow of the Royal Academy of Engineering and a Fellow of the British Computer Society.
Jean-François Raskin, Université libre de Bruxelles
Hybrid Approaches to Reactive Synthesis: Integrating Learning and Formal Verification
Reactive synthesis produces controllers that are correct by construction.However, formal methods for synthesis face high complexity, undecidability, and sometimes the difficulty of writing complete specifications. Machine learning scales better and generalises well in practice, but it offers weaker guarantees. In this paper, we review three ways of combining the two, based on joint work with several colleagues. First, in "LTL synthesis with hints", the user gives a few examples and a passive automata learning algorithm generalises them. The synthesis algorithm ensures that this generalisation preserves the realisability of the specification. Second, for POMDPs, we cast policy synthesis as active automata learning. An online sampling-based planner answers membership queries, and a probabilistic model checker answers equivalence queries. As a result, every finite-state controller we return is verified. Third, we use formal methods to guide Monte Carlo tree search with symbolic advice, and we show that this preserves its convergence guarantees. We then train a neural network to imitate the advice, which removes the latency of computing it. In each case, we identify which component proposes a solution and which one provides the guarantee.
Jean-François Raskin is a professor of computer science at the Université libre de Bruxelles (ULB) working on formal methods for the verification and synthesis of reactive systems. His research focuses on graph games—including quantitative and imperfect-information models—and their applications to controller synthesis. More recently, he has studied multi-player games and their applications to rational synthesis and verification. He has also contributed to approaches that combine reactive synthesis with learning techniques.
Ranjit Jhala, University of California, San Diego
Foundational Constraints for Expressive Refinements
SMT-based program verifiers are hamstrung by two problems: expressiveness, because predictable verification restricts specifications to the boundaries of SMT decidability, and trust, because the solver is a large, unverified artifact whose soundness bugs may quietly compromise every tool built on it. In this talk, we describe Flex, a foundational Constrained Horn Clause (CHC) solver implemented in Lean, that reduces the constraint solver's trusted base to the kernel alone, and allows using Lean's entire proof ecosystem to verify low-level systems code, via two contributions. First, we show how Flex encodes CHCs as plain Lean propositions where the Horn variables are existentially bound predicates, and how to implement CHC solvers as tactics (meta-programs) that compute kernel-checkable proofs of the CHC propositions. Then, we show how Flex allows us to leapfrog the expressiveness limitations of SMT by unleashing Lean's entire ecosystem of proof machinery to prove arbitrary functional correctness properties of various low-level Rust libraries using the Flux refinement type checker.
Ranjit Jhala is a Professor of Computer Science at University of California, San Diego, USA.
Rohit Gurjar, IIT Bombay
A deterministic parallel algorithm for bipartite matching
The bipartite matching problem is one of the most extensively studied problems in algorithms and complexity theory. Beyond numerous practical applications such as assigning suitable tasks to machines, its study has led to several influential ideas in the field. In this talk, we will review the history of the problem from the perspective of parallel algorithms and present a result that gives the first deterministic parallel (NC) algorithm for it, settling a question that had remained open for more than four decades. Based on joint work with Abhranil Chatterjee, Sumanta Ghosh, Roshan Raj, and Thomas Thierauf
Rohit Gurjar is a faculty member at the Department of Computer Science and Engineering at the Indian Institute of Technology Bombay. His research spans algebraic complexity theory, pseudorandomness, parallel complexity and polyhedral combinatorics.
Gautam Kamath, Courant Institute of Mathematical Sciences at New York University.
The Broader Landscape of Robustness in Algorithmic Statistics
Mean estimation is a simple statistical task, solved optimally by a simple algorithm: the empirical mean. The story changes dramatically when the estimator is required to be robust. What exactly it means for an estimator to be robust can depend on the situation. It can be robust to model misspecification or adversarial contamination. It can be robust to outliers caused by heavy-tailed data. Or it can be robust in the sense of differential privacy. We will discuss how, surprisingly, we can design computationally efficient algorithms subject to all these types of robustness using the same underlying technical ideas, resulting in powerful estimators that are qualitatively quite different from the empirical mean. These connections offer glimpses of a broader landscape of robustness in statistical estimation.
A survey article accompanying this talk is published in IEEE BITS Magazine (https://arxiv.org/abs/2412.02670).
Gautam Kamath is an assistant professor of computer science at the Courant Institute of Mathematical Sciences at NYU, affiliated with the Theoretical Computer Science and the Computational Intelligence, Vision, and Robotics Lab (CILVR). Gautam has been recognized with numerous awards for his work, including the 2026 Gödel Prize, the 2026 Presburger Award, the Ontario Early Researcher Award in 2025, the 2024 Caspar Bowden Award for Outstanding Research in Privacy Enhancing Technologies (and the 2026 runner up).
SAT+SMT School
Dates: 14th, 15th December 2026
Strategic behaviour in matching markets
Dates: 14th December 2026
Quantum lower bounds through query complexity
Dates: 15th December 2026
Recent advances in algorithms
Dates: 14th, 15th December 2026
Recent Highlights in Programming Languages
Dates: 16th -- 18th December 2026
Workshop on Games and Automata for Synthesis
Dates: 19th December 2026
Workshop on exposition, explanation and depth
Dates: 19th, 20th December 2026
Recent trends in crypto
Dates: 19th, 20th December 2026