From FSL
Revision as of 14:27, 13 April 2010 by Stefane1 (Talk | contribs)

Jump to: navigation, search

Circ is an automated prover that is implemented as an extension of Maude. Circ implements the circularity principle, which generalizes both circular coinduction and structural induction, and can be expressed in plain English as follows. Assume that each equation of interest (to be proved) e admits a frozen form fr(e) and a set of derived equations [more ...] Online-sm.JPG


Concurrent runtime verification aims at detecting concurrency errors in a system by running it and observing its execution traces; errors can be detected despite the fact that the analyzed execution traces may not necessarily hit them. Typical concurrency errors include dataraces and deadlocks, both notoriously hard to detect by ordinary testing, but general safety property violations (expressed using MOP logics) can also be detected. Static analisis can be used to improve the predictive capability of concurrent runtime verification. [more ...]

  • jPredictor is a concurrent runtime verification tool for Java

K is a general purpose programming paradigm that is particularly suited for formally defining programming languages. It extends rewriting logic, and all of our current language definitions have Maude implementations. The earlier Rewriting Logic Semantics definitions are similar in spirit to K. Two of the most complete definitions are listed below:

  • KOOL is an experimental object-oriented language, being developed with the rewrite-based K framework. It is a pure and dynamic language, with support for a wide range of existing features, including named, parameterized exceptions

(exceptions are classes) and runtime type inspection. The current version also includes support for basic concurrency, allowing arbitrary expressions to be spawned in threads and used in locks. [more ...] Online-sm.JPG

  • K-Scheme is a definition of Scheme written in the rewrite-based K framework.

K-Scheme supports the meta-programming features of Scheme, as well as giving an executable specification for much of the (finite) non-determinism allowed in Scheme by the specification. [more ...] Online-sm.JPG

Matching Logic

Matching Logic, a program verification logic inspired by RLS. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Patterns can naturally specify data separation and require no special support from the underlying logic. [more ...] Online-sm.JPG


Monitoring-Oriented Programming, abbreviated MOP, is a software development and analysis framework aiming at reducing the gap between formal specification and implementation by allowing them together to form a system. In MOP, runtime monitoring is supported and encouraged as a fundamental principle for building reliable software. [more ...]

  • JavaMOP is an MOP tool for Java
  • BusMOP is an MOP tool for monitoring consumer off the shelf components over a bus

Past Projects


GFOL is a logic whose formulae are built using the traditional first-order connectives and quantifiers, but whose terms are generic, in the sense that no particular syntax is assumed for them. Terms are only required to constitute a term syntax, i.e., to have free variables and substitution that obey some natural axioms. Classical first-order terms, as well as any type of terms involving bindings, fall into this category. Many lambda calculi can be viewed as (and not merely encoded as) theories in GFOL. This has an important methodological consequence for our calculi- and programming-languages- specification goals: the "general purpose" GFOL semantics offers, in a uniform way, meaningful semantics for each particular specified calculus [more ...]

Personal tools