Currently our research falls into one of the following three areas:
Below we list our specific projects.
K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program [more ...]
Matching logic allows us to regard a language through both operational and axiomatic lenses at the same time, making no distinction between the two. A programming language is given a semantics as a set of rewrite rules. A language-independent proof system can then be used to derive both operational behaviours and formal properties of a program. In other words, one matching logic semantics fulfils the roles of both operational and axiomatic semantics in a uniform manner [more ...]
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 ...]
Predictive runtime analysis is a technique to detect potential concurrency errors in a system by observing its execution traces; the analyzed execution traces may not necessarily hit the errors directly. Typical concurrency errors that can be predictively detected include dataraces and deadlocks, both notoriously hard to find by just ordinary testing. We also have techniques that can predict general safety property violations, expressed using any formalism that permits monitor sythesis, including temporal logics and regular patterns. [more ...]
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 ...]
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 ...]