Windows 7 Bart De Smet: LINQ to Z3

Discussion in 'Live RSS Feeds' started by News, Nov 23, 2010.

  1. News

    News Extraordinary Robot
    News Feed

    Jun 27, 2006
    Likes Received:
    Bart De Smet is one of the highly talented software engineers on Erik Meijer's team and the chief architect of the LINQ to Anything dream. You should watch his excellent PDC10 session on this topic.As you learned on Channel 9 Live's PDC10 conversation with Wolfram Schulte and Erik Meijer, Z3 is a theorem prover (the fastest in the world, in fact). Z3 is one of several advanced software engineering technologies coming out of MSR's RiSE team.

    A while ago, Bart implemented a LINQ to Z3 library and I've wanted to dig into this with him for some time. Recently, I got the chance to do just that and it makes for an excellent episode of Going Deep.

    Bart writes in his initial post on the LINQ to Z3 project:

    With LINQ to Z3 my goal is to abstract away from the low-level Z3 APIs and provide nice syntax with rich static typing support on top of it. The basic idea is the following:

    • Define the “shape” of a theorem, e.g. what symbolic names (and their types) to use;
    • Express constraints over those symbolic names using LINQ syntax (more specifically the where keyword);
    • Ask the resulting object for a solution, resulting in an instance of the “shape” type specified at the start.
    An example of LINQ to Z3:

    var theorem = from t in ctx.NewTheorem() where t.X1 - t.X2 >= 1 where t.X1 - t.X2

Share This Page