Software Engineering Seminar

You may subscribe to meyer-seminar Google group to receive information about forthcoming sessions.

Forthcoming sessions

About the seminar

The Seminar is a forum for discussions of programming methodology, software verification, and software engineering in general. The seminar is open to all those who want to participate. Talks are in English or Russian.

The seminar includes both research presentations and surveys. We welcome presentations of both kinds by all members of the local software engineering community and by visitors! If you are interested in presenting a talk, please write to Lidia Perovskaya (lperovskaya+sev@gmail.com).

Schedule (updated 16.06.2011)

After discussion with participants, we decided on the following schedule as best for most people:

• Thursday, 18–21
• Friday, 18–21

By default, Thursday sessions will be by ITMO members and Friday by guests, but this is only a general guideline. Depending on visitors’ schedule we may organize sessions at other times.

Practical details

Unless otherwise indicated, the sessions take place at ITMO (Sytninskaya Ploschad, Saint Petersburg), room 218. (Occasionally, sessions will take place other Saint Petersburg universities).

If you are not from ITMO, you will need to be registered with ITMO security. Please fill in the form here or write to Lidia.

Past sessions

Friday, 13 January 2012

19:30–21:00 Bertrand Meyer: The varieties of loop invariants

Abstract

The key practical issue in verifying software is to come up with the right loop invariants. We are performing an extensive analysis of loop invariants in important algorithms across all major areas of computer science, and have developed a taxonomy. I will present some of the results of this ongoing work, performed with Sergey Velder (ITMO) and Carlo Furia (ETH).

Thursday, 12 January 2012

16:00–17:30 Bertrand Meyer: Technically speaking!

Abstract

A good technical talk requires good technical work; that is the essential condition, but it is not sufficient. Too many good science and technology efforts are damaged by bad presentation. Conversely, good presentation can give your research the exposure and appreciation it deserves.
In this talk I will explain the fundamental rules of good technical presentations (доклады), derived from having observed hundreds of technical and scientific presentations over the years, some of them outstanding and many that would have benefitted from better lecturing skills. The topics include managing time, choosing what to focus on, devising effective slides (e.g. PowerPoint), interacting with the audience, avoiding typical mistakes, using technical English properly, and the other ingredients that can make the difference between a so-so technical talk and one that the audience will remember for a long time.
The talk will be in English and the discussion in English and Russian.

Thursday, 29 December 2011

18:00–19:00 Nadia Polikarpova: API design with strong specifications

Abstract

Designing good APIs is hard, and most recommendations on the topic given in the literature are very informal and difficult to apply. This talk discusses how strong behavioral specifications help construct better APIs by avoiding over-abstraction and inconsistencies in class hierarchies. We introduce model-based contracts: a methodology to equip object-oriented components with expressive and structured specifications, and to evaluate their completeness.
As an example, this talk presents EiffelBase2 — a data structure library for Eiffel, developed from the start with strong specifications and with the ultimate goal of proving its full functional correctness. We focus on how strong specifications solidify the design of the library, improve its usability and enable more extensive verification.

19:00–20:00 Bertrand Meyer: Agile methods: the good, the hype and the ugly

Abstract

Agile methods (such as Extreme Programming, Scrum and Lean Software) are a remarkable mix of very good, unremarkable and very bad ideas. This short presentation summarizes the key agile ideas and analyzes which ones software projects should retain and which they should reject.

Thursday, 1 December 2011

18:00–19:00 Ben Livshits, Microsoft Research: Rozzle: De-Cloaking Internet Malware with Multi-Execution (slides: download)

Abstract

This talk focuses on the interaction between static and runtime analysis on a large scale. In recent years, attacks that exploit vulnerabilities in browsers and their associated plugins have increased significantly. These attacks are often written in JavaScript and literally millions of URLs contain such malicious content. While static and runtime methods for malware detection been proposed in the literature, both on the client side, for just-in-time in-browser detection, as well as offline, crawler-based malware discovery, these approaches encounter the same fundamental limitation. Web-based malware tends to be environment-specific, targeting a particular browser, often attacking specific versions of installed plugins. This targeting occurs because the malware exploits vulnerabilities in specific plugins and fail otherwise. As a result, a fundamental limitation for detecting a piece of malware is that malware is triggered infrequently, only showing itself when the right environment is present. In fact, we observe that using current fingerprinting techniques, just about any piece of existing malware may be made virtually undetectable with the current generation of malware scanners.
We propose Rozzle, a JavaScript multi-execution virtual machine, as a way to explore multiple execution paths within a single execution so that environment-specific malware will reveal itself. Using large-scale experiments, we show that Rozzle increases the detection rate for offline runtime detection by almost seven times. In addition, Rozzle triples the effectiveness of online runtime detection. We show that Rozzle incurs virtually no runtime overhead and allows us to replace multiple VMs running different browser configurations with a single Rozzle-enabled browser, reducing the hardware requirements, network bandwidth, and power consumption.

19:00–20:00 Alexander Gavrilov: Microsoft Solutions Framework Essentials (slides: download)

Abstract

Microsoft Solutions Framework (MSF) provides proven practices for planning, building, and deploying a variety of technology solutions, combining aspects of software design and development and building and deploying infrastructure into a single project lifecycle for guiding technology solutions of all kinds. MSF helps developers achieve a delicate balance of flexibility while meeting commitments; speed while minimizing risk.

Thursday, 24 November 2011

18:00–19:00 Lidia Perovskaya: Agile, Scrum, XP: religion, propagation, cult, theory and practice

Abstract

Extreme programming and other close techniques are extremely popular and common in software engineering now, but it's not clear yet, are they really effective or not.
Authors of Agile Manifesto are giving promo-cources all over the world, but it is unknown, are they efficient enough. This talk would be a critical overview of XP, survey on main XP ideas and papers about XP efficiency.

Thursday, 10 November 2011

18:00–20:00 Andrey Tikhomirov and Anton Bannykh: Proving and disproving in first-order logic (Vampire)

Abstract

This will be survey talk about Vampire (automated theorem prover). I will describe specific algoritms and approaches applied to problems in the first-order logic. The talk is based on Andrey Vornkov's LASER'2011 course.

Friday, 28 October 2011

18:00–19:00 Mikhail Moiseev and Alexey Zakharov: Static Analysis Method for Deadlock Detection in SystemC Designs

Abstract

One of the goals of SystemC is high level system design verification at the early stage. Currently, simulation is widely used for this purpose. As the level of design parallelism grows, efficiency of simulation-based verification methods decreases. Thus different formal verification methods for SystemC are actively researched.
We present an approach to deadlock detection in SystemC designs based on static code analysis. Our approach to static analysis considers SystemC scheduler semantics. The developed approach has been implemented in Deadlock Analyzer tool.We demonstrate efficiency of our tool by applying it to dining philosophers, crossroads, producer-consumer cases and to a reallife model of video accelerator.

19:00–20:00 Anton Bannykh: The Coq proof assistant

Abstract

Coq is a proof assistant, that is an interactive environment where the user can define objects and prove theorems. Objects in Coq are either concrete data such as integers and trees, or abstract notions such as sets and relations. A proof in Coq is translated into a concrete term which is checked by a trusted kernel. From a Coq development, it is also possible to extract an Ocaml or Haskell program which, by construction, will be correct with respect to the specification given and proven in Coq.
The talk will cover basic aspects of the language and the proof environment.

Thursday, 20 October 2011

18:00–19:00 Vladimir Itsykson: Automated Program Transformation for Migration to New Libraries

Abstract

In modern software engineering the task of migration from one system environment to another may arise very often (e.g. software migrating from Windows to Linux or from desktop PC to some mobile platform). This task may be accomplished manually, but this will certainly be not cost- and time-effective and will require additional testing and verification. Therefore various automated techniques aimed to solve this problem seem to be very useful.
The talk takes into consideration one of such approaches, mainly focused on transferring source code between two library environments. The main idea of proposed approach is usage of formal library specifications. These specifications are described by means of partial specification language called PanLang. Source code porting is carried out automatically based on semantics of both libraries.

19:00–20:00 Mikhail Glukhikh: Software Reliability Estimation Based on Static Error Detection

Abstract

The estimation of a programs' reliability is an essential part in the process of software development. Existing methods for the analysis of software reliability are based on run-time data, program metrics, and properties of development process or program architecture. The disadvantage of these methods is that they use indirect information about the errors, which are the main cause of program unreliability. In our talk we will present a novel approach for software reliability estimation. This approach is based on error detection using static source code analysis. We extend static analysis with developed algorithms which calculate error probabilities and program reliability characteristics. The characteristics are the probability of successful program termination, the probability of the program is operable after execution of n statements, and mean number of executed statements before failure.

Thursday, 13 October 2011

18:00–19:00 Andrey Tikhomirov: Software model checking via systematic testing

Abstract

This will be survey talk about systematic testing. I will describe several tools from Microsoft Research: DART and SAGE.

19:00–20:00 Anton Bannykh: Using an automatic program verifier (Dafny) (slides: download)

Abstract

Dafny is both language and program verifier. It is high-level, fully automatic, based on Boogie and produces both reasonable feedback on failure and C# code on success.

Thursday, 6 October 2011

19:00–21:00 Dmitry V. Koznov: Research projects of Saint-Petersburg State University CASE-technologies laboratory

Abstract

The main topic area for the CASE-technologies lab is visual modeling (UML, BPMN, DSM, etc.). Three current research projects of the lab will be presented: Docline, Imrpoving public services, v2v transformations.
Docline project is dedicated to development of a method and tool for documentation reuse. The project is based on Docbook (Unix/Linux XML language for document development) and provides parameterized reuse of documentation. The approach also provides diagram support for documentation reuse design, refactoring of documentation and tool for Eclipse. Mainly, we address the approach to product line development. There is a branch of the approach for model-driven Web-application development: we provide traceability from models (WebML/WebRatio) to user documentation (DocLine). Now we consider various perspectives to integrate the approach with different high-level software development methods, which support reuse, providing traceability from software specifications to software documentation and back (e.g. aspect oriented approach).
Project <Imrpoving public services> is dedicated to modeling e-government services. Actually, a lot of information is connected with such services. But usually a user gets long text sheets with huge number of details and variants, and not all of them are related to his problem. We suggest an idea to provide a friendlier web-interface to expose to the user only the information one needs. We plan to use model based approach for internal organization of content, collection of information about services and for new user interface metaphors. Project is supported by the ENPI program, for supporting a Finnish-Russian cross-broader cooperation (2011–2013).
v2v transformation (view to view) approach addresses to a well-known multi-view problem in a model driven approach. We suggest an idea of formal specification of view transformations, which can be easily implemented in the context of graphical editors. Showing/unshowing UML classes, which are associated with a selected one, or showing/unshowing inheritance hierarchy for selected class — are examples of v2v transformations. We also are developing a toolset that is integrated with the Eclipse Modeling Project.

Thursday, 22 September 2011

18:00–19:00 Bertrand Meyer: Multirequirements: Giving software requirements their due

Abstract

Note: this will be a dry run of my talk at SEC-R (http://www.secr.ru/lang/en-en/key-speakers/bertrand-meyer). I expect to revise it extensively for the conference so do not expect a fully debugged presentation!
Everyone knows (in spite of the agile propaganda) that requirements are critical for software systems quality, but in practice many projects define requirements poorly. One of the biggest obstacles is that people often treat requirements definition as a separate activity and the requirements themselves as a separate product of the software lifecycle. The notion of multirequirements, introduced in this talk, rehabilitates requirements as a first-class citizen in the software lifecycle.
Multirequirements result from a radically new view, seamlessly integrating requirements with the other processes and products of software engineering. They subsume the classical opposition between formal and informal approaches to requirements engineering, and combine many styles: textual, mathematical, graphical. Rather than yielding a separate product, multirequirements are closely intertwined with other artifacts of the software lifecycle, such as design and implementation, supporting the key goal of traceability. They take full advantage of object-oriented ideas, which can be as effective for requirements as they are for programming.
The talk will present the notion of multirequirements, illustrate it through a number of examples, contrast it with older approaches such as model-driven engineering, and discuss its role in a modern, seamless style of object-oriented software development.

19:00–20:00 Sergey Velder: Survey of Abstract Interpretation

Abstract

This will be a survey talk on methods of sound approximation of computer program semantics based on abstract interpretation. This technique was introduced by Patrick and Radhia Cousot.

Thursday, 11 August 2011

18:00–19:00 Mikhail Belyaev: Static Program Analysis Using Type and Effect Systems (slides: download or view online)

Abstract

Automatic software defect detection is a vital way of improving the overall reliability of computer programs. Analyzing programs in languages like C is especially important as these languages are often used to write critical software. Type and effect systems are a promising approach to static analysis of programs, including, but not limited to, software defect detection. This approach is widely described in theory but lacks practical use. The first part of this talk includes a survey on this approach including its basic principles, notation and properties. It also provides an overview of some existing applications of type and effect systems for different purposes. The second part introduces a tool for static analysis based on LLVM compiler infrastructure and its SSA code model. This tool uses type and effect systems to detect software defects in C programs through type inference with an extensive use of an external SMT solver.

19:00–20:00 Sergey Velder: Floyd verification technique

Abstract

In 1960s, several methods of formal verification were discovered, such as Floyd method of inductive assertions, Hoare reasoning, Dijkstra method of weakest preconditions and McCarthy's recursive induction. This talk describes the first of them, Floyd method. This is the most general verification technique, intended for programs represented in common form by block diagrams. Floyd method includes such stages as inductive assertions construction, well-founded sets construction and inverse substisutions. Each of these stages will be described in the talk.

Thursday, 21 July 2011

18:00–19:00 Andrey Tikhomirov: Techniques for proving programs with pointers (seraration logic, shape analysis) (slides: download, view online or view online in a different way)

Abstract

This will be survey talk about techniques for proving programs with pointers. I will describe several methods: separation logic and shape analysis.

19:00–20:00 Anton Bannykh: Survey of Satisfiability Modulo Theories (SMT) problem (slides: download, view online or view online in a different way)

Abstract

SMT solvers check satisfiability of first-order formulas with respect to some theories of interest. SMT solvers proved to be efficient and are widely used in software and hardware verification, scheduling, model checking etc.

Thursday, 14 July 2011

17:00–18:00 Ben Livshits, Microsoft Research: Finding Malware on a Web Scale with Static and Runtime Analysis

Abstract

Over the last several years, JavaScript malware has emerged as one of the most popular ways to deliver drive-by attacks to unsuspecting users through the browser. This talk covers recent Microsoft Research experiences with finding malware on the web. It highlights two tools: Nozzle and Zozzle. Nozzle is a runtime malware detector that focuses on finding heap spraying attacks. Zozzle is a mostly static detector that finds heap sprays and other types of JavaScript malware. Both are extremely precise: Nozzle false positive rate is close to one in a billion; Zozzle's is about one in a million.
Both are deployed by Bing and are used daily to find thousands of malicious web sites. This talk will focus on interesting interplay between static and runtime analysis and cover what it takes to migrate research ideas into real-world products.

18:00–19:00 Mikhail Moiseev, SPBGPU: Static analysis for error detection in multithreaded programs (Russian)

Abstract

Static error detection in multithreaded programs with good-enough efficiency characteristics is a hard challenge. Instead of sequential programs there are thread interleaving which leads to growth number of program states. The other problem in multithreaded program analysis is synchronization errors — special errors such as deadlock, race condition, livelock and others. So use of well-known static analysis algorithms, which obtain good results for single-threaded programs, is not efficient for multithreaded programs.
In this seminar a survey of existing static analysis approaches and the most interesting algorithms for multithreaded programs will be done. After that I will present a static analysis method, which allows extracting necessary information for detection of most widespread errors types in C/C++ multithreaded programs including some synchronization errors. This method based on lockset analysis algorithm, which considers may-happen-in-parallel relations between program statements. I will take lots of examples which illustrate error detection problems and possible solutions. In the end of the seminar some experimental results and efficiency characteristics of the method will be discussed.

Friday, 8 July 2011

16:30–17:30 Bertrand Meyer: The Calculus of Object Structures

Abstract

Verifying properties of object-oriented software requires a method for handling references in a simple and intuitive way, closely related to how O-O programmers reason about their programs. The method presented here involves four components: compositional logic, a framework for describing program semantics and proving program properties; negative variables to address the specifics of O-O programming, in particular the notion of qualified call; the alias calculus, which determines whether reference expressions can ever have the same value; and the calculus of object structures, a specification technique for describing properties of the structures that arise during the execution of an object-oriented program.
The talk illustrates the method by providing a proof of the standard algorithm for reversing a linked list.

17:30–18:30 Anton Akhi: Survey of tools for automatic program correction (slides: download, view online or view online in a different way)

Abstract

It will be shown that automatic bug fixing is not a magic, but an interesting task to be solved. I will describe several ways to automatically fix bugs in programs. The methods are based on Genetic Programming, Contract usage, Machine learning etc.

Thursday, 7 July 2011

19:00–21:00 Bertrand Meyer: Concurrent Programming Is Easy!

Abstract

I will describe the current state of the SCOOP model for simple and safe concurrency. SCOOP has been implemented as part of EiffelStudio 6.8 (released in May) and is a comprehensive approach to concurrent programming, emphasizing simplicity and compatibility with standard, sequential models of programming. In other words, while many people state that programming concurrent applications requires a complete change of methods, SCOOP builds on well-known techniques of object-oriented programming and extends them minimally to cover concurrency, with the aim of avoiding the common difficulties and errors that plague concurrent programs; in particular, data races are not possible in SCOOP.

Thursday, 16 June 2011

10:00–12:00 Vladimir Itsykson: Static analysis techniques (slides: download or view online)

12:00–14:00 Bertrand Meyer: The alias calculus (slides: download, view online or view online in a different way)

Abstract

One of the key obstacles to proving modern programs correct is to determine whether two references can ever become attached during execution to the same object; this question lies in particular at the heart of the "frame problem". I will present a theory, calculus ("alias calculus"), graphical notation ("alias diagrams") for computing aliasing automatically, and demonstrate its implementation.
See the paper at http://se.ethz.ch/~meyer/publications/aliasing/alias-revised.pdf.

Tuesday, 7 June 2011

10:00–12:00 Bertrand Meyer: Survey of ETH research in verification

13:30–16:30 Bertrand Meyer: Survey of ETH research in verification (continued)

Monday, 6 June 2011

10:00–12:00 Sergey Velder: Survey of Model Checking

Abstract

This will be survey talk and the current state of the art in Model Checking.

13:30–16:30 Bertrand Meyer: Survey of Design by Contract techniques (slides: download or view online)

Abstract

This will not be a research talk but a tutorial on Design by Contract and the current state of the art.