Kumar Madhukar, IIT Delhi, An Abstraction-Based Framework for Neural Network Verification
Deepak DSouza, IISc, Static Race Detection for Periodic Real-Time programs
Stanly Samuel, IISc, Bangalore, GenSys: A Scalable Fixed-Point Engine for Maximal Controller Synthesis over Infinite State Spaces
Sudakshina Dutta, IIT Goa, Semantic Program Alignment for Equivalence Checking
Abhishek Bichhawat, IIT Gandhinagar, Are you messaging securely?
Soumodev Mal, CMI, On the Satisfiability of Context-free String Constraints with Subword Ordering
Mayank Deora, ISI Kolkata, Neural Network Repair using Formal Methods
Mir Md Sajid Sarwar, IACS, Kolkata, A Contrastive Plan Explanation Framework for Hybrid System Models
Atanu Kundu, IACS, Kolkata, SAT-Reach: A Bounded Model Checker for Affine Hybrid Systems
Ashutosh Gupta, IIT Bombay, What does the heart want?
Tephilla Prince, IIT Dharwad, Two Dimensional Bounded Model Checking: A Novel Verification Strategy
Ravindra Metta, TCS Research, Bounded Model Checking +Fuzzing: Effective and Efficient Test generation
Divyesh Unadkat, TCS Research and IIT Bombay, Dance of the Dragons: Induction, Difference Computation and SMT Solving
Dhruv Nevatia, CMI, Register Systems through the Lens of Logic
Sorav Bansal, IIT Delhi and CompilerAI, The Compiler as a Database of Code Transformations
Shikha Singh, IIT Madras, Agents on Planet Kripke: Real or Deceptive
Rupashree Rangaiyengar, IISc, Bangalore, Program Analysis for Akka Programs
Kumar Madhukar, IIT Delhi, An Abstraction-Based Framework for Neural Network Verification
Abstract
This talk will be based on a CAV 2020 paper with the same title. The
paper addresses the scalability issue of neural network verification
approaches by proposing over-approximation of neural networks to reduce
their size. The over-approximation may be too coarse, in which case the
underlying verification tool might return a spurious counterexample.
Under such conditions, a counterexample-guided refinement is done to
adjust the approximation, and then the process is repeated. The
proposed approach is orthogonal to, and can be integrated with, many
existing verification techniques.
Towards the end, I will also be talking briefly about some related and possible future work on this topic.
Deepak DSouza, IISc, Static Race Detection for Periodic Real-Time programs
Abstract
We consider the problem of statically detecting data races in periodic
real-time programs that use locks, and run on a single processor
platform. We propose a technique based on a small set of rules that
exploits the priority, periodicity, locking, and timing information of
tasks in the program. One of the key requirements is a response time
analysis for such programs, and we propose an algorithm to compute this
for the case of non-nested locks. We have implemented our analysis for
real-time programs written in C in a tool called PEPRacer and evaluated
its performance on a small set of benchmarks from the literature.
This is joint work with Varsha Suresh, Rekha Pai, Meenakshi D'Souza, and
Sujit Chakraborty.
Stanly Samuel, IISc, Bangalore, GenSys: A Scalable Fixed-Point Engine for Maximal Controller Synthesis over Infinite State Spaces
Abstract
The synthesis of maximally-permissive controllers in infinite-state systems has many practical applications. Such controllers directly correspond to maximal winning strategies in logically specified infinite-state two-player games. In this paper, we introduce a tool called GenSys which is a fixed-point engine for computing maximal winning strategies for players in infinite-state safety games. A key feature of GenSys is that it leverages the capabilities of existing off-the-shelf solvers to implement its fixed point engine. GenSys outperforms state-of-the-art tools in this space by a significant margin. Our tool has solved some of the challenging problems in this space, is scalable, and also synthesizes compact controllers. These controllers are comparatively small in size and easier to comprehend. GenSys is freely available for use and is available under an open-source license.
Sudakshina Dutta, IIT Goa, Semantic Program Alignment for Equivalence Checking
Abstract
In this talk, a robust semantics-driven method for program equivalence checking will be explained. Given two functions, the method finds a trace alignment over a set of concrete executions of both programs and constructs a product program particularly amenable to checking equivalence. The algorithm is applicable to challenging equivalence problems beyond the scope of existing techniques. The correctness of the hand-optimized vector implementation of strlen that ships as part of the GNU C Library, as well as the correctness of vectorization optimizations for 56 benchmarks derived from the Test Suite for Vectorizing Compilers are verified using the method.
Abhishek Bichhawat, IIT Gandhinagar, Are you messaging securely?
Abstract
While many messaging apps claim end-to-end security of the exchanged
messages, there are no formal guarantees offered by the applications
regarding the same. To this end, we have built DY* (https://reprosec.org/dystar/),
which is a formal verification framework for the
symbolic security analysis of cryptographic
protocol code written in the F* programming
language. Unlike existing automated symbolic
provers, our framework accounts for advanced
protocol features like unbounded loops and mutable
recursive data structures, as well as low-level
implementation details like protocol state
machines and message formats, which are often at
the root of real-world attacks. We have
demonstrated the effectiveness of our framework
through several in-depth symbolic security
analyses of protocols like Signal, ISO-DH, ACME
and Noise.
In this talk, we will discuss the DY* framework, and a couple of
protocols that we have verified in the framework.
Soumodev Mal, CMI, On the Satisfiability of Context-free String Constraints with Subword Ordering
Abstract
String constraints impose constraints over variables that take strings
as assignments. Given a string constraint C, the satisfiability problem
asks if there is an assignment which satisfies every constraint in C.
Most classes of string constraints in their full generality although
have high expressive power turn out to be undecidable. Hence, a natural
direction to recover decidability is to consider meaningful subclasses
of such constraints. In this talk, we consider a variant of string
constraints given by membership constraints in context-free languages
and subword relation between variables. We call this variant
subword-ordering string constraints. The satisfiability problem for the
variant turns out to be undecidable (even with regular membership). We
consider a fragment in which the subword order constraints do not
impose any cyclic dependency between variables. We show that this
fragment is NEXPTIME-complete. As an important application of our
result, we establish a strong connection between the acyclic fragment
of the subword-ordering string constraints and acyclic lossy channel
systems, an important distributed system model. This allowed us to
settle the complexity of control state reachability in acyclic lossy
channel pushdown systems. The problem was shown to be decidable by Atig
et al. in 2008. However, no elementary upper bound was known. We show
that this problem is NEXPTIME-complete.
This is a joint work with C. Aiswarya and Prakash Saivasan.
Mayank Deora, ISI Kolkata, Neural Network Repair using Formal Methods
Abstract
This talk is based on two papers: 'Minimal Modifications of Deep Neural Networks using Verification', presented at the 23rd Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning LPAR 2020) and 'Minimal Multi-Layer Modifications of Deep Neural Networks (https://arxiv.org/abs/2110.09929)'. The first paper addresses the problem of Minimal Modification of Deep Neural Networks. This problem is reduced to the Neural Network verification problem, which is an easier problem than retraining the DNN. The solution given in the first paper is limited to modifying only a single layer whereas the second paper addresses the same problem by proposing a method that allows multiple layer modifications as well. The papers are accompanied with a software implementation and experimental results on a number of benchmarks.
Mir Md Sajid Sarwar, IACS, Kolkata, A Contrastive Plan Explanation Framework for Hybrid System Models
Abstract
In artificial intelligence planning, having an explanation of a plan given by a planner is often desirable. The ability to explain various aspects of a synthesized plan to an end-user not only brings in trust on the planner but also reveals insights of the planning domain and the planning process. Contrastive questions such as "Why action A instead of action B?" can be answered with a contrastive explanation that compares properties of the original plan containing A against the contrastive plan containing B. In this paper, we explore a set of contrastive questions that a user of a planning tool may raise and we propose a re-model and re-plan framework to provide explanations to such questions. Earlier work has reported this framework on planning instances for discrete problem domains described in the Planning Domain Definition Language (PDDL) and its variants. In this paper, we propose an extension for planning instances described by PDDL+ for hybrid systems which portray a mix of discrete-continuous dynamics. Specifically, given a mixed discrete continuous system model in PDDL+ and a plan describing the set of desirable actions on the same to achieve a destined goal, we present a framework that can integrate contrastive questions in PDDL+ and synthesize alternate plans. We present a detailed case study on our approach and propose a comparison metric to compare the original plan with the alternate ones.
Atanu Kundu, IACS, Kolkata, SAT-Reach: A Bounded Model Checker for Affine Hybrid Systems
Abstract
Bounded model checking (BMC) of hybrid systems is challenging due to the continuous system variables and an interplay between discrete and continuous system dynamics. Existing works reduce the BMC for hybrid systems to the satisfiability of SMT constraints encoding the hybrid system dynamics, solved consequently with efficient SMT solvers. However, the encoded constraints can be complex, and deciding its satisfiability can be difficult for hybrid systems with many modes and transitions and for large bounds. In this paper, we propose a bmc algorithm, particularly for hybrid systems with piecewise affine dynamics, modeled as an hybrid automaton. Our algorithm combines sat-solving based path enumeration of hybrid automata and symbolic state-space exploration along paths by flowpipe construction. We show that a synergy between symbolic state-space exploration and sat-based path enumeration can significantly benefit in path-pruning and in a directed exploration of the search-space. In addition, optimization techniques to reuse and share the symbolic states across paths have been proposed for efficiency. Finally, our bmc procedure searches for a concrete counterexample trajectory exploiting the constraints obtained from reachability analysis. The algorithm is implemented in the tool SAT-Reach, and we evaluate its performance in comparison with dReach, an SMT-solving based bounded model checker for non-linear hybrid systems, and XSpeed, Flow*, which are symbolic state-space exploration tools for affine and non-linear hybrid systems respectively. Experiments demonstrate the efficacy of our algorithm.
Ashutosh Gupta, IIT Bombay, What does the heart want?
Abstract
TBA
Tephilla Prince, IIT Dharwad, Two Dimensional Bounded Model Checking: A Novel Verification Strategy
Abstract
Bounded model checking (BMC) is an efficient formal verification
technique which allows for desired properties of a software system to
be checked on bounded runs of an abstract model of the system. The
properties are frequently described in some temporal logic and the
system is modeled as a state transition system. We propose a counting
logic L_{C}, to describe the temporal properties of
client-server systems with an unbounded number of clients. We also
propose two dimensional bounded model checking (2D-BMC) strategy that
uses two distinguishable parameters, one for execution steps and
another for the number of tokens in the net representing a
client-server system, and these two evolve separately, which is
different from the standard BMC techniques in the Petri Nets formalism.
This 2D-BMC strategy is implemented in a tool called DCModelChecker
which leverages the 2D-BMC technique with a state-of-the-art
satisfiability modulo theories (SMT) solver Z3. The system is given as
a Petri Net and properties specified using L_{C} are
encoded into formulas that are checked by the solver. Our tool can also
work on benchmarks from the Model Checking Contest (MCC). As ongoing
work, we apply the 2D-BMC strategy to models with distinguishable
clients and describe their properties using a suitable logic.
This is joint work with Ramchandra Phawade and S. Sheerazuddin.
Ravindra Metta, TCS Research, Bounded Model Checking +Fuzzing: Effective and Efficient Test generation
Abstract
Coverage Guided Fuzzing (CGF) is a greybox test generation technique. Bounded Model Checking (BMC) is a whitebox test generation technique. Both these have been highly successful at program coverage as well as error detection. It is well known that CGF fails to cover complex conditionals and deeply nested program points. BMC, on the other hand, fails to scale for programming features such as large loops and arrays. To alleviate the above problems, we (1) combined BMC and CGF by using BMC for a short and potentially incomplete unwinding of a given program to generate effective initial test prefixes, which are then extended into complete tes inputs for CGF to fuzz, and (2) in case BMC gets stuck even for the short unwinding, we automatically identify the reason and appropriate remedial strategy, and rerun BMC with the corresponding remedial strategy. We call this approach as BMCFuzz and implemented it in the VeriFuzz framework. This implementation was experimentally evaluated by participating in Test-Comp 2021 and the results show that BMCFuzz is both effective and efficient at covering branches as well as exposing errors. In this talk, we present the details of BMCFuzz and our analysis of the experimental results.
Divyesh Unadkat, TCS Research and IIT Bombay, Dance of the Dragons: Induction, Difference Computation and SMT Solving
Abstract
Proving correctness of array programs is an immensely daunting task. In
this talk, we show how the magical powers of the three dragons,
Mathematical Induction, Difference Computation and SMT Solving can be
used to breathe fire on this challenge. During the dance, dragons take
turns to aid each other in attacking the problem. We call the dance,
with non-trivial but elegant transformational steps, as 'Full-Program
Induction'. It can eviscerate the task of proving quantified as well as
quantifier-free properties of array manipulating programs, notably
without relying on other dragons such as loop specific invariant
generation. Gizmos like Vajra and Diffy have been built to hone this
dance of the dragons. The strife of verifying properties in massive
armies of array benchmarks has been charred with immense efficacy
within seconds using these gizmos.
This is a joint effort with Prof. Supratik Chakraborty and Prof.
Ashutosh Gupta. The presentation is based on our publications at CAV
2021, TACAS 2020 (and it's extended journal version to appear in STTT
2022).
Dhruv Nevatia, CMI, Register Systems through the Lens of Logic
Abstract
In this talk, we shall analyse register systems over graph databases,
over an infinite data domain. We define a model of non-deterministic,
2-way, concurrent register automata walking on the underlying graphs of
graph databases. We then consider the following problem: Given a family
of graph databases where the underlying graphs are described by an
HR-equational system, and such a concurrent graph walking register
automaton, is some graph database in the family accepted by the
automaton? The general problem is undecidable even for multi-head DFA
(deterministic with no registers) over non-data words. I shall show
that a bounded version of this problem is decidable.
We shall start by describing behaviours using graphs with data
constraints. The bounded problem can then be reduced to the
MSO-satisfiability problem over HR-equational graphs, which is known to
be decidable using Courcelle's Recognizability theorem. This technique
gives a uniform approach for the analysis of a wide class of register
systems over graph databases.
Some non-trivial applications of these results include the decidability
of the satisfiability problem for the positive fragment of vertical
XPath (also closed under path intersection and order tests) and the
emptiness problem for concurrent graph transition systems over
series-parallel graphs as well as register pushdown automata over data
words.
Sorav Bansal, IIT Delhi and CompilerAI, The Compiler as a Database of Code Transformations
Abstract
A modern compiler is perhaps the most complex machine developed by humankind. Yet it remains fragile and inadequate for meeting the demands of modern optimization tasks necessitated by Moore's law saturation. In our research, we explore a different approach to building compiler optimizers that is both completely automatic and more systematic. The basic idea is to use AI-style search techniques to automatically discover replacement rules that resemble peephole optimizations. A key component of this compiler architecture is an equivalence checker that validates the optimization rules automatically. I will describe the overall scheme, and delve into some interesting details of automatic equivalence checking. I will also share our recent work on automatic generation of debugging headers using our equivalence checker. This talk is based on work published at ASPLOS06, OSDI08, SOSP13, APLAS17, HVC17, SAT18, PLDI20, OOPSLA20, and CGO22.
Shikha Singh, IIT Madras, Agents on Planet Kripke: Real or Deceptive
Abstract
TBA
Rupashree Rangaiyengar, IISc, Bangalore, Program Analysis for Akka Programs
Abstract
TBA