and Verification of Software 
Wednesday SeminarsNext SeminarSeminar ListingHomeMarch Seminar14033
Show Details Abstract The Maximum Weight Matching (MWM) problem is considered in the online preemptive setting. Edges of underlying graph are presented one after other. At every stage the given edge has to be either accepted or rejected in the current matching. Once rejected, the edge can never be considered again in current matching. Once accepted, the edge can be later on removed from current matching. The goal is to output a Maximum Weight Matching. The deterministic upper and lower bounds for the competitive ratio for this problem are tight. But there is a large gap between randomised upper and lower bounds. We wish to fill this gap. In last talk, I spoke on the randomized algorithm. In this talk, I will discuss the lower bound due to Epstien et.al. References
Seminar14032
Show Details Abstract In this talk, we shall look at logics over words. It is known that first order logic (FO) with an order relation, <, defines exactly the set of all aperiodic regular languages. This class of languages is known to be a strict subset of regular languages. The difficulty of first order logic is its inability to count. Can we overcome this if we allow other relations? We will see that an addition predicate, +, is not very helpful. What about multiplication? Suddenly we see that one can count to log of the word length. Hence, the "Crane Beach conjecture" turns out to be false for this logic. Will adding extra predicates help us count more? We see that no predicate can enhance the counting capability further. For example, the language L="set of all words with even number of a's" is not definable in FO with any set of relations. How can we enhance the counting capability? Introducing modulo counting quantifiers (or other regular quantifiers) is one way. We will see that these quantifiers interact with addition and multiplication in highly nontrivial ways giving some interesting results and lots of open problems. Many of these open problems closely relate to those in circuit complexity. References
Seminar14031
Show Details Abstract The Maximum Weight Matching (MWM) is considered in the online preemptive setting. Edges of underlying graph are presented one after other. At every stage the given edge has to be either accepted or rejected in the current matching. Once rejected, the edge can never be considered again in current matching. Once accepted, the edge can be later on removed from current matching. The goal is to output a Maximum Weight Matching. The deterministic upper and lower bounds for the competitive ratio for this problem are tight. But there is a large gap between randomised upper and lower bounds. We wish to fill this gap. In this talk, I will discuss the upper and lower bounds due to Epstien et.al. References
Seminar14021
Show Details Abstract The prevalent implementandverify software development methodologies typically involve an implementation stage and a separate verification stage. Testing/Formal verification is usually employed to gain confidence that the implemented programs are bugfree. Although the failed test cases or the failed proof obligations provide some hint, there is no structured help available to the user in the actual task of implementing the programs. Programmers rely on adhoc use cases and informal reasoning to guess the program constructs. "Calculational Style of Programming" is a correctbyconstruction programming methodology wherein programs and the correctness proofs are systematically derived together from the formal specifications. Program constructs and the associated invariants are naturally discovered during the program derivation process. However, carrying out the calculational derivations manually is cumbersome and errorprone. We have developed a framework, Progsynth, for calculational derivation of programs wherein program and formula transformations are performed coherently. Our objective has been two fold. Firstly, we automate the mundane formula manipulations and various proof tasks involved in the calculational derivations. We have designed powerful transformation rules by employing an external theorem prover (SMT solver, Z3) in addition to using the prevalent rewrite based techniques. Secondly, we capture the high level program derivation heuristics in the form of synthesis tactics to provide the user with guidance. In this talk, I will first introduce the calculational approach and then present the ProgSynth framework and its various features. With the help of a simple example, I will then explain how ProgSynth enables users to focus on the creative aspect of the program derivation process by taking care of underlying details. References
Seminar14011
Show Details Abstract Constraint problems have played a key role in diverse areas spanning testing, formal verification, planning, inferencing and the like. Apart from the classical problem of checking satisfiability, the problems of generating satisfying assignments randomly and of counting the total number of satisfying assignments have also attracted significant theoretical and practical interest over the years. Prior work offered heuristic approaches with no guarantee of solution distribution, and approaches with proven guarantees, but poor performance in practice. In this talk, I will describe a novel approach based on limited independent hashing and present two practical algorithms, UniWit and ApproxMC, for solving these two fundamental problems. Unlike prior work, our algorithms provide strong theoretical guarantees and also scale better to large problem sizes. Speaker's Profile: Kuldeep Singh Meel graduated with a B.Tech. in Computer Science and Engineering from IIT Bombay in 2012. He is currently a PhD student in Rice University, working with Prof. Moshe Vardi (and Supratik Chakraborty at IIT Bombay). His research broadly falls in the intersection of program synthesis, computeraided verification and formal methods. He is the recipient of the 2013 Andrew Ladd fellowship. References To be updated Seminar14012
Show Details Abstract Automatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous tools, both in academics and industry, allowing the verification of Boolean properties — those that can be either true or false. Current needs evolve to a finer analysis, a more quantitative one. Examples of quantitative properties are the lifespan of an equipment, the energy consumption of an application, the reliability of a program, or the number of results matching a database query. Expressing these properties requires new specification languages, as well as algorithms checking these properties over a given structure. In this talk, we will investigate several formalisms, equipped with weights, able to specify such properties : denotational ones — like regular expressions, firstorder logic with transitive closure, or temporal logics — or more operational ones, like navigating automata, possibly extended with pebbles. A first objective is to study some expressiveness results comparing these formalisms. In particular, we give efficient translations from denotational formalisms to the operational one. These objects, and the associated results, are presented in a unified framework of graph structures. This permits to handle finite words and trees, nested words, pictures or Mazurkiewicz traces, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modeling databases for example), or natural language processing. Second, we tackle some of the algorithmic questions that naturally arise in this context, like evaluation and satisfiability. In particular, we study some decidability and complexity results of these problems depending on the underlying semiring and the structures under consideration (words, trees...). Finally, we consider some interesting restrictions of the previous formalisms. Some permit to extend the class of semirings on which we may specify quantitative properties. Another is dedicated to the special case of probabilistic specifications : in particular, we study syntactic fragments of our generic specification formalisms generating only probabilistic behaviors. Speaker Profile: Prof Paul Gastin is a professor of computer science and the current head of the computer science department at Ecole Normale Superieure (ENS) de Cachan, France. He is also the codirector of the IndoFrench International Laboratory (InForMeL). His research domain is the verification and control of safety critical systems, with a focus on concurrent and realtime systems. His works include models for such systems (distributed, quantitative, realtime automata, sequence diagrams, Mazurkiewicz traces); specification formalisms such as temporal logics (expressivity, decidability, complexity); and the development of efficient algorithms for verification and control. References To be updated 
People —> Principal Investigators —> Research Employees —> Students Activities —> Weekly Meetings —> Formal Methods Update '05 —> Workshop'05 —> Workshop 2002 —> Workshop 2017 Projects —> R & D Projects —> Sponsored Projects —> Exploratory Projects Papers/Reports —> Papers —> Technical Reports —> Theses Download —> Course Material —> Online documentation Others —> Photographs —> Internal Website —> Webmail 

