Centre for Formal Design
and
Verification of Software

Wednesday Seminars

Next SeminarSeminar ListingHome




March

Seminar-14-03-3
Date- 19th March 2014
Time- 03:15 PM
Speaker- Sumedh Tirodkar, Ph.D. student, Dept. of CSE
Title- Online preemptive matching (lower bound)
Venue- CFDVS Conference room, IIT Bombay.

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
  1. Improved Bounds for Online Preemptive Matching, STACS, 2013 by L. Epstein, A. Levin, D. Segev, O. Weimann.
  2. Finding graph matchings in data streams, APPROX, 2005 by A. McGregor.
  3. Buyback problem ÿÿ approximate matroid intersection with cancellation costs, ICALP, 2011 by A. Badanidiyuru Varadaraja.


Seminar-14-03-2
Date- 12th March 2014
Time- 03:15 PM
Speaker- Sreejith A V, Visiting Fellow at the School of Technology and Computer Science, TIFR
Title- First order logics extended with counting quantifiers
Venue- CFDVS Conference room, IIT Bombay.

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 non-trivial ways giving some interesting results and lots of open problems. Many of these open problems closely relate to those in circuit complexity.

References
  1. Finite Automata, Formal Logic, and Circuit Complexity. by Howard Straubing
  2. Descriptive complexity by Neil Immerman .
  3. Crane Beach Conjecture. by Barrington, Immerman, Lautemann, Schweikardt, and Therien.
  4. Definability of Languages by Generalized First-order Formulas over (N,+). by Roy and Straubing.
  5. Non-definability of Languages by Generalized First-order Formulas over (N, +). by Krebs and Sreejith .


Seminar-14-03-1
Date- 5th March 2014
Time- 03:15 PM
Speaker- Sumedh Tirodkar, Ph.D. student, CSE
Title- Online Preemptive Matching
Venue- CFDVS Conference room, IIT Bombay.

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
  1. Improved Bounds for Online Preemptive Matching. by L. Epstein, A. Levin, D. Segev, O. Weimann.
  2. Finding graph matchings in data streams. by A. McGregor.
  3. Buyback problem approximate matroid intersection with cancellation costs. by A. Badanidiyuru Varadaraja.


February

Seminar-14-02-1
Date- 26th February 2014
Time- 03:15 PM
Speaker- Dipak Chaudhari, Ph.D. student, Dept. of CSE
Title- Derivation of Imperative Programs from Specifications
Venue- CFDVS Conference room, IIT Bombay.

Show Details

Abstract

The prevalent implement-and-verify 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 bug-free. 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 ad-hoc use cases and informal reasoning to guess the program constructs.
"Calculational Style of Programming" is a correct-by-construction 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 error-prone. 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
  1. Syntax-guided synthesis. by Rajeev Alur et al.
  2. Combinatorial sketching for finite programs. by Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat.
  3. Refinement Calculus: A Systematic Introduction. by Ralph J. Back and Joakim Wright.
  4. A Discipline of Programming. by Edsger Wybe Dijkstra.
  5. Programming: The Derivation of Algorithms. by Anne Kaldewaij


January

Seminar-14-01-1
Date- 8th January 2014
Time- 03:00 PM
Speaker- Mr. Kuldeep Singh Meel, Ph.D. student, Rice University, USA
Title- Sampling Techniques for Constraint Satisfaction and Beyond
Venue- CFDVS Conference room, IIT Bombay.

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, computer-aided verification and formal methods. He is the recipient of the 2013 Andrew Ladd fellowship.

References
To be updated


Seminar-14-01-2
Date- 15th January 2014
Time- 3:30 PM
Speaker- Prof. Paul Gastin
Title- SPECIFICATION AND VERIFICATION OF QUANTITATIVE PROPERTIES VIA EXPRESSIONS, LOGICS, AND AUTOMATA
Venue- CFDVS Conference room, IIT Bombay.

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, first-order 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 co-director of the Indo-French International Laboratory (InForMeL). His research domain is the verification and control of safety critical systems, with a focus on concurrent and real-time systems. His works include models for such systems (distributed, quantitative, real-time 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
[   Home  |   CSE  |   IIT Bombay  |   Contact  ]
For suggestions and comments contact: Webmaster