Entries tagged with rise - Channel 9

C9 Conversations: Yuri Gurevich On Imperative, Abstraction, Algorithms and Logic

Charles — Tue, 09 Feb 2010 20:10:00 GMT

Welcome to the latest installment of C9 Conversations. For this episode, we were very fortunate to get a chance to converse openly with one of the world’s preeminent mathematical logicians, the great Yuri Gurevich.

Dr. Gurevich is Professor Emeritus of Electrical Engineering and Computer Science at the University of Michigan. He is currently a principle research scientist in Wolfram Schulte’s RiSE team (Research in Software Engineering group at Microsoft Research).

Originally, Dr. Gurevich started his career as an algebraist. Later he became a logician. Then he moved to computer science, where his main projects have been Abstract State Machines, Average Case Computational Complexity, and Finite Model Theory. Dr. Gurevich has been honored as a Dr. Honoris Causa of the University of Limburg, Belgium (1998), as a Fellow of the Association for Computing Machinery (1996), as well as a Fellow of the John Simon Guggenheim Memorial Foundation (1995).

Dr. Gurevich's fundamental work on the theory of Abstract State Machines (ASMs) is of paramount importance for theoretical and applied computer science. The significance of the theoretical concepts developed by Gurevich is confirmed by the substantial impact they have on mathematical modeling of discrete dynamic systems.

*This is probably the only interview in C9's history where a good case is made for imperative programming versus declarative and functional (this starts right off the bat at around 02:31).

Tune in. Meet Yuri Gurevich.

Francesco Logozzo: Programmazione per Contratti e runtime checking in .NET con i CodeContracts

Peli de Halleux — Sat, 06 Feb 2010 00:09:00 GMT

Francesco Logozzo, ricercatore nel gruppo di ingegneria del software (RiSE) a Microsoft Research, offre una breve introduzione alla programmazione per contratti ed al progetto CodeContracts per .NET .

I CodeContracts permettono di specificare il comportamento del codice utilizzando il codice stesso.

Francesco ci spieghera’ (alla lavagna e con un demo di ispirazione ciclistica) come migliorare la qualita’ del codice e rendere il debugging piu’ efficace usando la libreria dei Contratti (inclusa in mscorlib 4.0) ed il runtime checker .

I CodeContracts possono essere scaricati con licenza industriale o accademica:

Il gruppo RiSE coordina la ricerca in ingegneria del software a Redmond negli USA.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Pex - Unit Testing of SharePoint Services that Rocks!

Matthijs Hoekstra — Sun, 31 Jan 2010 10:33:00 GMT

SharePoint Services are challenging for unit testing because it is not possible to execute the SharePoint Service without being connected to a live SharePoint site. For that reason, most of the unit tests written for SharePoint are actually integration tests as they need a live system to run. In this session, we show how to use Pex, an automated test generation tool for .NET, to test SharePoint Services in isolation. From a parameterized unit test, Pex generates a suite of closed unit tests with high code coverage. Pex also contains a stubbing framework, Moles, that allows to detour any .NET method to user-defined delegates, e.g., replace any call to the SharePoint Object Model by a user-defined delegate.

Peli de Halleux from Microsoft Research presented this presentation on SharePoint Connections 2010 Amsterdam.

Peli is a Senior Research Software Design Engineer at Microsoft Research in Redmond, USA, where he has been since October 2006 working the Pex project. From 2004 to 2006, he worked in the Common Language Runtime (CLR) as a Software Design Engineer in Test (SDE/T) in charge of the Just In Time compiler. Before joining Microsoft, he earned a PhD in Applied Mathematics from the Catholic University of Louvain. Earlier, he developed the unit testing framework MbUnit.

Nikolai Tillmann: Moles - Replace any .NET method with a delegate

Peli de Halleux — Fri, 29 Jan 2010 21:00:00 GMT

Nikolai Tillman, a member of the RiSE group at Microsoft Research, gives a short demo of Moles, a new framework that allows replacing any .NET method with a delegate. In the context of unit testing, one can use Moles to isolate from environment dependencies (such as time, file system, database, etc...) even when those dependencies are hard-coded through static method or sealed types. In this demo, Nikolai goes through the famous Y2K bug and how to test it...

Moles tutorial (pdf)

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

The Verification Corner: Loop Invariants

Peli de Halleux — Tue, 12 Jan 2010 08:03:00 GMT

In this episode of The Verification Corner, Rustan Leino talks about Loop Invariants. He gives a brief summary of the theoretical foundations and shows how a program can sometimes be systematically constructed from its specifications. Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research.

Whiteboard slides [.pdf] [.pptx]
Spec# Demo project [.zip]
Find past and future episodes of the The Verification Corner!

The Verification Corner is a show on Software Verification Techniques and Tools. The show is produced by the Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Nikolaj Bjørner and Leonardo de Moura: The Z3 Constraint Solver

Peli de Halleux — Thu, 31 Dec 2009 19:00:00 GMT

Nikolaj Bjørner and Leonardo de Moura are Researchers in the Research in Software Engineering (RiSE) team at Microsoft Research. They are talking and demoing Z3, a high-performance SMT constraint solver. Solving constraint systems is the root of of many software analysis techniques so it is not surprising to see Z3 powering many tools developed at Microsoft: Spec#/Boogie, Pex, SLAM, SAGE, FORMULA, HAVOC and more.

In this video, you'll get a 10000 feet overview of Z3 and constraint solving in general with a demo on how to use the C# API. For more details, you will find many articles that should keep you busy for a while.

Z3 home page

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Francesco Logozzo - Static Checking with Code Contracts for .NET

Peli de Halleux — Tue, 22 Dec 2009 19:47:00 GMT

Francesco Logozzo, a researcher at the Research in Software Engineering (RiSE) group at Microsoft Research, gives a demo of the Static Checker that comes with Code Contracts for .NET tools. The static checker allows you to verify that all the assertions in your code hold without actually running the code!

Francesco also goes to the whiteboard and gives us a short tutorial on Abstract Interpretation, the technique used by the static checker to prove the assertions.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Manuel Fahndrich et Peli de Halleux - Code Contracts et Pex pour .NET

Peli de Halleux — Fri, 18 Dec 2009 04:12:00 GMT

Manuel Fähndrich et Peli de Halleux, deux membres du groupe RiSE à Microsoft Research, nous font une petite demo de Code Contracts et Pex. Les Code Contracts peuvent être utilise pour specifier les pré-conditions et post-conditions de methodes. Ils peuvent aussi être compilé en assertions a l'exécution. Pex peut dès lors analyser et tenter de trouver des contres examples pour les invalider. Ceci est notre première video en francais, donc attendez-vous à avoir quelques termes anglais dans la conversation...

Les outils peuvent etre téléchargé des sites suivants:

Original video in English
Code Contracts: http://research.microsoft.com/contracts
Pex: http://research.microsoft.com/pex

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Jeffrey Van Gogh: Testing Rx with Pex

Peli de Halleux — Tue, 15 Dec 2009 15:16:00 GMT

Ever wonder how the Reactive Extensions get tested? Jeffrey Van Gogh gives a glimpse at how they do it. The Rx developers have been using Pex and writing parameterized unit tests. In this video, we look at Enumerable.Zip and how we can use Pex to help testing it.

Jeffrey also explains how they use Pex in their build process to regenerate the entire unit test suite on each build!

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Juan Chen and Nikhil Swamy: FINE, Functional Programming for End-to-End Security Verification

Peli de Halleux — Thu, 10 Dec 2009 19:12:00 GMT

Juan Chen and Nikhil Swamy, two researchers at the Research in Software Engineering group, present FINE, a new programming language for .NET.

Software systems are governed by increasingly complex security policies. Ensuring that a system properly enforces its policy is hard. FINE is a new programming language (similar to F#) whose type system can be used to check that rich, stateful authorization and information flow policies are properly enforced. FINE is compiled to DCIL, a new minimal extension of .NET CIL. Our compiler carries type information throughout and allows DCIL programs to be verified independently for security.

In this video, Juan an Nikhil give the big picture and a shiny demo of FINE.

FINE home page
Read the article about FINE

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

MSDN Flash Podcast 013 – Code Contracts at TechEd Europe

Eric Nelson — Tue, 01 Dec 2009 13:43:00 GMT

While at TechEd Europe in November 2009 I had a chance to catch up with the two lead developers of the Pex team Peli de Halleux and Nikolai Tillmann to talk about Code Contracts.

Code Contracts contains a common library (System.Diagnostics.Contracts) for expressing pre-conditions, post-conditions and invariants which any tool writer can take advantage of. A number of tools are available on devlabs including a documentation extracter and a static analysis tool. Code Contracts works with .Net 4 and .Net 2.

Hear why Code Contracts is a better way of implementing assertions including enabling the conditons to be specified against interfaces - sweet!

MSDN Flash Podcast 012 – Pex automated testing at TechEd Europe

Eric Nelson — Tue, 01 Dec 2009 13:35:00 GMT

While at TechEd Europe in November 2009 I had a chance to catch up with the two lead developers of the Pex team Peli de Halleux and Nikolai Tillmann.

Pex enables white box testing. It looks at your code, finds all the branches and determines which inputs will result in those branches being executed. Pex attempts to exercise every reachable statement in your code.

It works with Visual Studio 2008 and Visual Studio 2010 Beta 2 and is restricted to .NET programs. It is available on devlabs.

One of the features we discuss is Moles. Moles allows you to
isolate tests from the environment - to replace any .NET method with your own delegate. This makes it easy to test code which has hard dependencies on databases, web services etc.

I also did a short blog post outlining the stubs and moles capabilitie of Pex.

Pex is an incubation project - hence feedback from developers is hugely important.

Enjoy.

SpecExplorer: Model-Based Testing made practicable

Peli de Halleux — Tue, 27 Oct 2009 04:45:00 GMT

Keith Stobie, Wolfgang Grieskamp, and Nico Kicillof gave a presentation on the new version of Spec Explorer 2010 for Visual Studio. Spec Explorer is a visual tool for modeling software behavior and generating test suites from those models. Spec Explorer’s approach to model-based testing has been shown to greatly enhance productivity of test case creation, to ensure predictability of requirement coverage, and to support lifecycle management and software updates. Models are typically written in C# and controlled by a configuration language which allows to express scenarios and test purposes. Microsoft itself chose Spec Explorer as a cornerstone of the effort to validate open protocol documentation, developing more than 200 test suites validating over 40,000 requirements for networking protocols in a production environment.

Emre Kiciman and Ben Livshits - Doloto: Download Time Optimizer for Web 2.0 Apps

Peli de Halleux — Mon, 05 Oct 2009 22:33:00 GMT

Emre Kiciman and Ben Livshits present the ideas behind Doloto. Doloto is an AJAX application optimization tool, especially useful for large and complex Web 2.0 applications that contain a lot of code, such as Bing Maps, Hotmail, etc. Doloto analyzes AJAX application workloads and automatically performs code splitting of existing large Web 2.0 applications.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Daryl Zuniga - Viewing Code Contracts.NET in Visual Studio

Peli de Halleux — Mon, 21 Sep 2009 22:59:00 GMT

Daryl Zuniga gives a fast and furious demo of the new editor extensions for Code Contracts.NET. When a developer overrides a method with Contracts, the rewritter would automatically insert the pre-conditions and post-conditions in the method body. Unfortunately, the editor is not aware of that - leaving the developer confused... Not anymore, Daryl's extension mines the Contracts on the fly and hosts them in the shiny new WPF editor of Visual Studio 2010.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Trishul Chilimbi - Green - Energy Efficient Software

Peli de Halleux — Tue, 15 Sep 2009 20:17:00 GMT

Trishul Chilimbi, a researcher from RiSE talks about Green. Green enables programmers to approximate expensive functions and loops while providing statistical quality of service guarantees. By giving away a couple percents of QoS, some applications may decrease their energy consumption by as much as 20%. Watch this video to learn all the details about Green...

Green Technical Report
Green story on Microsoft Research

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Daryl Zuniga and Mike Barnett - Xml Documentation from Code Contracts for .Net

Peli de Halleux — Mon, 10 Aug 2009 22:55:00 GMT

Mike Barnett and Daryl Zuniga, a high school intern at RiSE, sit down to talk about Code Contracts for .NET and documentation. Daryl has been working this summer on a tool that inserts contracts elements into the Xml Documentation files generated by the C#/VB compiler. Daryl also updated the Sandcastle stylesheets so that the contracts appear in the documentation pages.

Code Contracts for .NET home page - forums
See more Channel 9 videos on Code Contracts

Update: the xml comment generation is now available for download!

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Ethan Jackson - BAM - Cloud Computing with Models

Peli de Halleux — Mon, 03 Aug 2009 22:11:00 GMT

A (very) short video with Ethan Jackson on BAM. BAM is a new approach to developing cloud applications through modeling, code synthesis, and simulation. With BAM you design applications that work in a dynamic environment with fluctuating resources. You can also check out a previous Channel9 video for more details about how things work.

BAM home page: http://research.microsoft.com/en-us/um/people/ejackson/bam.aspx

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Patrice Godefroid - Automated Whitebox Fuzz Testing with SAGE

Peli de Halleux — Tue, 14 Jul 2009 18:29:00 GMT

Patrice Godefroid gives an overview of Automated Whitebox Fuzz Testing, a powerful testing technique applied at Microsoft through a tool called SAGE. Listen how he is working with the SAGE team to 'eradicate all buffer overrun bugs' in Windows...

Read more in this paper or this slide deck.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Architecture Behind CAT.NET

Jossie Tirado — Mon, 29 Jun 2009 22:24:00 GMT

Ben Livshits, from Microsoft Research, talks about the architecture behind CAT.NET, which is a static analysis tool on Visual Studio that helps find vulnerabilities like SQL Injection, CSRF, XSS among others, within managed code.

Ben’s knowledge on static and dynamic dataflow analysis made him a key contributor on the creation of CAT.NET. He walks us through different examples of how the data analysis happens depending on complexity and explains how precision varies.

Learn more about Microsoft Information Security Tools.

www.msinfosec.com

Ben Livshits and Emre Kiciman - AjaxView, Performance Profiling of AJAX web sites

Peli de Halleux — Mon, 22 Jun 2009 18:34:00 GMT

Ben Livshits and Emre Kiciman talk about the Ajax Profiling Extensions (also known as AjaxView), a tool that allows to profile web sites using Ajax. The tool lets you investigate the performance of the client side javascript! Ben and Emre explain how the profiling works, i.e. how they instrument the javascript on the fly, collect execution traces, and so forth. They also show a really cool demo of the tool where they turn on profiling for a couple web pages, then analyze the performance directly in Visual Studio.

Ajax Profiling Extensions @msdn: http://code.msdn.microsoft.com/AjaxView
AjaxView @MSR: http://research.microsoft.com/en-us/projects/ajaxview/

(We have a new jingle for the RiSE videos thanks the musical talent of Tom Ball. The full track of "San Juan Strut" can be found at www.themiddlethird.org)

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Sebastian Burckhardt - Data Race Detection with CHESS

Peli de Halleux — Fri, 12 Jun 2009 18:31:00 GMT

Sebastian Burckhardt gives a short tutorial of some of the new features of CHESS: data race detection and ChessBoard. CHESS is a concurrency testing tool takes a concurrent unit test and executes it with different thread schedules. Sebastian explains us how CHESS can detect data races, a very subtle kind of concurrency bug. You'll also learn how to drill into concurrency issues using the ChessBoard, a little application designed to drill and investigate concurrent tests.

CHESS home page: http://research.microsoft.com/en-us/projects/chess/
CHESS forums: http://social.msdn.microsoft.com/Forums/en-us/chess/threads/

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Margus Veanes and Pavel Grigorenko - Qex - Symbolic SQL Query Exploration

Peli de Halleux — Tue, 02 Jun 2009 23:59:00 GMT

Margus Veanes and Pavel Grigorenko present a new exciting project: Qex. Pavel did an internship in the Research in Software Engineering team (RiSE) investigating automatic data generation methods for parameterized SQL queries. In this video, he shows the result of his 3-month work. Qex translates SQL queries to logic formulas and give to our in-house constraint solver, Z3. When Z3 finds a solution, Qex translates that solution back to SQL code that can be executed in the database. This is similar to how Pex works.

Find more about Qex at http://research.microsoft.com/qex or read the technical report.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

RiSE at the International Conference on Software Engineering

Wolfram Schulte — Thu, 14 May 2009 19:07:00 GMT

Many researchers from the Research in Software Engineering team (RiSE) will be attending the 31st International Conference on Software Engineering in Vancouver (ICSE'09). Here is what RiSE is presenting this year:

Does Distributed Development Affect Software Quality? An Empirical Case Study of Windows Vista (ICSE: Research paper). Christian Bird, Nachiappan Nagappan, Premkumar Devanbu, Harald Gall, Brendan Murphy Winner of ACM SIGSOFT Distinguished Papers Award. By studying the development of Windows Vista we evaluate whether distributed software development is more challenging than collocated development.
Do Crosscutting Concerns Cause Defects? (ICSE: TSE/TOSEM Session), Marc Eaddy, Thomas Zimmermann, Kaitlin D. Sherwood, Vibhav Garg, Gail C. Murphy, Nachiappan Nagappan, Alfred V. Aho. TSE/TOSEM Session. We asked the question, “How much does the amount that a concern is crosscutting affect the number of defects in a program?” and conducted three extensive case studies to help answer this question. All three studies revealed a moderate to strong statistically significant correlation between the degree of scattering and the number of defects.
Predicting Defects in SAP Java Code: An Experience Report (ICSE: Software Engineering in Practice papers), Thomas Zimmermann, Tilman Holschuh, Markus Päuser, Kim Herzig, Rahul Premraj, Andreas Zeller. In a study on a large SAP Java system, we evaluated and compared a number of defect predictors, based on code features such as complexity metrics, static error detectors, change frequency, or component imports.
HOLMES: Effective Statistical Debugging via Efficient Path Profiling (ICSE: Research papers), Trishul Chilimbi, Ben Liblit, Krishna Mehra, Aditya Nori, Kapil Vaswani. We describe a statistical debugging tool called HOLMES that efficiently isolates bugs by finding paths that correlate with failure.
The Secret Life of Bugs: Going Past the Errors and Omissions in Software Repositories (ICSE: Research Paper), Jorge Aranda, Gina Venolia. Every bug has a story behind it. This paper uses rich bug histories and survey results to identify common bug fixing coordination patterns and to provide implications for tool designers and researchers of coordination in software development
Guided Path Exploration for Regression Test Generation (ICSE: NIER Track).Kunal Taneja, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Wolfram Schulte. Given two versions of the same software, the approach described in this paper can automatically generate a test suite that exercises only those program behaviors which are different. A prototype has been implemented as an extension to Pex.
Improving Bug Tracking Systems (ICSE: NIER Track), Thomas Zimmermann, Rahul Premraj, Jonathan Sillito, Silvia Breu. We present a prototype of an interactive bug tracking system that gathers relevant information from users and automatically identifies files that need to be fixed to resolve a bug.
Codebook: Social Networking over Code (ICSE: NIER Track). Andrew Begel and Robert DeLine. Codebook is a social networking service that connects software developers through the work artifacts that they share -- code, bugs, tests, specifications, etc -- to enable them to keep track of task dependencies, maintain connections to other teams, and understand the history and rationale behind the code they use.
Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract (ICSE: Demos). M. Barnett, M. Fahndrich, P. de Halleux, F. Logozzo, N. Tillman. Pex, a unit-test generator, and Code Contracts, a design-by-contract system, provide even more benefits when used together for developing high-quality robust programs.
VCC: Contract-based Modular Verification of Concurrent C (ICSE: Demos). Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte. 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 is currently used to verify the core of Microsoft Hyper-V, consisting of 50,000 lines of system-level C code.
Deconstructing Concurrency Heisenbugs (ICSE Demo). Thomas Ball, Sebastian Burckhardt, Madan Musuvathi, Shaz Qadeer. CHESS is a tool for finding and reproducing "Heisenbugs", which result from unexpected interference among threads. CHESS has been integrated into the test frameworks of many code bases inside Microsoft and is used by testers on a daily basis.
An Empirical Study of Testing File-System-Dependent Software With Mock Objects (AST Workshop)
Madhuri Marri, Tao Xie, Nikolai Tillmann, Jonathan de Halleux and Wolfram Schulte. A case study on how to use parameterized mock objects in unit testing in combination with the test input generation tool Pex.
A Brief History of Software - from Bell Labs to Microsoft Research (MSR workshop, keynote)

Tom will report on the power of combining statistical expertise with software engineering expertise to address pressing problems of software production in a statistically valid manner. He will trace the history from early work at AT&T to present work at Microsoft.
Making CHASE Mainstream (CHASE Workshop keynote), Rob DeLine. Rob will discuss why “people issues” have not gotten enough attention among software engineering researchers and suggests ways to make research in this area more mainstream.
Coordination in Large-Scale Software Teams (CHASE Workshop). Andrew Begel, Nachiappan Nagappan, Christopher Poile, and Lucas Layman. A survey of Microsoft engineers shows that coordination between large-scale software teams is very challenging, but can be eased with better communication and tools tailored towards each engineer’s role in the collaboration.

The Design of a Task Parallel Library (Working Group Software Engineering for parallel Systems, keynote), Wolfram Schulte. Wolfram discusses the design and implementation of the TPL, which makes it easy to exploit potential parallelism in a .NET program.
Parameterized Unit Testing (Tutorial): Principles, Techniques, and Applications in Practice.
Nikolai Tillmann, Jonathan de Halleux, Tao Xie, and Wolfram Schulte. A hands-on introduction to parameterized unit testing: how it relates to unit testing, how to leverage automated tools, what good test patterns are, and how it can be used in practice.

Cheers, Wolfram Schulte.

Manuel Fahndrich and Peli de Halleux - The Synergy of Code Contracts and Pex

Peli de Halleux — Thu, 23 Apr 2009 18:59:00 GMT

Manuel Fähndrich and Peli de Halleux sit down for a quick coding session that shows how to use Code Contracts and Pex together. Code Contracts can be used to specify what your code should do, they get turned into runtime checks which Pex can analyse and try to find counter-examples for. This was a fun session with Manuel and really shows the synergy of the two tools/approaches.

Both tools can be downloaded from Devlabs or our academic project pages.

Code Contracts: http://research.microsoft.com/contracts
Pex: http://research.microsoft.com/pex
See this video in French!

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.