Archives for posts with tag: rise
« Older Entries

Code Contracts and Pex: Power Charge Your Assertions and Unit Tests

May 28, 10 //
Comments Off

By Nikolai Tillmann and  Mike Barnett

Learn how Code Contracts provides a set of tools for design-by-contract programming and how Pex is an advanced unit-testing tool that uses automated program exploration to intelligently create unit tests with high code coverage. 
See how they work together so that your code has fewer defects.

Learn about new features for Code Contracts including automatic documentation generation, call-site checking for components and reference assemblies for the .NET Framework and for Pex including a light-weight mocking framework, improved support for large code bases, and more thorough test input generation.

Links:
PEX // Code Contracts // Mike Barnett // Nikolai Tillmann // MDCC // DPE DK

Inside SPUR – A Trace-Based JIT Compiler for CIL

April 15, 10 //
Comments Off

Computer Scientists and MSR Researchers Wolfram Schulte, Herman Venter, Nikolai Tillmann, and Manuel Fahndrich join Erik Meijer for an Expert to Expert deep dive into the theory and implementation strategies inside of SPUR, a research Tracing Just-In-Time (TJIT) compiler for Microsoft’s Common Intermediate Language CIL (the target language of C#, VB.NET, F#, and many other .NET languages).  

Tracing just-in-time compilers (TJITs) determine frequently executed traces (hot paths and loops) in running programs and focus their optimization effort by emitting optimized machine code specialized to these traces. Prior work has established this strategy to be especially beneficial for dynamic languages such as JavaScript, where the TJIT interfaces with the interpreter and produces machine code from the JavaScript trace. 

In order to validate that the performance gains of a TJIT for interpreted languages like JavaScript do not depend on specific idioms of the language, the SPUR team produces a performance evaluation of a JavaScript runtime that translates JavaScript to CIL and then runs on top of SPUR.

Read the SPUR research paper.

Margus Veanes – Rex – Symbolic Regular Expression Exploration

April 15, 10 //
Comments Off

Margus Veanes, a Researcher from the RiSE group at Microsoft Research, gives an overview of Rex, a tool that generates matching string from .NET regular expressions. Rex turns regular expressions into symbolic automatons, then gives them to a constraint solver to find matching strings.

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

The Verification Corner – Loop Termination

March 29, 10 //
Comments Off

In this episode of The Verification Corner, Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, shows how to prove loop termination. During his demonstration, Rustan presents the theoretical background information necessary to build the proof before modeling it using the Dafny language.

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

E2E: JavaScript Performance, Project JSMeter and Web Programming

March 29, 10 //
Comments Off

JavaScript is the most widely used programming language on the web. As the great Douglas Crockford likes to say, JavaScript is both the world’s most popular programming language and the world’s least popular programming language at the same time.

In this episode of Expert to Expert (to Expert), Erik Meijer joins MSR research scientists Ben Livshits and Ben Zorn to talk about JavaScript, project JSMeter and today’s trends in web programming.

Dr. Zorn and Dr. Livshits have been doing a significant amount of research on how JavaScript is used in the real world by analyzing JS execution on large-scale (JS-heavy) commercial web sites. Their formal exploration of JS executing in the real world, Project JSMeter, has yielded results, which seem to indicate that current JS performance test suites are at best suspect in terms of how JavaScript is actually running on the web, in production, on real sites, etc. But read the findings and make your own judgments, of course. 

Tune in. Enjoy.

Microsoft Research: Tools to Help Resolve Concurrency Problems

March 5, 10 //
Comments Off

If you are developing multi-threaded applications, there is a possibility that you may be having concurrency problems, and these problems can be difficult to reproduce and identify.

At PDC09, Madan Musuvathi and Sebastian Burckhardt showed off some tools (“Cuzz” and “FeatherLite”) that Microsoft Research is currently working on that may one day assist developers in addressing concurrency issues they may be having in their application. I’ve invited them to join me today to talk with us about some of the issues involved with tracking down concurrency problems, as well as how each tool works.

If you’d like more information about the tools they are working on, you may want to check out their PDC09 session, which is available here:

You can also find more details about what Madan and Sebastian are doing in Microsoft Research on the Microsoft Research Website:

The Verification Corner – Specifications in Action with Spec#

March 1, 10 //
Comments Off

In this episode of The Verification Corner, Rustan Leino gives a demonstration of specifications in action. He builds a program that chunks strings into pieces, i.e. a chunker, in Spec#. During the demo, he shows the verifier, the developer, and the specifications fit together in the development cycle. Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research.

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

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

February 9, 10 //
Comments Off

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).

Read Yuri’s Annotated Articles

Tune in. Meet Yuri Gurevich.

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

January 29, 10 //
Comments Off

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…

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

The Verification Corner: Loop Invariants

January 12, 10 //
Comments Off

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.

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.

« Older Entries