## Monday, 24 September 2012

### Regular Expression Sub-Matching using Partial Derivatives

Here's our paper and the talk presented at PPDP'12.
There's quite a bit of recent interest in the use of derivatives for matching and parsing, e.g. see the works by Owens/Reppy/Turon on "Regular-expression derivatives reexamined" and Might/Darais/Spiewak on "Parsing with derivatives: a functional pearl".
Our use of derivatives and partial derivatives for regular expression sub-matching
is inspired by our own prior where we derive up-cast and down-cast coercions out of a proof system describing regular expression containment based on partial derivatives. See our APLAS'04 and ML Workshop'05 papers.

## Friday, 27 July 2012

### Model Checking DSL-Generated C Source Code

We report on the application of SPIN for
model-checking C source code which is generated out of
a textual domain-specific language (DSL).
We have built a tool which automatically generates the necessary
SPIN wrapper code using (meta-)information available at the DSL level.
The approach is part of a larger tool-chain
for developing mission critical applications.
The main purpose of SPIN is for bug-finding where
error traces resulting from SPIN
can be automatically replayed at the DSL level and
yield concise explanations in terms of a temporal specification DSL.
The tool-chain is applied in some large scale
industrial applications.

The paper appeared in SPIN'12. Here are links to the paper, talk and implementation.

Labels:
dsl,
haskell,
linear temporal logic,
model-checking

## Friday, 8 June 2012

### Regular Expression Sub-Matching using Partial Derivatives

Regular expression sub-matching is the problem of finding for
each sub-part of a regular expression a matching sub-string.
Prior work applies Thompson and Glushkov NFA methods for the construction
of the matching automata. We propose the novel use of derivatives and
partial derivatives for regular expression sub-matching.
Our benchmarking results show that the run-time performance is promising
and that our approach can be applied in practice.

Here's a link to the paper and the implementation.

This is the substantially revised and almost completely re-written (paper and implementation) version of our earlier draft.

Labels:
haskell,
partial derivatives,
regular expressions

## Monday, 4 June 2012

### Constructive Finite Trace Analysis with Linear Temporal Logic

We consider linear temporal logic (LTL) for run-time testing
over limited time periods. The technical challenge
is to check if the finite trace produced by the system
under test matches the LTL property.
We present a constructive solution to this problem.
Our finite trace LTL matching algorithm
yields a proof explaining why a match exists.
We apply our constructive LTL matching
method to check if LTL properties are sufficiently covered
by traces resulting from tests.

The paper appeared in TAP'12. Here's a link to the paper and the talk.

The system has been implemented in Haskell and is applied in some real-world projects. Some of the Haskell source code will be made publicly available (later in the year).

Subscribe to:
Posts (Atom)