Formal Methods and Safety Critical Systems

Welcome to the formal methods and critical systems group's website at UIUC. Our group currently consists of the following personnel:

Meetings and Presentations

Any UIUC student, visitor or faculty member is welcome to subscribe to our list and to attend our meetings. To subscribe, please follow this link.

We currently meet every Thursday at 4:00PM in 368 CSL, but sometimes there are exceptions, so make sure that you check the exact meeting place, date and time. Below is a list of recent presentations. Links to all presentations can be found here.

Thursday, March 13, 4:00PM, 368CSL
Mark-Oliver Stehr
The Open Calculus of Constructions: Rewriting with Dependent Types

Rewriting logic provides a powerful first-order logical and semantic framework for the specification of computational systems that can deal with functional behavior as well as with concurrency and nondeterminism. Modern type theories with dependent types, on the other hand, are higher-order functional programming languages in which higher-order logics can be interpreted according to the Curry-Howard-isomorphism.

With the open calculus of constructions we explore the interaction between two key features: conditional rewriting modulo equational theories as in rewriting logic (with its membership equational sublogic) and dependent types with universes as they are known from Martin-Loef's type theory and the calculus of constructions. The resulting formalism is surprisingly powerful and it has many interesting applications including higher-order equational/behavioral programming/specification, inductive/coinductive theorem proving, theorem proving modulo equational theories, and specification/analysis of concurrent/reactive systems.

Since the formalism comes with both a classical set-theoretic semantics and an operational semantics, it is especially suitable to formalize mathematical theories in a computational fashion, category theory being one example as indicated for instance by a formalization of the categorical semantics of rewriting logic itself. A prototype of the open calculus of constructions has been developed on the top of the Maude rewriting engine and several examples will be presented in this talk.

Friday, March 07, 4:00PM, B02 (Auditorium) CSL
David MacQueen, University of Chicago
Should ML be Object-Oriented

At a fundamental level, functional and object-oriented programming languages are all ``higher-order'', in the sense that they support computing with values that are themselves pieces of program code encapsulated with a local environment. In functional languages these ``active'' values are functions, while in object-oriented languages they are objects. Both styles of higher-order language claim to provide good support for writing adaptable programs, but functional and object-oriented languages achieve this adaptability in different ways: functional programs rely on parameterization at the value, type and module level, while object-oriented languages rely primarily on subtyping and implementation inheritance.

In this talk I compare these two approaches, mainly in terms of the features and properties of their type systems, and consider the benefits and disadvantages of unifying (or merging) the two paradigms by adding object-oriented features to ML as a base language. We argue that while some of the simpler aspects of object-oriented languages are compatible with ML, adding a full-fledged class-based object system to ML leads to an excessively complex type system and relatively little expressive gain, especially if we aim to preserve that mostly functional style of programming that is a major advantage of ML.

Thursday, February 27, 4:00PM, 368CSL
Miguel Palomino Tarjuelo
Equational Abstractions

Abstraction reduces the problem of whether an infinite state system satisfies a temporal logic property to model checking that property on a finite state abstract version. The most common abstractions are quotients of the original system. We present a simple method of defining quotient abstractions by means of equations collapsing the set of states. The method assumes that the concurrent system has been specified by means of a rewrite theory $\mathcal{R}=(\Sigma,E,R)$, and consists on adding more equations, say $E'$, to get a quotient system specified by the rewrite theory $\mathcal{R}/E'=(\Sigma,E\cup E',R)$. We call such a system an {\em equational abstraction} of $\mathcal{R}$. This equational abstraction is useful for model checking purposes if: (1) $\mathcal{R}/E`$ is an {\em executable} rewrite theory in an appropriate sense; and (2) the state predicates are {\em preserved} by the quotient simulation. Requirements (1) and (2) are {\em proof obligations} that can be discharged by theorem proving methods. Our approach can be mechanized using the rewriting logic language Maude and its associated LTL model checker, inductive theorem prover, and coherence checker.

Links

Last update: 7 March 2003
grosu@uiuc.edu