Logic Society of Delhi

April 4 2025, Ashoka University:

Seminar: Tractable Representations for Automated Functional Synthesis.
Speaker: S. Akshay, Shridhar Shukla Chair Professor in Digital Trust, IIT Bombay.
(abstract, It is often easy to write down the specification of a system as a relation between inputs and outputs. But implementing the system is a functional problem: to provide functions that produce outputs from inputs. The question we ask is if we can automatically synthesize such a function from the given relation? This question has generated a lot of interest in recent years, especially in the Boolean setting, where despite theoretical hardness results, many techniques and tools have been developed that now scale surprisingly well. In this talk, we shine a light on this problem from a Knowledge Representation perspective. We identify structural properties and develop normal forms for the specification that guarantee provably efficient synthesis. Further, we move towards a characterization of what makes Boolean functional synthesis easy and examine techniques to compile into such forms.

[Based on joint work with Supratik Chakraborty, Sahil Jain and Shetal Shah at CAV'23 and AMAI'23] about the speaker S. Akshay is a Professor in the Department of Computer Science and Engineering at IIT Bombay, where he holds the Shridhar Shukla Chair for Digital Trust and is affiliated with the IITB Trust Lab and the Ashank Desai Centre for Policy Studies. His research interests span formal methods and AI with a focus on quantitative (timed/probabilistic) verification, automata theory and automated synthesis. He has given multiple invited talks and tutorials on functional synthesis in venues including Highlights 2022, AAAI 2022 and IJCAI 2022 as well as organized workshops on various topics ranging from Trustworthy AI to Functional Synthesis and Automata, Concurrency and Timed systems in India and outside. )

March 4 2025, IIT Delhi:

Seminar: Distribution Testing: The New Frontier for Formal Methods.
Speaker: Kuldeep Meel, Stephen Fleming Early Career Associate Professor, Georgia Institute of Technology.
(abstract, The dominant guiding philosophy in the first sixty years of Computer Science was for designers to design systems that were always correct, and to accept nothing less as users. But times have changed: Users and designers are accustomed to systems with statistical components and behaviors. What does it mean for the formal methods community? In this talk, we argue that such a dramatic change in the acceptance and design of systems presents exciting opportunities to make fundamental contributions: we need to rethink the notions and techniques for the design of specifications and verification methodologies. In particular, we will focus on the systems whose behaviors are not naturally captured by symbolic relations but rather require reliance on probability distributions. We will discuss our recent efforts in designing formal methodologies for testing whether a sampling subroutine generates a desired distribution. We will showcase the challenges, opportunities, and rewards in our journey. about the speaker Kuldeep Meel holds Stephen Fleming Early-Career Associate Professorship in the School of Computer Science, and an Associate Professor at the University of Toronto (on leave). His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2022 ACP Early Career Researcher Award, the 2019 NRF Fellowship for AI, and was named AI's 10 to Watch by IEEE Intelligent Systems in 2020. His research program's recent recognitions include the Distinguished Paper Award at CAV-23 and CAV-24, ICLP-24 Best Paper Award,2023 CACM Research Highlight Award, 2022 ACM SIGMOD Research Highlight, IJCAI-22 Early Career Spotlight, Best Paper Award nominations at ICCAD-21 and DATE-23, 1st Place in Model Counting Competition (2020 and 2022). He is passionate about teaching, and most proud of being recipient of university-level Annual Teaching Excellence Awards in 2022 and 2023. )

February 14 2025, IIIT Delhi:

Seminar: The Art of Writing Righting Code.
Speaker: Aalok Thakkar, Assistant Professor, Ashoka University.
(abstract, In this talk, we will explore the quest for program correctness, a cornerstone of computer science since its inception. We will begin with the historical developments that laid the groundwork for program correctness and the work of some key historical figures who laid the groundwork in this area. Then we look at automated reasoning, in particular Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT). These advances have enabled scalable and efficient analysis of complex systems.

Finally, I will talk about program synthesis, a paradigm that shifts the focus from verifying existing code to automatically generating correct-by-construction programs. We will explore the theoretical underpinnings of synthesis, and then I will give an overview of some of my work on example-guided synthesis of relational queries. By examining these three phases—verification, automated reasoning, and program synthesis—we gain a comprehensive understanding of the area of formal methods. Time permitting, we will discuss how these paradigms interact with advances in neural and large foundational models. about the speaker Aalok Thakkar is an assistant professor in the department of Computer Science at Ashoka University and specializes in the areas of programming languages, formal logic, and artificial intelligence. In 2023, he obtained my Ph.D. advised by Rajeev Alur and Mayur Naik. During this time, he developed the example-guided framework for synthesis of relational queries. In the past, he has worked with Adobe Systems, Aptos Labs, AWS Automated Reasoning Group, Laboratoire Specification et Verification, Nokia Bell Labs, and Movement Labs. )

January 29 2025, Ashoka University:

Seminar: Testing correctness of samplers using property testing: from theory to practice and back again.
Speaker: Sourav Chakraborty, Professor, Indian Statistical Institute, Kolkata.
(abstract, How can one test the correctness of a program that is supposed to output an element from a large universe according to a certain distribution? These kinds of programs are heavily used in real life but are rarely tested for correctness. This problem can be framed as a problem in property testing. Property testing is a subject that deals with these challenges. It tries to design sub-linear algorithms for testing various properties of inputs. The key lies in the way the data is accessed by the algorithm.

One of the central problems in property testing and many other related subjects is testing if a distribution has a certain property - say whether a distribution on a finite set is uniform. The conventional way of accessing the distributions is by drawing samples according to the distributions. Unfortunately, in this setting the number of samples that are necessary for testing properties of distribution (for most natural properties) is polynomial in the size of support of the distribution. Thus when the support is relatively big the algorithms become impractical in real life applications.

We introduced a new way of accessing the distribution using ``conditional-sampling oracle". This oracle can be used to design much faster algorithms for testing properties of distribution and thus makes the algorithm useful in practical scenarios. We show that the conditional oracle can be implemented in many real life problems and we have been able to show the usefulness of this model and our algorithms in practical purposes and in other areas of research - like testing of probabilistic verification. This model also throws a number of interesting theoretical questions. about the speaker Sourav Chakraborty is a Professor in the Advanced Computing and Microelectronics Unit (ACMU) of the Computer and Communication Sciences Division (CCSD) at the Indian Statistical Institute (ISI) , Kolkata, India. Before joining ISI on July 2018 he was a faculty member at Chennai Mathematical Institute , India, from September 2010. Before that he was a postdoc at the Algorithms and Complexity department of Centrum Wiskunde & Informatica (CWI), Amsterdam, Netherlands from September 2009 to August 2010. From October 2008 to August 2009 he was a postdoc at the Computer Science Department of Technion, Israel. In June 2008 he finished his PhD in Computer Science from University of Chicago under the supervision of Prof. László Babai.

His field of research is Theoretical Computer Science. His focus has been in the classical and quantum complexity of Boolean functions (including property testing, sensitivity and block sensitivity of Boolean functions and quantum database search), in electronic commerce, in graph algorithms and in coding theory. )

January 27 2025, IIT Delhi:

Seminar: Distinct Elements in Streams and the Klee's Measure Problem.
Speaker: Sourav Chakraborty, Professor, Indian Statistical Institute, Kolkata.
(abstract, We will present a very simple streaming algorithm on F0 estimation that also caught the eye of Donald E. Knuth. In a recent article, Donald E. Knuth started with the following two paragraphs:

"Sourav Chakraborty, N. V. Vinodchandran, and Kuldeep S. Meel have recently proposed an interesting algorithm for the following problem: A stream of elements (a1, a2,...,am) is input, one at a time, and we want to know how many of them are distinct. In other words, if A = {a1, a2,...,am} is the set of elements in the stream, with multiplicities ignored, we want to know |A|, the size of that set. But we don't have much memory; in fact, |A| is probably a lot larger than the number of elements that we can hold in memory at any one time. What is a good strategy for computing an unbiased estimate of |A|?

Their algorithm is not only interesting, it is extremely simple. Furthermore, it's wonderfully suited to teaching students who are learning the basics of computer science. (Indeed, ever since I saw it, a few days ago, I've been unable to resist trying to explain the ideas to just about everybody I meet.) Therefore I'm pretty sure that something like this will eventually become a standard textbook topic. This note is an initial approximation to what I might write about it, if I were preparing a textbook about data streams."

This simple algorithm comes out of the first ever "efficient" streaming algorithm (from PODS 21) for the Klee's Measure problem, which was a big open problem in the world of streaming for many years. about the speaker Sourav Chakraborty is a Professor in the Advanced Computing and Microelectronics Unit (ACMU) of the Computer and Communication Sciences Division (CCSD) at the Indian Statistical Institute (ISI) , Kolkata, India. Before joining ISI on July 2018 he was a faculty member at Chennai Mathematical Institute , India, from September 2010. Before that he was a postdoc at the Algorithms and Complexity department of Centrum Wiskunde & Informatica (CWI), Amsterdam, Netherlands from September 2009 to August 2010. From October 2008 to August 2009 he was a postdoc at the Computer Science Department of Technion, Israel. In June 2008 he finished his PhD in Computer Science from University of Chicago under the supervision of Prof. László Babai.

His field of research is Theoretical Computer Science. His focus has been in the classical and quantum complexity of Boolean functions (including property testing, sensitivity and block sensitivity of Boolean functions and quantum database search), in electronic commerce, in graph algorithms and in coding theory. )

January 15-22 2025, Virtual and in New Delhi:

World Logic Day Celebrations.
Join us for a series of virtual talks, followed by an in-person reception. More details, abstracts, conferencing links, and reception details are here.

November 27 2024, Ashoka University:

Seminar: Proving Security Protocols Correct.
Speaker: Vaishnavi Sundararajan, Chandruka New Faculty Fellow and Assistant Professor at IIT Delhi.
(abstract, Security protocols underpin most aspects of our digital lives nowadays, with finance, health, and even citizenship requiring some online interaction. Mere testing does not suffice for such critical systems, since even one missed test-case could prove to be incredibly costly. So we turn to formal verification, which converts the system into some “abstract” model, casts properties as statements over this model, and then checks if the model satisfies those statements. Formal verification has been done for many security protocols (including TLS, and the Signal messaging protocol) and even found many bugs. The standard verification framework was proposed by Danny Dolev and Andy Yao in a 1983 paper, where the network is assumed to be adversarial, and all communicated messages are modelled as terms in an algebra. We will see a few examples of how this model can be used to find logical flaws in protocols. We recently extended this model to deal with protocols for the internet age which involve certification, by distinguishing between “normal” messages (like encrypted or hashed terms) and “assertions” (statements of the form “this message is an encryption of a 0 or a 1”) using two different algebras. This allows us to better represent such security protocols and avoid human errors in the modelling phase, as well as make the resultant protocol description more readable. We will see some examples of protocols modelled using assertions, and if time permits, briefly discuss that this expressivity comes at no extra cost, i.e. protocol verification is no harder in the presence of an actively malicious adversary in this new model than it was in the original Dolev-Yao model. about the speaker Vaishnavi Sundararajan is a Chandruka New Faculty Fellow and Assistant Professor in the Department of Computer Science and Engineering at the Indian Institute of Technology Delhi. She is also associated with the Center of Excellence in Cyber Systems and Information Assurance (CSIA). She is interested in applying formal methods and logic to various fields, primarily security. Vaishnavi completed her PhD at the Chennai Mathematical Institute, where she was advised by R Ramanujam and S P Suresh. She has also done postdoctoral stints at CNRS (IRISA), Ericsson Research, and UC Santa Cruz. )