Sumanth Prabhu, TCS Research and IISc Bangalore, Specification Synthesis with Constrained Horn Clauses
Soumyadip Bandyopadhyay and Rakshit Mittal, BITS Pilani, Goa Campus, Translation Validation of Loop involving Code Optimizing Transformations using Petri Net based Models of Programs
Akshatha Shenoy, TCS Research, Property Directed Self Composition
Divyesh Unadkat, TCS Research and IIT Bombay, Exploiting Induction and Difference Computation to Verify Array Programs
Rahul Sharma, Microsoft Research, Machine Learning with 2KB RAM
Subodh Sharma, IIT Delhi, Analysis of Release-Acquire Concurrency with Partial Order Domain
Akash Lal, Microsoft Research, Learning-based Controlled Concurrency Testing
Sreejith A V, IIT Goa, Regular languages over countable words
Supratik Chakraborty, IIT Bombay, Counter-example guided repair in Boolean functional synthesis
K V Raghavan, IISc Bangalore, Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains
Priyanka Golia, IIT Kanpur and NUS, Program Synthesis as Dependency Quantified Modulo Theory
Govind R, Universite de Bordeaux and CMI, Partial order reduction for timed systems
Missula Meghana, IIT Bombay, Automated inference of production rules for glycans
Krishna S, IIT Bombay, Verification of Concurrent Programs under Release Acquire
Akshay S, IIT Bombay, Can Zones be used to analyze pushdown timed automata? — a simulations-vs-equivalence story!
Nishant Sinha, OffNote Labs, The Shape of U — Befriending Tensors
Shibashis Guha, TIFR, Mean-payoff adversarial Stackelberg games
Vrunda Dave, IIT Bombay, On the Separability Problem of String Constraints
Sumanth Prabhu, TCS Research and IISc Bangalore, Specification Synthesis with Constrained Horn Clauses
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
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
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
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
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
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
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
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
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
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
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
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
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
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!
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
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,
Shibashis Guha, TIFR, Mean-payoff adversarial Stackelberg games
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
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