Home

Bertrand Meyer

  1. A comprehensive operational semantics of the SCOOP programming model.

    Thu, 01/06/2011 - 16:01 — SomNambul
    Authors: Bertrand Meyer, Sebastian Nanz, Benjamin Morandi
    Subjects: and Cluster Computing, Distributed, Parallel
    Abstract

    Operational semantics has established itself as a flexible but rigorous means
    to describe the meaning of programming languages. Oftentimes, it is felt
    necessary to keep a semantics small, for example to facilitate its use for
    model checking by avoiding state space explosion. However, omitting many
    details in a semantics typically makes results valid for a limited core
    language only, leaving a wide gap towards any real implementation.

  2. A Comparative Study of the Usability of Two Object-oriented Concurrent Programming Languages.

    Tue, 11/30/2010 - 16:01 — SomNambul
    Authors: Bertrand Meyer, Sebastian Nanz, Faraz Torshizi, Michela Pedroni
    Subjects: Programming Languages
    Abstract

    Concurrency has been rapidly gaining importance in general-purpose computing,
    caused by the recent turn towards multicore processing architectures. As a
    result, an increasing number of developers have to learn to write concurrent
    programs, a task that is known to be hard even for the expert. Language
    designers are therefore working on languages that promise to make concurrent
    programming "easier" than using traditional thread libraries.

  3. Specifying Reusable Components.

    Wed, 03/31/2010 - 15:02 — SomNambul
    Authors: Carlo A. Furia, Bertrand Meyer, Nadia Polikarpova
    Subjects: Software Engineering
    Abstract

    Reusable software components need expressive specifications. This paper
    outlines a rigorous foundation to model-based contracts, a method to equip
    classes with strong contracts that support accurate design, implementation, and
    formal verification of reusable components. Model-based contracts
    conservatively extend the classic Design by Contract with a notion of model,
    which underpins the precise definitions of such concepts as abstract
    equivalence and specification completeness.

  4. The theory and calculus of aliasing.

    Thu, 01/14/2010 - 16:01 — SomNambul
    Authors: Bertrand Meyer
    Subjects: Software Engineering
    Abstract

    A theory, graphical notation, mathematical calculus and implementation for
    finding whether two given expressions can, at execution time, denote references
    attached to the same object. Intended as the basis for a comprehensive solution
    to the "frame problem" and as a complement to, or even a replacement for,
    separation logic, shape analysis, ownership types and dynamic frames.

  5. Inferring Loop Invariants using Postconditions.

    Mon, 09/07/2009 - 22:13 — SomNambul
    Authors: Carlo A. Furia, Bertrand Meyer
    Subjects: Software Engineering
    Abstract

    One of the obstacles in automatic program proving is to obtain suitable loop
    invariants.

    The invariant of a loop is a weakened form of its postcondition (the loop's
    goal, also known as its contract); the present work takes advantage of this
    observation by using the postcondition as the basis for invariant inference,
    using various heuristics such as "uncoupling" which prove useful in many
    important algorithms.

    Thanks to these heuristics, the technique is able to infer invariants for a
    large variety of loop examples.

Math-arch

Syndicate content