Sumanth Prabhu, TCS Research and IISc Bangalore, Specification Synthesis with Constrained Horn Clauses

Slides     Video

Abstract

The problem of synthesizing specifications of undefined procedures has a broad range of application, but the usefulness of the generated specifications depends on its quality. In this talk, I present our recent paper that synthesizes maximal and meaningful specifications. We look at how the technique in the paper can be used in open program verification to not only discover specifications of missing functions, but also invariants for complex control flow.
This talk is based on following paper: Specification Synthesis with Constrained Horn Clauses. PLDI 2021 Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar and Deepak D'Souza

Soumyadip Bandyopadhyay and Rakshit Mittal, BITS Pilani, Goa Campus, Translation Validation of Loop involving Code Optimizing Transformations using Petri Net based Models of Programs

Slides     Video

Abstract

Translation validation is the process of proving semantic equivalence between source and source-translation, i.e., checking the semantic equivalence between the target code (which is a translation of the source program being compiled) and the source code. In this talk, we propose a translation validation technique for Petri net based models of programs which verify several code optimizing transformations involving loop. These types of transformation have been used in several application domains such as scheduling phase of High level synthesis, high performance computations etc. Our Petri net based equivalence checker checks the computational equivalence between two one-safe colour Petri nets. In this work, we have taken two versions of CPNs one corresponds to the source program and the other, the target programs. Using path based analysis technique, we have developed a sound method for proving several code optimizing transformations involving loop. We have also compared our results with other Petri net based equivalence checkers.

Akshatha Shenoy, TCS Research, Property Directed Self Composition

Slides     Video

Abstract

In this talk, I will be presenting a paper from CAV 2019 with the same title. The paper addresses the problem of verifying k-safety properties: properties that refer to k interacting executions of a program. A prominent way to verify k-safety properties is by self composition, reducing the problem to checking an ordinary safety property over a program that executes k copies of the original program in some order. The way in which the copies are composed determines how complicated it is to verify the composed program. The paper formulates the problem of inferring a self composition function together with the inductive invariant needed to verify safety of the composed program, and develops a property-directed inference algorithm to infer composition-invariant pairs, if one exists, in a restricted language.

Divyesh Unadkat, TCS Research and IIT Bombay, Exploiting Induction and Difference Computation to Verify Array Programs

Slides     Video

Abstract

In this talk, we present a novel verification technique to prove properties of a class of array programs with a symbolic parameter N. The technique constructs two slightly different versions of the given program and infers difference invariants between the corresponding variables of the two versions at key control points. The difference invariants are crucially used during the inductive step of the analysis, allowing us to exploit the synergy between the two techniques. We have implemented an instance of this technique in a prototype tool called diffy. It outperforms state-of-the-art tools for verifying array programs on a large set of benchmarks.

Rahul Sharma, Microsoft Research, Machine Learning with 2KB RAM

Slides     Video

Abstract

For an intelligent edge, it is imperative to deploy ML models directly on tiny IoT devices. However, IoT devices are resource constrained which makes such deployments hard. In particular, ML models are written at a high level with no regard to the memory constraints of the underlying hardware and typically use floating-point arithmetic. IoT devices typically have no floating-point units and a model that exceeds memory limits by even a single byte would fail to run on the device. SeeDot is a compiler that translates floating-point machine learning inference algorithms to fixed-point code that use 8-bit or 16-bit integers, with minimal loss in classification accuracy. SeeDot takes memory constraints as inputs and uses clever memory management to generate code that fits within the memory limits of the device. We show how SeeDot enables deploying recurrent neural networks (RNNs) on an Arduino Uno, a device with only 2KBs of RAM. We show the first demonstration of face detection running on an ARM Cortex M4 microcontroller with only hundreds of KBs of memory. Finally, SeeDot’s FPGA backend allows developers to run ML on embedded FPGAs with no additional developer overhead and reducing power consumption by 300x.

Subodh Sharma, IIT Delhi, Analysis of Release-Acquire Concurrency with Partial Order Domain

Slides     Video

Abstract

In this talk, I will present our ongoing work on verifying concurrent programs running under the release-acquire (RA) fragment of the C11 memory model using thread-modular reasoning. The RA model provides weaker guarantees than sequential consistency, and allows for the construction of high performance implementations (e.g., read-copy-update synchronisation) without making programmability overly complex. Under the RA model a total order on the stores of each global memory location is enforced, which restricts loads reading from overwritten stores. In addition, the updates in an RA program lack immediate global visibility, which makes programs under RA semantics naturally amenable to thread-modular reasoning. I will discuss our specific contributions (partial order domains) with regard to thread-modular reasoning and argue that our technique is effective in refutation as well as verification of RA programs.

Akash Lal, Microsoft Research, Learning-based Controlled Concurrency Testing

Slides     Video

Abstract

This talk will be based on an OOPSLA 2020 paper with the same title. Here's the abstract from the paper.

Concurrency bugs are notoriously hard to detect and reproduce. Controlled concurrency testing (CCT) techniques aim to offer a solution, where a scheduler explores the space of possible interleavings of a concurrent program looking for bugs. Since the set of possible interleavings is typically very large, these schedulers employ heuristics that prioritize the search to "interesting" subspaces. However, current heuristics are typically tuned to specific bug patterns, which limits their effectiveness in practice. In this paper, we present QL, a learning-based CCT framework where the likelihood of an action being selected by the scheduler is influenced by earlier explorations. We leverage the classical Q-learning algorithm to explore the space of possible interleavings, allowing the exploration to adapt to the program under test, unlike previous techniques. We have implemented and evaluated QL on a set of microbenchmarks, complex protocols, as well as production cloud services. In our experiments, we found QL to consistently outperform the state-of-the-art in CCT.

Sreejith A V, IIT Goa, Regular languages over countable words

Slides     Video

Abstract

In this talk, we are interested in languages over countable words. Finite and omega words are proper subsets of countable words. Languages that are definable in the monadic second-order logic form a natural class of languages called regular languages. There are also important fragments of interest like first-order logic, weak monadic second-order logic, linear temporal logic. Some natural algorithmic problems arise - satisfiability, expressive equivalence, etc. These are answered in the finite and omega words case through an equivalent machine model called finite automata. We present a similar notion for countable words called "o-monoids". We answer the algorithmic problems in the case of countable words through a study of o-monoids. Finally, we conclude the talk with a principle to decompose "o-monoids" and a few applications of this principle.

The talk contains the following work:
"Limited set quantifiers over countable linear orderings," Colcombet and Sreejith, ICALP 15
"Two-Variable Logic over Countable Linear Orderings," Amaldev and Sreejith, MFCS 16
"Block products for algebras over countable words and applications to logic," Bharat Adsul, Saptarshi Sarkar, Sreejith, LICS 19

Supratik Chakraborty, IIT Bombay, Counter-example guided repair in Boolean functional synthesis

Slides     Video

Abstract

Boolean functional synthesis concerns synthesizing Skolem functions for existentially quantified variables in a 2QBF specification. The problem has interesting applications even when the 2QBF specification is "unrealizable" in the classical sense. Over the last decade, significant progress has been made in solving this problem for large and difficult benchmarks. A useful paradigm that has emerged from this work is one of guess-check-repair of Skolem functions. In this talk, we look deeper into some effective techniques for "guessing" candidate Skolem functions, and for counterexample-guided repair of such functions, as implemented in state-of-the-art tools.

K V Raghavan, IISc Bangalore, Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains

Slides     Video

Abstract

Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This paper addresses the problem of precise data flow analysis for such systems. To obtain good precision, data flow analysis needs to somehow skip execution paths that read more messages than the number of messages sent so far in the path, as such paths are infeasible at run time. Existing data flow analysis techniques do elide a subset of such infeasible paths, but have the restriction that they admit only finite abstract analysis domains. In this paper we propose a generalization of these approaches to admit infinite abstract analysis domains, as such domains are commonly used in practice to obtain high precision. We have implemented our approach, and have analyzed its performance on a set of 14 benchmarks. On these benchmarks our tool obtains significantly higher precision compared to a baseline approach that does not elide any infeasible paths and to another baseline that elides infeasible paths but admits only finite abstract domains.

Priyanka Golia, IIT Kanpur and NUS, Program Synthesis as Dependency Quantified Modulo Theory

Slides     Video

Abstract

Given a specification over inputs X and output Y , defined over a background theory T, the problem of program synthesis is to design a program f such that Y = f(X) satisfies the specification. Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant approach for program synthesis where in addition to the specification, the end-user also specifies a grammar L to aid the underlying synthesis engine. In this talk, we are going to focus on the feasibility of synthesis techniques without grammar, a sub-class defined as T-constrained synthesis.

We will discuss, how fundamental problem of program synthesis can be reduced to another fundamental problem of finding a witness of a Dependency Quantified Formula Modulo Theory (DQF(T)). When the underlying theory is the theory of bitvectors, the corresponding DQF(BV) problem can be further reduced to Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF solving to design DQBF-based synthesizers that outperform the domain-specific synthesis techniques, thereby positioning DQBF as a core representation language for program synthesis.

This is a joint work with Subhajit Roy (IITK) and Kuldeep S. Meel (NUS). The full version of the paper is available at https://arxiv.org/abs/2105.09221. To appear in IJCAI 2021.

Govind R, Universite de Bordeaux and CMI, Partial order reduction for timed systems

Slides     Video

Abstract

In our work, we study the reachability problem for networks of timed automata. We focus on the issue of state-space explosion due to interleavings in these networks and propose solutions for alleviating the effects of this explosion. In the talk, we will present two algorithms for reachability in networks of timed automata based on the ideas of local time semantics and partial order reduction.

Joint work with Frédéric Herbreteau, B Srivathsan and Igor Walukiewicz.

Missula Meghana, IIT Bombay, Automated inference of production rules for glycans

Slides     Video

Abstract

Glycans are tree-like polymers made up of sugar monomer building blocks. They are found on the surface of all living cells, and distinct glycan trees act as identity markers for distinct cell types. Proteins called GTase enzymes assemble glycans via the successive addition of monomer building blocks. The rules by which the enzymes operate are not fully understood. In this talk, we present the first SMT-solver-based iterative method that infers the assembly process of the glycans by analyzing the set of glycans from a cell. We have built a tool based on the method and applied it to infer rules based on published glycan data.

Krishna S, IIT Bombay, Verification of Concurrent Programs under Release Acquire

Slides     Video

Abstract

This is an overview on the verification of concurrent programs under the release acquire (RA) semantics. In the non parameterized setting, the reachability problem is undecidable even in the case where the input program is finite-state. What works well for this class is under approximate reachability, in the form of bounded view switching, an analogue of bounded context switching, relevant to RA. Moving on to the parameterized setting, the semantics of RA can be simplified, lending a better complexity for verification. We characterize the landscape here by showing that the safety verification is pspace-complete for the case where the distinguished threads are loop-free, and jumps to nexp-complete for the setting where an unrestricted distinguished ego thread interacts with the environment threads.

Akshay S, IIT Bombay, Can Zones be used to analyze pushdown timed automata? — a simulations-vs-equivalence story!

Slides     Video

Abstract

Timed automata and pushdown automata are classical models: the former capture time and the latter recursion. When we mix the two, we get a powerful model of pushdown timed automata (PDTA) that extend classical timed automata with a pushdown LIFO-stack. With just timed automata (i.e., without the stack), reachability analysis depends on finite-state abstractions. Using the so-called "zone-abstraction" instead of the "region-abstraction" leads to faster performance and as a result most tools that implement timed automata use the Zone abstraction.

Surprisingly, for PDTA, despite many theoretical results over the last 25+ years, there are no known Zone approaches. In this work, we ask why. Are zones inherently incompatible with an unbounded stack? What do we need to change in the Zone reachability algorithm so that it works for PDTA? The answer leads us into a rabbit-hole of simulations and equivalences used to prune the zone exploration and we emerge with an efficient zone-based implementation at the end.

Based on joint work with Karthik R. Prakash from IITB and Paul Gastin from U. Paris Saclay, to be presented at CAV'21.

Nishant Sinha, OffNote Labs, The Shape of U — Befriending Tensors

Video

Abstract

The Tensor (n-dimensional array) is the principal software abstraction for designing and coupling the different components of modern machine learning systems. Unfortunately, writing code using popular tensor libraries is very challenging, because (a) the libraries expose the developers to a low-level, physical memory model (b) broadcast semantics between tensors of different sizes are adhoc and lead to surprising errors.

In this talk,

• We present a new language to specify tensor shapes and their transformations, by attaching "semantic" names to individual tensor dimensions.
• The shape annotations are library-agnostic, improve code readability, and make it easy to write semantic shape assertions and transformations.
• We present the tsalib library which integrates named shape annotations into existing Python tensor programs seamlessly using optional type annotations. With examples (self-attention in Transformers, convolution-sequence in Resnets), we illustrate how shape annotations improve code readability dramatically and even reduce the code size.

Shibashis Guha, TIFR, Mean-payoff adversarial Stackelberg games

Slides     Video

Abstract

We consider two-player nonzero-sum games played on bi-weighted graphs with the mean-payoff function. The adversarial Stackelberg value (ASV) of Player 0 (leader) is the largest value that she can obtain when announcing her strategy to Player 1 (follower) who in turn responds with any of his best responses. It is shown that the ASV is not always achievable. In the threshold problem, given a threshold, we check if the ASV is greater than the threshold. This problem is shown to be in NP. Besides, the ASV can be computed by an encoding using the theory of the reals with addition.

Next, we study these games under (i) modelling imprecisions - the weights on the edges of the game arena may not be exactly correct, they may be slightly away from the right one, and (ii) sub-optimal response of Player 1- he may play epsilon-optimal best-responses instead of best-responses. The optimal Player 0 strategies for ASV are shown to be fragile to such imprecisions, and a solution concept is suggested to obtain strategies that are robust to both modeling imprecision, and as well as to the epsilon-optimal responses of Player 1. We also study several algorithmic problems related to this solution concept.

This talk is based on the following two works.

1. The Adversarial Stackelberg Value in Quantitative Games by Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin
2. Fragility and Robustness in Mean-payoff Adversarial Stackelberg Games by Mrudula Balachander, Shibashis Guha, and Jean-François Raskin

Vrunda Dave, IIT Bombay, On the Separability Problem of String Constraints

Slides     Video

Abstract

In this talk, we will look at the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We will first see that regular separability of straight-line string constraints is undecidable. Later, in the quest of finding an effective decision procedure for separability of string constraints, we will look at a sequence of decision problems as we restrict the separator class and/or the string constraint class.

Joint work with: Parosh Abdulla, Mohamed Faouzi Atig, S Krishna