Microsoft Research & Institute for System Programming RAS
Joint Workshop, Moscow, 19-20 June, 2009
Location: Room 110, Solzhenitsina str. 25, Moscow
June 19th, Friday10:00-12:00 / Morning session I
Opening - Welcome note by Victor Ivannikov (ISPRAS), Rostislav Yavorskiy (Microsoft Research)
Wolfram Schulte (Microsoft Research), Automating Software Testing Using Program Analysis
Alexander Petrenko (ISPRAS), UniTESK branches and applications
Coffee break
12:00-13:30 / Morning session II
Wolfram Schulte (MSR), The Power of Rich Syntax for Model-based Development
Igor Konnov (MSU), CheAPS: Parameterized Model Checking Tool
13:30-14:30 / Lunch
14:30-16:30 / Afternoon session I
Wolfram Schulte (MSR), VCC: Contract-based Modular Verification of Concurrent C
Nikita Nalyutin (MEPhI), Software engineering, software verification and configuration management activities at MEPhI
Coffee break
16:30-18:00 / Afternoon session II
Eugene Shatokhin, Denis Silakov (ISPRAS), LSB Infrastructure Project
Elena Popova (MEPhI), The Formal Approach to Computer Game Rule Development Automation
Dmitry Ermolov (Yandex), Sudoku solver based on Z3 prover
June 20th, Satyrday
10:00-12:00 / Morning session I
Wolfram Schulte (MSR), Program Analysis 2.0
Nikolay Pakulin (ISPRAS), Telecommunication protocols testing
Coffee break
12:00-13:30 / Morning session II
Wolfram Schulte (MSR), Experimental software engineering
Alexander Kamkin (ISPRAS), Hardware designs testing based on contract specification
Closing
ABSTRACTS
Speaker: Wolfram Schulte, Microsoft Research
Title: Automating Software Testing Using Program Analysis
During the last ten years, code inspection for standard programming errors has largely been automated with static code analysis. During the next ten years, we believe we will see similar progress in automating testing, and specifically test generation, thanks to advances in program analysis, efficient constraint solvers and powerful computers. We present an overview of two related projects currently under way at Microsoft in greater detail: Sage for Security Testing of unmanaged code and PEX for unit testing of managed code.
Speaker: Alexander K.Petrenko, ISPRAS
Title: UniTESK branches and applications
UniTESK technology emerged in 1999. It is based on the idea of test generation from pre- and postconditions. During the recent 10 years UniTESK team developed a number of verification techniques and a suite of tools based on the UniTESK technology, and applied the tools and techniques to different kinds of software and hardware designs. The talk will present a common picture of UniTESK features and application domains.
Speaker: Wolfram Schulte, Microsoft Research
Title: The Power of Rich Syntax for Model-based Development
Abstract: During the last century, many general purpose programming languages have been developed, all having rigid syntax and often von-Neuman specific semantics. With the rise of model-based development this changes: We believe that in this century we will see many more domain specific languages. These languages use rich and custom syntaxes to capture domain specific abstractions, refinement mappings, and design spaces. In this talk we show how a formalization of rich syntax can be used to compose abstractions, validate refinement maps, and construct design spaces. We compute these properties on several concrete examples using our tool Formula, which uses a variant of Horn logic to represent and analyze rich syntax.
Speaker: Igor Konnov, Moscow State University
Title: CheAPS: Parameterized Model Checking Tool
Parameterized Model Checking Problem is an extension of Model Checking aimed to reason about infinite families of finite models comprised of n homogenous processes. Several approaches to PMC have been developed since mid-eighties, among them: invariant-based techniques, abstraction techniques, symmetry reduction techniques, and symbolic techniques. Checker of Asynchronous Parameterized Systems (CheAPS) exploits the technique of network invariants. The key points in CheAPS are the checking of invariance property with respect to semiblock simulation and the verification of temporal properties on the invariants found. The latter is performed by the Spin Model Checker thanks to the fact that processes are described in Promela language. The former is the central piece of the tool. Various heuristics were developed in order to speed up the checking of invariance property. Several parameterized models have been checked with the help of CheAPS.
Speaker: Wolfram Schulte, Microsoft Research
Title: VCC: Contract-based Modular Verification of Concurrent C
Most system level software is written in C and executed concurrently. Because such software is often critical for system reliability, it is an ideal target for formal verification. Annotated C and the Verified C Compiler (VCC) form the first modular sound verification methodology for concurrent C that scales to real-world production code. VCC's verification methodology rests on two-state invariants that span multiple objects without sacrificing thread- or data-modularity. To capture knowledge about the system state VCC introduces claims, which are derived first-class objects.
VCC is integrated in Microsoft Visual Studio and it comes with support for verification debugging: an explorer for counterexamples of failed proofs helps to find errors in code or specifications, and a prover log analyzer helps debugging proof attempts that exhaust available resources (memory, time). VCC is currently used to verify the core of Microsoft Hyper-V, consisting of 50,000 lines of system-level C code.
Speaker: Nikita Nalyutin, Moscow Engineering and Physics Institute (National Nuclear Research University)
Title: Software engineering, software verification and configuration management activities at MEPhI
During last 30 years Cybernetics department of Moscow Engineering and Physics Institute accumulated a significant experience in systematic verification of software systems. These activities were heavily influenced by the verification for aviation industry, with its standards, establishing complex and thorough requirements for all development processes. We present a general overview of Cybernetics department activities in software engineering, our approach to teaching software verification. Also we present an overview of project CoSC, currently underway at Cybernetics department, which primary goal is to enforce common configuration management process with a set of formal methods for configuration status calculation.
Speakers: Eugene A. Shatokhin, Denis V. Silakov, ISPRAS
Title: LSB Infrastructure - tools and technologies to support development, usage and maintenance of the Linux Standard Base.
Outlined in this report are the main components of the LSB Infrastructure system - the integrated set of tools that support development, usage and maintenance of the Linux Standard Base. Some of these tools provide convenient means to access the LSB Specification. Other components (test suites, Distribution Testkit Manager, Application Checker, etc.) allow to check a given Linux distribution or an application for LSB compliance, help to analyze the results and partially automate the process of LSB certification. Some of the technologies employed to develop the test suites mentioned above are also briefly discussed.
Speaker: Wolfram Schulte, Microsoft Research
Title: Program Analysis 2.0
Microsoft Research's efforts in program analysis began with detecting defects in C and C++ programs with tools such as ESP, PREfast, PREfix, and SLAM, all of which have been widely deployed internally. The PREfast and SLAM technologies also were incorporated into shipping Microsoft products (Visual Studio and the Driver Development Kit, respectively).
In the last few years, we have been working on program analysis tools for .NET, focusing on: (1) code contracts and verifying code against contracts; (2) automatic test generation; (3) checking for concurrency defects. These tools are based on advances in abstract interpretation over linear inequalities, symbolic execution of object-oriented programs, efficient and precise automatic theorem proving, and direct model checking of concurrent systems. All of the above tools are available for both academic and commercial use, in partnership with Visual Studio.
Speaker: Nikolay Pakulin, ISPRAS
Title: Testing of Telecommunication Protocols
Well-known techniques of automated test elicitation from state machines work fine for small, simple protocols. Unfortunately they experience state explosion when applied to complex modern telecommunication protocols. The industrial approach, based on manual development of test cases, requires significant effort and can hardly guarantee proper coverage of requirements or protocol specification. The talk presents UniTESK-based approach to telecom testing, that combines both efficient test generation with rigorous behavior specification.
Speaker: Alexander Kamkin, ISPRAS
Title: Using Cycle-Accurate Contract Specifications for Testing Hardware Models.
Contract specifications in the form of pre- and post-conditions are widely used in software engineering for development and functional testing of software systems. The talk considers some other application of contract specifications, testing of hardware models (more specifically, models of synchronous hardware developed in such languages as Verilog and VHDL). A formal approach to specification and testing of such models is introduced. The suggested approach is based on pre- and post-conditions of one-cycle microoperations; it takes into account concurrency (operation overlapping), pipeline interlocks, and other particular features of hardware designs. The approach has been applied to several units of MIPS64-compatible microprocessor. The talk comprises a brief description of the experience.
5