Difference between revisions of "Projects"

From FSL
Jump to: navigation, search
m
 
(32 intermediate revisions by 5 users not shown)
Line 1: Line 1:
 
__NOTOC__ __NOEDITSECTION__
 
__NOTOC__ __NOEDITSECTION__
{{Header | [[Circ]]}}
+
Currently our research falls into one of the following three areas:
 +
: '''''[[K and Matching Logic | Programming Language Design and Semantics]]'''''
 +
: '''''[[Runtime Verification]]'''''
 +
: '''''[[Circ | Behavioral Specification]]'''''
 +
You want to work on these topics? See [[Grigore Rosu]]'s list of [[Open Problems and Challenges]].
 +
Below are our specific projects (at least one of us is working on one of these).
  
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 [[ Circ | [more ...]]] {{TryItOnline|Special:CircOnline}}
 
  
{{Header | [[jPredictor]]}}
+
{{Header | [[k: | K]]}}
  
[[Concurrent Runtime Verification | 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 logic repository | MOP logics]]) can also be detected. Static analisis can be used to improve the predictive capability of concurrent runtime verification.  [[Concurrent Runtime Verification | [more ...]]]
+
'''''[[k: | 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 [[k: | [more ...]]]
:* [[jPredictor]] is a concurrent runtime verification tool for Java
+
  
{{Header | [[k:Main Page | K]]}}
 
  
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 [http://maude.cs.uiuc.edu Maude] implementations.  The earlier Rewriting Logic Semantics definitions are similar in spirit to K.  Two of the most complete definitions are listed below:
+
{{Header | [[:ml:Matching Logic|Matching Logic]]}}
  
* [[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. [[ KOOL | [more ...]]] {{TryItOnline|Special:KOOLOnline}}
+
'''''[[:ml:Matching Logic | 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 [[:ml:Matching Logic | [more ...]]]  
  
* [[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.  [[ K-Scheme | [more ...]]]  {{TryItOnline|Special:KSchemeOnline}}
 
 
{{Header | [[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.  [[Matching Logic | [more ...]]] {{TryItOnline|Special:MLOnline}}
 
  
 
{{Header | [[MOP]]}}
 
{{Header | [[MOP]]}}
  
 
'''''[[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.  [[Monitoring-Oriented Programming | [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.  [[Monitoring-Oriented Programming | [more ...]]]  
:* '''''[[JavaMOP]]''''' is an MOP tool for Java
+
 
:* '''''[[Special:BusMOPOnline|BusMOP]]''''' is an MOP tool for monitoring consumer off the shelf components over a bus
+
 
 +
{{Header | [[jPredictor]]}}
 +
 
 +
[[Predictive Runtime Analysis | 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.  [[Predictive Runtime Analysis | [more ...]]]
 +
 
 +
 
 +
{{Header | [[Circ]]}}
 +
 
 +
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 [[ Circ | [more ...]]]
 +
 
 +
 
 +
{{Header | [[ROSRV]]}}
 +
 
 +
'''''[[ROSRV]]''''' is a runtime verification framework for the Robot Operating System (ROS). ROS is an open-source framework for robot software development, providing operating system-like functionality on heterogeneous computer clusters. With the wide adoption of ROS, its safety and security are becoming an important problem. [[ ROSRV | [more ...]]]
 +
 
  
 
== Past Projects ==
 
== Past Projects ==
 +
  
 
{{Header | [[Generic First-Order Logic | GFOL]]}}
 
{{Header | [[Generic First-Order Logic | GFOL]]}}
  
 
[[Generic First-Order Logic | 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 [[Generic First-Order Logic | GFOL]].  This has an important methodological consequence for our calculi- and programming-languages- specification goals: the "general purpose" [[Generic First-Order Logic | GFOL]] semantics offers, in a uniform way, meaningful semantics for each particular specified calculus [[ Generic First-Order Logic | [more ...]]]
 
[[Generic First-Order Logic | 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 [[Generic First-Order Logic | GFOL]].  This has an important methodological consequence for our calculi- and programming-languages- specification goals: the "general purpose" [[Generic First-Order Logic | GFOL]] semantics offers, in a uniform way, meaningful semantics for each particular specified calculus [[ Generic First-Order Logic | [more ...]]]

Latest revision as of 03:43, 26 February 2016

Currently our research falls into one of the following three areas:

Programming Language Design and Semantics
Runtime Verification
Behavioral Specification

You want to work on these topics? See Grigore Rosu's list of Open Problems and Challenges. Below are our specific projects (at least one of us is working on one of these).


K

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

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


MOP

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


jPredictor

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

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


ROSRV

ROSRV is a runtime verification framework for the Robot Operating System (ROS). ROS is an open-source framework for robot software development, providing operating system-like functionality on heterogeneous computer clusters. With the wide adoption of ROS, its safety and security are becoming an important problem. [more ...]


Past Projects

GFOL

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
Namespaces

Variants
Actions
Navigation