[FM-India] ICTAC 2012 School on Software Engineering

[Madhavan Mukund]

ICTAC 2012 School on Software Engineering

A School on Software Engineering is being organized as a part of ICTAC
2012, on Monday, 24th September 2012, at IIIT, Electronics City,
Bangalore. The school will feature four invited talks in the area of
Formal Methods for Software Engineering. All the talks will be
delivered in tutorial-style and will be accessible to Master’s
students and Ph.D scholars working in this area.

Registration

There is no fee to attend the School on Software Engineering. However
participants are required to register for the school at:

    www.iarcs.org.in/ictac2012/sesregform.php

A limited amount of support for travel by bus or train is available for
participants from academic institutions. To apply for travel
support, please email details including from station, mode of travel, and
amount of support required, to ictac2012 at iist.unu.edu, by 31st August
2012.

More details about the school are available at
http://www.iiitb.ac.in/ictac/School-on-Software-Engineering.html.

Talks:

1. Supratik Chakraborty, IIT Bombay

Title:  Abstract Interpretation in Software Model Checking

Abstract: Abstract interpretation is a powerful framework for static
analysis of programs. Since its introduction almost four decades back by
Patrick Cousot and Radhia Cousot, this has continued to be an
active area of research for those interested in program analysis
and/or program verification. Automated tools for software model
checking have successfully made use of abstract interpretation
techniques over the years to analyze real-life programs. This tutorial is
intended to familiarize the audience with the basic theory of
abstract interpretation, and also demonstrate through example tools how
the theory can be applied for practical program verification. We will
focus primarily on assertion checking in numerical and
heap-manipulating sequential programs as application areas, and also look
at some challenges that remain to be solved.


2. Peter Mueller, ETH, Zurich

Title: Verification of Concurrent Programs with Chalice

Abstract: A program verifier is a tool that allows developers to prove
that their code satisfies its specification for every possible input and
every thread schedule. This lecture describes a verifier for
concurrent programs called Chalice. Chalice’s verification methodology
centers around permissions. A memory location may be accessed by a thread
only if that thread has permission to do so. Proper use of
permissions allows Chalice to deduce upper bounds on the set of
locations modifiable by a method and guarantees the absence of data races
for concurrent programs. Verification in Chalice is automatic and modular.


3. Komondoor V Raghavan, Indian Institute of Science, Bangalore

Title: Modeling of software systems using Alloy

Abstract: Modeling and analysis of the user’s requirements is the key,
preliminary phase in the design and development of any software
system. The state of the practice for this in industry is to use
informal techniques such as textual requirements and UML
diagrams. Using formal, semantics-based tools makes this process more
rigorous, and helps designers to exhaustively capture and analyze the
requirements. This, in turn leads to good designs, and reduced risk of the
system ultimately failing to meet user’s requirements. Alloy
<http://alloy.mit.edu> is a tool for abstract modeling and analysis of the
data entities in a software system, using relational logic. In this
tutorial we will present the key capabilities of Alloy via a
demo, and will also discuss the algorithms used internally within
Alloy for analyzing data models.


4. Nishant Sinha, IBM Research, Bangalore

Title: Finding Bugs in Concurrent Programs via Constraint Solving

Abstract: Finding bugs in concurrent programs is challenging because it
involves examining a large number of thread interleavings together with
complex sequential reasoning over potentially infinite set of data values.
Bug finding by enumerating the entire set of data values and interleavings
is impractical. Therefore, symbolic techniques have been developed to
reason over a set of data values and interleavings simultaneously. A
popular symbolic technique involves transforming the given program into a
set of first-order logic constraints, such that a solution to those
constraints corresponds to a feasible error trace in the original program.
In this tutorial we will overview the modern DPLL-based constraint solving
technology and describe how to obtain first-order logic constraints in a
systematic and efficient manner starting from concurrent programs written
in the C language.

======================================================================