Home

Carlo A. Furia

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

  2. Refinement and Verification of Real-Time Systems.

    Wed, 02/10/2010 - 16:01 — SomNambul
    Authors: Carlo A. Furia, Paul Z. Kolano, Richard A. Kemmerer, Dino Mandrioli
    Subjects: Logic in Computer Science
    Abstract

    This paper discusses highly general mechanisms for specifying the refinement
    of a real-time system as a collection of lower level parallel components that
    preserve the timing and functional requirements of the upper level
    specification. These mechanisms are discussed in the context of ASTRAL, which
    is a formal specification language for real-time systems.

  3. What's Decidable About Sequences?.

    Thu, 01/14/2010 - 16:01 — SomNambul
    Authors: Carlo A. Furia
    Subjects: Logic in Computer Science
    Abstract

    We present a first-order theory of sequences with integer elements,
    Presburger arithmetic, and regular constraints, which can model significant
    properties of data structures such as arrays and lists. We give a decision
    procedure for the quantifier-free fragment, based on an encoding into the
    first-order theory of concatenation; the procedure has PSPACE complexity.

  4. A Theory of Sampling for Continuous-time Metric Temporal Logic.

    Tue, 12/01/2009 - 16:01 — SomNambul
    Authors: Carlo A. Furia, Matteo Rossi
    Subjects: Logic in Computer Science
    Abstract

    This paper revisits the classical notion of sampling in the setting of
    real-time temporal logics for the modeling and analysis of systems. The
    relationship between the satisfiability of Metric Temporal Logic (MTL) formulas
    over continuous-time models and over discrete-time models is studied; more
    precisely, it is shown to what extent discrete-time sequences obtained by
    sampling continuous-time signals capture the semantics of MTL formulas over the
    two time domains.

  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