FMI: Formal Methods Update Meeting 2022

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

Slides

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

Slides

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

Slides

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?

Slides

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

Slides

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

Slides

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

Slides

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

Slides

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.

Tephilla Prince, IIT Dharwad, Two Dimensional Bounded Model Checking: A Novel Verification Strategy

Slides

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

Slides

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

Slides

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.

Abstracts