1,061 research outputs found
Behavioral automata composition for automatic topology independent verification of parameterized systems
No full textVerifying correctness properties of parameterized systems is a long-standing problem. The challenge lies in the lack of guarantee that the property is satisfied for all instances of the parameterized system. Existing work on addressing this challenge aims to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the cut-off. A property satisfied on the system with the cut-off ensures that it is satisfied for systems with any larger parameter. The major problem with these techniques is that they only work for certain classes of systems with specific communication topology such as ring topology, thus leaving other interesting classes of systems unverified. We contribute an automated technique for finding the cut-off of the parameterized system that works for systems defined with any topology. Given the specification and the topology of the system, our technique is able to automatically generate the cut-off specific to this system. We prove the soundness of our technique and demonstrate its effectiveness and practicality by applying it to several canonical examples where in some cases, our technique obtains smaller cut-off values than those presented in the existing literature.This is a manuscript of a proceeding published as Hanna, Youssef, Samik Basu, and Hridesh Rajan. "Behavioral automata composition for automatic topology independent verification of parameterized systems." In Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pp. 325-334. ACM, 2009. 10.1145/1595696.1595758. Posted with permission.</p
Golok: Push-button Verification of Parameterized Systems
No full textParameterized systems verification is a long-standing problem, where the challenge is to verify that a property holds for all (infinite) instances of the parameterized system. Existing techniques aim to reduce this problem to checking the properties on smaller systems with a bound on the parameter referred to as the "cut-off" such that if the property holds for system instances of size cut-off that implies that it holds for larger system instances. In most existing techniques, human guidance is required to deduce the invariants for the system's behavior, which are then used to compute cut-off. In contrast, we present an fully automatic sound method (but necessarily incomplete) for generating the cut-off that works for synchronous parameterized systems with heterogeneous processes communicating via single-cast and/or broadcast. Our technique is independent of the system topology and the property to be verified. Given the specification and the topology of the system, our technique generates the system-specific cut-off. We have realized our technique in a tool, Golok, which shows that it can be automated. We present the results of running Golok on 15 parameterized systems where we obtain smaller cut-offs than those presented in the existing literature for 14 cases.Copyright © 2011, Youssef Hanna, David Samuelson, Samik Basu, Hridesh Rajan. All rights reserved.</p
Bahumukhī mana, bahurupī prema
No full textThe document contains a novel written by the Bengali author Nirpendra Kumar Basu (1898-1979). The monograph is from the private collection of Sharmadip Basu
Outer Length Scales in Nocturnal Stable Boundary Layers
No full textRecently, Basu and Holstlag (2021) proposed a unified framework for describing outer length scales (OLS). By utilizing this framework, we document various characteristics of OLS in nocturnal boundary layers over the US Great Plains.Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.Atmospheric Remote Sensin
Cupid Joins the War
No full textThe author explores the history of love and sex in war though the ages. This monograph is from the private collection of Sharmadip Basu, Kolkata, W.B., India
Measuring the Impact of Influence on Individuals: Roadmap to Quantifying Attitude
No full textInfluence diffusion has been central to the study of propagation of
information in social networks, where influence is typically modeled as a
binary property of entities: influenced or not influenced. We introduce the
notion of attitude, which, as described in social psychology, is the degree by
which an entity is influenced by the information. We present an information
diffusion model that quantifies the degree of influence, i.e., attitude of
individuals, in a social network. With this model, we formulate and study
attitude maximization problem. We prove that the function for computing
attitude is monotonic and sub-modular, and the attitude maximization problem is
NP-Hard. We present a greedy algorithm for maximization with an approximation
guarantee of . Using the same model, we also introduce the notion of
"actionable" attitude with the aim to study the scenarios where attaining
individuals with high attitude is objectively more important than maximizing
the attitude of the entire network. We show that the function for computing
actionable attitude, unlike that for computing attitude, is non-submodular and
however is \emph{approximately submodular}. We present approximation algorithm
for maximizing actionable attitude in a network. We experimentally evaluated
our algorithms and study empirical properties of the attitude of nodes in
network such as spatial and value distribution of high attitude nodes.The following is a manuscript of an article published as Fu, Xiaoyun, Madhavan Padmanabhan, Raj Gaurav Kumar, Samik Basu, Shawn Dorius, and A. Pavan. "Measuring the Impact of Influence on Individuals: Roadmap to Quantifying Attitude." In 2020 IEEE/ACM International Conference on Advances in Social Networks Analysis and Mining (ASONAM), pp. 227-231. IEEE Computer Society, 2020. Copyright 2020 IEEE. Posted with permission
Magnanimous Kunti by Samaresh Basu/ সমরেশ বসুর কলমে মনস্বিনী কুন্তী
No full textSamaresh Basu wrote a number of books based on Puran-Mahabharata under the pseudonym Bhramar and Kalkoot. Such as, ‘Shamba (1978)’, ‘Juddher Sesh Senapati (1984)’, ‘Prachetas (1984)’, \u27Pritha (1986)\u27, ‘Antim Pranay (1987)’ etc. ‘Pritha’ was published in the magazine \u27Prasad\u27 under the pseudonym \u27Bhramar\u27. In such books, the author analyzed the traditional story of the Puranas in a new perspective.
One of the memorable Panchakanyas in Puranas, Empress Kunti has been recreated in the light of the author\u27s spirit in this book. In the present article we will discuss how the character of Kunti has been recreated by Samaresh Basu in \u27Pritha\u27.
At the beginning of the story, before reaching the context of Kunti, the author undertakes a very realistic analysis of heaven-hell, Gods-demons, Samhita era-Puranic era, male-female relationship, marriage customs, child birth and the position of women in society. Then he explained the solitude, self-immolation and transition of Kunti from a feminist perspective.
The story of love-marriage-motherhood-heroism-restraint-pain-sacrifice of this remarkable female character of Mahabharata has been captured in a new way in the unique writing of Kalkoot. Inventing many thoughtful arguments the author tried to establish the father-son relationship between Yudhisthira-Vidura and Karna-Durbasha. How the author incarnated new contexts in the familiar story of Mahabharata and how he made it acceptable by arranging relevant arguments in favour of his new thoughts – this essay will try to elaborate these points
SMT-based formal verification of safety properties in neural networks
No full textThough they have been around since the late 1950s, artificial neural networks, or just neural networks (NNs), were not commonly considered as a potential (practical to implement) solution to real-world problems until the last couple of decades, when the dive into deep learning and big data started to produce significant benefits. In this case, a real-world problem refers to one that is common outside the realm of scientific exploration and research. Applications of NNs continue to increase in number and variety. As implementations of these ideas become more practical, their applications reach safety-critical systems (e.g., autonomous vehicles), making the verification of their conformity to safety requirements more critical. One of the benefits of a NN is that its internals need not be explicitly coded in order to produce reasonable outputs, demonstrating the ``learning'' aspect of machine learning. However, this creates new issues with verification. There are many established formal methods of software verification, such as bounded model checking and counterexample guided abstraction refinement (CEGAR), but these do not directly translate to NN verification. When the behavior of a machine cannot be stored explicitly as every possible path from input to output, it is not trivial to ensure it functions properly. Enumeration of NN behavior is prohibitively expensive because of the nature and number of computations it performs. This is largely because NNs typically cannot be exhaustively tested in a practical, efficient, computation-friendly way. Fortunately, in recent years, scholars have found ways to bring traditional verification techniques into the world of NNs. This paper reviews three such methods, compares them, and analyzes their potential for future use. These methods are: abstraction refinement due to Pulina and Tacchella, pure-SMT solving due to Huang et al., and Reluplex due to Katz et al.</p
A model checking approach for analyzing and identifying intervention policies to counter infection propagation over networks
No full textThe spread of infections (disease, ideas, fires, etc.) in a network (group of people, electronic network, forest, etc.) can be modeled by the evolution of states of nodes in a graph defined as a function of the states of the other nodes in the graph. Given an initial configuration of the graph with a subset of the nodes infected, a propagation function that specifies how the states of the nodes change over time, and a quarantine function that specifies the generation of regions centered on the infected nodes, from which the infection cannot spread; we identify and verify intervention policies designed to contain the propagation of the infection over the network. The approach can be used to determine an effective policy in such a scenario
Extending substitutability in composite services by allowing asynchronous communication
No full textWeb services are programs that are self-contained, self-describing, interoperable, platform-independent, and accessible over a network. These properties allow several Web services to be combined together to form a Web service composition. However, when a component service within a Web service composition becomes unavailable or unusable, it is necessary to identify a substitute service that can replace the failed component while preserving the original functionality of the composition. This is the problem of Web service substitution.
Most existing work that addresses this problem requires strict functional equivalence between the original component and its substitute. In contrast, Pathak et al. have shown in 2007 that it is sufficient for a substitute service to provide the same functionality with respect to the rest of the composition as the component it is replacing. Pathak et al. apply a technique called quotienting to determine the portion of the composition's overall functionality that is satisfied by the original component. The quotienting operation yields the property that must be satisfied by a substitute for that component.
While the use of quotienting allows more possible substitute services to be accepted, it is possible to relax the substitutability condition even further by considering asynchronous communication between component services within the Web service composition model. Our work accomplishes this task by providing a formal framework for representing asynchronous communication within a Web service composition. In our framework, the asynchronous communication is encapsulated in a buffer process, which stores each message until a component is ready to consume it. We prove the correctness of our solution, describe our implementation, and discuss some directions for future research.</p
- …
