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.

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.

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.

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