A Domain-Specific Language for Regular Sets of Strings and Trees.
AbstractWe propose a new high-level programming notation, called FIDO, that we have designed to concisely express regular sets of strings or trees. In particular, it can be viewed as a domain-specific language for the expression of finite-state automata on large alphabets (of sometimes astronomical size). FIDO is based on a combination of mathematical logic and programming language concepts. This combination shares no similarities with usual logic programming languages. FIDO compiles into finite-state string or tree automata, so there is no concept of run-time.It has already been applied to a variety of problems of considerable complexity and practical interest. In the present paper, we motivate the need for a language like FIDO, and discuss our design and its implementation. Also, we briefly discuss design criteria for domain-specific languages that we have learned from the work with FIDO. We show how recursive data types, unification, implicit coercions, and subtyping can be merged with a variation of predicate logic, called the Monadic Second-order Logic (M2L) on trees. FIDO is translated first into pure M2L via suitable encodings, and finally into finite-state automata through the MONA tool.
Introduction
Finite-state problems are everywhere, embedded in
many layers of software systems, but are often difficult
to extract and solve computationally. This
basic observation is the motivation for the work presented
in this paper.
Recent research by us and our colleagues has exploited
the Monadic Second-Order Logic (M2L) on
finite strings and trees to solve interesting and challenging
problems. In each case, the results are obtained
by identifying an inherent regularity in the
problem domain, thus reducing the problem to questions
of regular string or tree languages. Successful
applications today include verification of concurrent
systems [9, 8], hardware verification [2], software engineering
[10], and pointer verification [7]. Work in
progress involves a graphical user interface for regular
expressions extended with M2L and document
logics for the WWW.
The r-ole of M2L in this approach is to provide an extraordinarily
succinct notation for complicated regular
sets. Our applications have demonstrated that
this notation in essence can be used to describe
properties, where finite state automata, regular ex-
pressions, and grammars would be tend to be cum-
bersome, voluminous, or removed from the user's
intuition. This is hardly surprising, since M2L is
a variation on predicate logic and thus natural to
use. Also, it is known to be non-elementarily more
succinct than the other notations mentioned above.
Thus, some formulas in M2L describe regular sets
for which the size of a corresponding DFA compared
to the size of the formula is not bounded by any finite
stack of exponentials.
The flip side of this impressive succinctness is that
M2L correspondingly has a non-elementary lower
bound on its decision procedure. Surprisingly, the
MONA implementation of M2L [5] can handle non-trivial
formulas, some as large as 500,000 charac-
ters. This is due in part to the application of BDD
techniques [4], specialized algorithms on finite-state
automata [3], and careful tuning of the implementation
[11]. Also, it turns out that the intermediate
automata generated, even those resulting from sub-set
constructions, are usually not big compared to
the automata representing the properties reasoned
about.
The successful applications of M2L and MONA reside
in a common, productive niche: they require
the specification of regular sets that are too complicated
to describe by other means, but not so complicated
as to be infeasible for our tools.
While the basic M2L formalism is simple and quite
intuitive, early experience quickly indicated that
this formalism in practice suffers from its primitive
domain of discourse: bit-labeled strings and trees.
In fact, M2L specifications are uncomfortably similar
to assembly code programs in their focus on
explicit manipulations of bit patterns. For M2L interpreted
on trees, the situation is even worse, since
the theory of two or more successors is far less familiar
and intuitive than the linear sublogic.
Similarly to the early experiences with machine lan-
guages, we found that M2L "programmers" spent
most of their time debugging cumbersome encodings

Our contributions
In this paper, we propose a domain-specific programming
formalism FIDO that combines mathematical
logic and recursive data types in what we
believe are new ways.
We suggest the following four kinds of values: finite
domains, recursive data values (labeled by finite
domains), positions in recursive data values,
and subsets of such positions. We show that many
common programming language concepts (like sub-
typing, coercions, and unification) make sense when
the underlying semantics is based on assigning an
automaton (and not a store transformer) to expressions

This semantic property allows us to view the compilation
process as calculations on values that are
deterministic, finite-state automata, just as an expression
evaluator calculates on numbers to arrive
at a result. That is, automata are the primitive objects
that are subjected to operations reflecting the
semantics of the language.
This view is quite different from the method behind
most state-machine formalisms used in verification
(such as the Promela language [6]): a language resembling
a general purpose language expresses a single
finite-state machine, whose state space and transition
system is constructed piecemeal from calculations
that explore the state space.
Our view, however, is similar to some uses of regular
expressions for text matching, except that most
implemented algorithms avoid the construction of
deterministic automata.
FIDO is implemented and provides, along with supporting
tools, an optimizing compiler into M2L for-
mulas. It has been used for several real-life applications
and is also the source of the biggest formulas
yet handled by MONA.
In this article, we motivate and explain FIDO. In
particular, we discuss the type system and compilation
techniques. We also give several examples
(some taken from articles already published, where
we have used FIDO without explaining its origin
or design). Some technical considerations concerning
the relationship between our data structures for
tree automaton representation [3] and the compilation
process will be explained elsewhere.
2 M2L and MONA
Basic M2L has a very simple syntax and seman-
tics. Formulas are interpreted on a binary tree (or
a string) labeled with bit patterns determining the
values of free variables. First-order terms (t) denote
positions in the tree and include first-order variables
(p) and successors (t:0 and t:1). Second-order terms
(T ) denote sets of positions (i.e. monadic predi-
cates) and include second-order variables (P ), the
empty set (;), unions (T 1
). The basic predicates are set membership
), and set inclusion T 1
). The logic
permits the usual connectives (-, :) and first
and second-order quantifiers
). By
convention, a leaf is a position p for which
p:1. The sublogic for strings uses only the
0-successor.
The MONA tool accepts such formulas in a suitable
ASCII syntax and produces a minimum DFA
that accepts all trees satisfying the given formula.
Thus, satisfiability of a formula is equivalent to non-
emptyness of the derived automaton, and validity is
equivalent to totality. The values of free variables
in the formula are encoded in the alphabet of the
automaton. Thus, a formula with
yields an alphabet \Sigma of size 2 32 . In the internal representation
of these automata, the transition function
is shared, multi-terminal \Sigma-BDD. With these
BDD techniques, the MONA tool has processed formulas
with hundreds of thousands of characters in
a few minutes.
3 The Motivation
A small example will motivate the need for a high-level
notation. Assume that we wish to use MONA
to prove the following (not too hard) theorem: for
every string in (a+b)   c, any a is eventually followed
by c.
To state this theorem in M2L, we must first choose
an encoding of the labels a, b, and c. For this purpose
we introduce two free second-order variables
. The labels can be encoded according to
the following (arbitrary) schema: a position p has
label a if
, that is, a corresponds to
the bit pattern 00. Similarly, we can assign to b the
bit pattern 01 and to c the pattern 10. The property
"a is eventually followed by c" becomes the formula:
The regular expression (a+b)   c can in a similar way
be encoded as the formula:
and the theorem above is then formally stated as
the implication OE ) /. The MONA tool will readily
verify that this formula is an M2L tautology, thus
proving our theorem.
A reason for M2L specifications being much more
voluminous than promised should now be apparent:
there is a significant overhead in encodings. More-
over, there are no automatic checks of the consistent
use of bit patterns.
Support for such encodings is usually supplied by
a type system. For M2L on strings, regular sets
immediately suggest themselves as notions of types.
It is quite common for M2L formulas to be of the
implicational form OE ) /, where OE is a formula
restricting the strings to a coarse regular set and
/ provides the more intricate restrictions. Thus, a
high-level version of the above formula could look
like:
string x: (a+b)   c;
The keywords string and pos are intended to declare
free variables of these two kinds. This formula can
be read as: "for all positions p in the string x, if p
has label a, then there exists a position q, also in x,
such that p is before q and q has label c". The main
formula is almost the same as the MONA version,
but the proper use of labels is now supported by the
compiler and can be verified by a type checker.
For M2L interpreted on trees, however, there is no
intuitive analogue to regular expressions. But from
programming languages we know an intuitive and
successful formalism for specifying coarse regular
sets of trees: recursive data types. Thus, we adopt a
well-known and trusted programming concept into
our high-level notation. Using this idea, we may
prove our theorem as follows:
string x: T;
Arbitrary recursive data types may of course be expressed
directly as formulas, but the translation is
voluminous and best performed automatically. The
translation also solves the problem that the Mona
decision procedure works on formulas whose domain
of discourse is only binary trees, whereas values of
recursive data types are trees with a varying number
of branches. (The solution is rather technical, since
it involves bending the recursive data type value into
the shape of a binary branching tree.)
Note that not all regular tree sets can be captured
by recursive data types. Consider binary trees, in
which nodes are colored red, green, or blue. The
subset of trees in which at most one node is colored
blue is not a recursive data type; however, it is easily
captured by the following FIDO specification:
tree x: RGB;
Certainly, more advanced and complicated notions
of data types could similarly be adopted [1]. How-
ever, the FIDO philosophy is to rely heavily on standard
programming language concepts to describe
complex structures and operations. The ambition is
that these idioms should be merged seamlessly with
logical concepts that describe complex properties of
such structures.
In general, we allow finite domains (from which the
name FIDO derives) to be the values of nodes. Finite
domains are constructed conjunctively and disjunctively
from enumerated and scalar types. Thus
the alphabets of tree automata reading such recursive
data types easily become very large.
4 The Design
While this paper is not intended as a proper language
report, we will explain the more interesting
or unusual concepts that the FIDO notation provides

Domains and Data Types
Finite domains are constructed from simple scalar
lists, freely combined with a product operator (&)
and a union operator (j). When the union of two
finite domains is formed, it is required that they are
disjoint. Thus, if we define the domains:
then a value of the domain State may be written
as State:[a,b,2]. From the more complicated definitions

we obtain values as: E:[a1,[a2,b3,[a2,b1]]]. In for-
mulas, finite domain values may be unified using a
syntax such as State:[pc?,a,r?], where ps and r are
unification variables.
The recursive data types are quite ordinary, except
that the constructors are generalized from single
names to finite domains.
The finite domains could of course be encoded as
(non-recursive) data types. We have chosen to have
a separate concept for several reasons. First, the
distinction between trees and their labels seems intuitive
for many applications. Second, we can allow
more operations on finite domains that on trees; for
example, the introduction of unification or concatenation
on trees would yield an undecidable formal-
ism. Third, in the translation into automata, finite
domains are encoded in BDDs whereas trees are encoded
in the state space; often, it is necessary for
the programmer to control this choice. An example
is:
which is a linear data type of sequences of state
values terminated by a node labeled done. A non-linear
example is:
denoting some binary trees. The notation [1.10]
abbreviates the corresponding 10 scalars.
Variables
There are four kinds of variables in FIDO. We introduce
them by examples. A domain variable s that
ranges over states may be declared as
dom S: State;
Tree variables (recursive data type variables) x and
y may be declared as:
tree x,y: Tree;
Each variable defines its own space of positions.
Thus, a position in x cannot be used to denote a
node in y. To declare a position variable that may
denote positions in either x or y, we write:
pos p: x,
A value of this variable points to a node in either x
or y, but in any case, the node pointed to is either
red or black. Similarly, a set variable S containing
positions in the union of x's and y's position spaces
may be declared as:
set S: x,
Quantification
All variables can be quantified over. For example,
the formula "there is a computation that contains a
loop" may involve quantification over both strings
(trees), finite domains, and positions:
9string x: Comp. 9dom s: State.
9pos p,q: x.(p!q - p=s - q=s)
Types
A type may have one of four different kinds: pos,
set, dom, and tree. The pos kind corresponds to
first-order terms, i.e. positions in trees; the set kind
similarly encompasses second-order terms; the dom
kind is new compared to M2L and describes values
of finite domains; finally, the tree kind is a further
extension that captures entire trees as values.
Within each kind, a type is further refined by a set
of tree names and a set of data type names. For
example, the type (pos,fx,yg,fR,S,Tg) denotes positions
of nodes in either the tree x or y that are
roots of subtrees of one of the data types R, S, or
T. These refined types prove to be very convenient
in restricting free variables in the model and in expressing
relativized quantifications. Furthermore,
this type structure proves crucial for optimizations
in the implementation.
The type rules impose restrictions on all operators
in the language. Generally, the rules boil down to
trivial statements about finite sets. For example,
if the terms s i
have types (set,X i
has type (set,X 1
Also, if the term
has type (pos,X,D), then the term p.n has type
T.n is the data type
reached from T along an n-successor.
Some formulas can be decided purely on the basis
of the type system. For example, if p has type
and s has type (set,X s ,D s ), then the
;. Such static decisions are exploited by the FIDO
compiler.
Notational Conveniences
A formal notation has a tendency to become a quagmire
of details. In the design of FIDO, we have
attacked this problem in three different ways.
First, it is often convenient implicitly to coerce values
between different kinds. This we have expressed
through a simple subtype structure. Two types
are related by the sub-type
in the following finite order:
@
@
@
tree
set
dom
pos
posset
root
read
The order relations have been decorated with coercions
functions: posset computes the set of positions
in a tree, root finds the root positions of a tree, and
read computes the label of a position. This subtype
structure is exploited to automatically insert coer-
cions. Note that our subtype structure clearly is
semantically coherent, so that coercions are unique
[12]. If we added the coercion: singleton: pos !
set, then semantic coherence would fail.
Second, we allow implicit casts between finite do-
mains. For example, in the definitions:
we will allow values of the domains Fruit and Root
to be used directly as values of the domain Veg-
etable, even though they strictly speaking should be
expressed as e.g. cast(Fruit:apple,Vegetable).
Third, we allow sensible defaults whenever possible.
Thus, if a name can unambiguously be determined
to have a specific meaning, then all formal qualifiers
may be dismissed. For example, if the name orange
is only used as a scalar in the domain Fruit, then
the constant Fruit:orange may be written simply as
orange.
As a specific example of these techniques, consider
the previous theorem:
We have already used a number of syntactic conveniences
here. From the above specification, the
compiler inserts the necessary coercions to reconstruct
the more explicit code:
9pos q:x,T.(p!q - read(q)=T:c))
which is somewhat harder to read. In a real-life
12-page formula, more than 400 such pedantic corrections
are automatically performed.
Decompilers
Any compiler writer must also consider the need
for decompilers. In the case of FIDO and MONA,
specifications are translated into a more primitive
logic. This is fine, if we only want to decide valid-
ity. However, MONA also has the ability to generate
counter-examples for invalid formulas. But a
MONA counter-example will make little sense for a
FIDO programmer, since it will have a completely
different structure and be riddled with bit patterns.
Consequently, the FIDO system provides a decompiler
that lifts such counter-examples into the high-level
syntax.
Another use of MONA, illustrated in the following
section, is to generate specific automata. For this
application, FIDO provides a different decompiler
that expresses an automaton as a particular kind
of attribute grammar at the level of recursive data
types.
5 Examples
We now provide a few examples illustrating the benefits
of the FIDO notation. We include applications
that aim to synthesize automata as well as some that
aim to verify properties. For each case we present a
toy example in some detail and sketch a large, previously
published application of a similar nature.
Synthesis
The following example considers (a fragment of) the
HTML syntax. Not all syntactically correct HTML-
specifications should be allowed. For example, a
document should never contain an anchor within
another anchor (to not confuse the reader). Such
a constraint could be incorporated into the context-free
syntax, but it would essentially double the number
of non-terminals. However, we can easily capture
HTML parse trees as values of a recursive data
type. On these trees we can then express as a logical
formula the restriction that we wish to impose:
anchor(u: URL, a: HTML) j
paragraph j
rule j
list(l: LIST);
follows:
The transition HTML j anchor: [0,0] 7! 1 means
that if the node is an anchor and each of its two
subtrees synthesizes the attribute value 0, then it
should synthesize the attribute value 1.
These simple ideas have been exploited in a collaboration
with the Ericsson telecommunications company
to formalize the constraints of design architectures
[10].
Verification
Two specifications, of say distributed systems, can
be compared by means of the implication or bi-
implication connective. Consider a simple-minded
mutual exclusion protocol for two processes with a
shared memory:
Turn: Integer range 1.2 :=
task body Proc1 is
begin
loop
b: loop exit when
d: Turn := 2
task body Proc2 is
begin
loop
b: loop exit when
c: Critical-Section-2;
d: Turn :=
loop
The FIDO specification models all valid interleaved
computations and simply asks whether the safety
property holds:
string ff: Computation;
let dom pc: PC; dom r: Turn.(
[a,pc?,r?] 7! [b,pc?,r?] j
Valid(string x: Computation): formula;
8pos p: x.(
if p.next6=done then
let dom s,t: State.
(p=s?; p.next=t?; Trans(s,t))
Mutex(string x: Computation): formula;
8pos p: x.(p6=[c,c,?])
The formula trans(s,t) . end denotes the binary
relation on State domain values that hold for the
pairs of values that can simultaneously match one
of the listed cases.
The corresponding raw MONA formula looks like:
(p
q in G0) & (q notin
POS-p in S1) !=? s1-p c)) & (POS-p in S2)) & (POS-p in S3))
& ((POS-p in S4) !=? s0-r)) & ((((((POS41 in S0) !=? s0-pc)
POS-p in S3)) & ((POS-p in S4) !=? s0-r)) & ((((((POS41 in
OS-p in S0) !=? s0-pc) & ((POS-p in S1) !=? s1-pc)) & (POS-p
in
POS41 in S0) !=? s0-pc) & (s1-t !=? s1-pc)) & (POS41 in S2)
in
~(POS-p in S3))) & (POS-p in S4)) & ((((((POS41 in S0) !=?
POS41 in S3)) & (POS41 in S4)))) - (((((((POS-p in S0) !=?
(~(POS-p in
in
(~(POS41 in S3))) & ((POS41 in S4) !=? s0-r)))) - ((((((POS
-p in S0) & (POS-p in S1)) & ((POS-p in S2) !=? s0-pc)) & (
(POS-p in S3) !=? s1-pc)) & ((POS-p in S4) !=? s0-r)) & (((
POS-p in S0)) & s1-s) & ((POS-p in S2) !=? s0-pc)) & ((POS-
in
in
(~ (POS41 in S1))) & ((POS41 in S2) !=? s0-pc)) & ((POS41
in
POS41 in S1)) & ((POS41 in S2) !=? s0-pc)) & ((POS41 in S3)
(~(POS41 in S1))) & ((POS41 in S2) !=? s0-pc)) & ((POS41 in
in
Since the simplistic mutual exclusion protocol is
clearly correct, this formula is a tautology. How-
ever, if we mistakenly tried to verify that Proc2
could never enter the critical region:
Mutex(string x: Computation): formula;
8pos p: x.(p6=[?,c,?])
then FIDO would generate the counterexample:
Computation:[b,a,1](
Computation:[b,b,1](
Computation:[c,b,1](
Computation:[d,b,1](
Computation:[a,b,2](
Computation:[a,c,2](
Computation:done)))))));
which exactly describes such a computation.
For more realistic examples, internal events can be
projected away by means of the existential quanti-
fier. In [8], a detailed account is given of an application
of the FIDO language to a verification problem
posed by Broy and Lamport in 1994. The distributed
systems are described in an interval logic,
which is easily defined in FIDO. The evolution of a
system over a finite segment of time is modeled as a
recursive, linear data type with a constructor that
define the current event. Thus position variables
instants. The thousands of events possible
in the distributed systems that are compared
are described by the types:
type
The property to be verified requires 12 pages of
FIDO specification which translates into an M2L
formula of size 500,000 characters.
An entirely different use of FIDO allows us to verify
many properties of PASCAL programs that use
pointers [7]. By encoding a store as a string and using
FIDO formulas to describe the effects of program
statements, we can automatically verify some desirable
properties. An example is the following pro-
gram, which performs an in-situ reversal of a linked
list with colored elements:
program
case tag: Color of
var x,y,p: List;
begin
while x!?nil do
p:=x-.next;
x:=p
end.
With our system, we can automatically verify that
the resulting structure is still a linked list conforming
to the type List. We can also verify that no
pointer errors have occurred, such as dangling references
or unclaimed memory cells. However, we cannot
verify that the resulting list contains the same
colors in reversed order. Still, our partial verification
will clearly serve as a finely masked filter for
many common programming errors.
The PASCAL tool adds another level of compila-
tion, from (simple) PASCAL programs to FIDO
specifications to M2L formulas and finally to finite-state
automata accepting encodings of the initial
stores that are counterexamples. The above program
pages of FIDO specification
which expands into a 60,000 character M2L formula.
The resulting automaton is of course tiny since there
are no counterexamples, but the largest intermediate
result has 74 states and 297 BDD-nodes. A direct
translation into MONA would essentially add
all the complexities of the FIDO compiler to the
implementation of the PASCAL tool.
6 The Implementation
We have implemented parsing, symbol analysis, and
type checking in entirely standard ways. What is
non-standard is that every subterm is compiled into
a tree automaton through an intermediate representation
as an M2L formula. Thus resource allocation
becomes a question of managing bit pattern encodings
of domain values, which are expressed in M2L
formulas. We have strived to achieve a parsimonious
strategy, since every bit squandered may potentially
double the MONA execution time.
As a concrete example, consider the type:
Its encoding in MONA requires seven bits in all.
Two type bits T0 and are used to distinguish
between the types Tree and Enum and special null
nodes in a tree; a single group bit G0 is used to distinguish
between the red-black and the leaf variants;
and four scalar bits S0, S1, S2, and S3 are used to
distinguish between the values of each final domain,
the largest of which is [0.10].
As an example, the formula:
macro TYPE-Tree(var1
(p in T0) & (p notin T1);
expresses that the type Tree is encoded by the bit
pattern 10.
The null nodes are required to encode an arbitrary
fan-out in a binary tree. For example, the tree:
'i
'i
'i
'i
'i
'i
@
@ @
is represented as:
'i
'i
'i
'i
'i
'i
'i
'i
'i
@
@ @
@
@ @
where the null nodes have double lines.
A well-formed value of the type Tree is described
by the MONA predicate TREE Tree. It imposes
the proper relationship between types and values of
nodes and their descendants. A technical problem
is that this predicate is most naturally described
through recursion which is not available in M2L.
This is solved by phrasing the requirements through
a universal quantification that imposes sufficient, local
well-formedness properties:
macro TREE-Tree(var1
(all1 q: (p!=q) =?
The NULL and WF predicates describe the relationship
between a single node and its immediate descendants

macro NULL(var1
(p notin T0) & (p notin T1) &
(p notin G0) &
(p notin
(p notin S2) & (p notin S3);
macro TYPE-Enum(var1
(p notin T0) & (p in T1);
macro GROUP-Tree-red-black(var1
(p notin G0);
macro GROUP-Tree-leaf(var1
(p in G0);
macro GROUP-Tree(var1
macro SCALAR-Enum(var1
(p notin
macro SCALAR-Tree-red-black(var1
macro SCALAR-Tree(var1
macro SUCC-Enum(var1
macro SUCC-Tree-red-black(var1
macro SUCC-Tree-leaf(var1
macro WF-Enum(var1
macro WF-Tree(var1
(p notin S0) & SUCC-Tree-leaf(p)
are encoded in a simple inductive man-
ner. For illustration, consider the tiny formula p2s,
where the arguments are general terms. The term
p of kind pos generates a tuple !
p is a first-order variable constrained by the formula
OE. Similarly, the term s of kind set generates
a tuple ! s; / ?, where s is now a second-order
variable. The term p2s then generates the formula
how existential quantification
corresponds to discharging of registers. It
is a fairly straightforward task to provide similar
templates for all the FIDO constructs, thereby providing
a compositional semantics and a recipe for a
systematic translation.
As a concrete example, consider the formula:
tree x: Tree;
x.left.right.left=red
which describes the regular set of trees in which a
specific node exists and is colored red. It is encoded
as the following MONA formula:
macro DOT-right(var1 p,var1
macro DOT-left(var1 p,var1
assume ex1 p: root(p) & TREE-Tree(p);
ex0 t0-1,t1-1,g0-1,s0-1:
ex0 t0-2,t1-2,g0-2,s0-2:
(t1-1!=?(POS6 in T1)) &
(t0-1!=?(POS6 in T0)) &
(g0-1!=?(POS6 in G0)) &
(s0-1!=?(POS6 in S0)) &
The analogy to run-time is the computation by
MONA of a finite-state automaton from the generated
formula. This is always guaranteed to ter-
minate, but may be prohibitively expensive. Thus,
the FIDO compiler does extensive optimizations at
many levels, in most cases relying heavily on the
type structure. FIDO formulas are symbolically reduced
to detect simple tautologies and to eliminate
unnecessary variables and quantifiers. A careful
strategy is employed to allocate short bit patterns
for finite domains, which includes a global analysis
of concrete uses.
We have also discovered that the FIDO type structure
contains a wealth of information that is not
currently being exploited by the MONA implemen-
tation. An ongoing development effort will enrich
the notion of tree automata to accommodate positional
information that can be derived from FIDO
specifications. This may in some case yield an exponential
speed-up at the MONA level.
7 FIDO as a DSL
In our opinion, FIDO is a compelling example of a
domain-specific language. It is focused on a clearly
defined and narrow domain: formulas in monadic
second-order logic or, equivalently, automata on
large alphabets. It offers solutions to a classical software
problem: drowning in a swamp of low-level en-
codings. It advocates a simple design principle: go
by analogy to standard programming language con-
cepts. It uses a well-known and trusted technol-
ogy: all the phases of a standard compiler, including
optimizations at all levels. It provides unique
benefits that cannot be matched by a library in a
standard programming language: notational con-
veniences, type checking, and global optimizations.
And during its development, we discovered new insights
about the domain: new notions of tree automata
and algorithms.



--R

A specification language based on WS2S.
Hardware verification using monadic second-order logic
Algorithms for guided tree automata.

Monadic second-order logic in practice
The model checker spin.
Automatic verification of pointer programs using monadic second-order logic
A case study in automated verification based on trace abstractions.
Automated logical verification based on trace ab- straction
Formal design constraints.
BDD algorithms and cache misses.
Three approaches to type struc- ture
--TR

--CTR
Anders Mller , Michael I. Schwartzbach, The pointer assertion logic engine, ACM SIGPLAN Notices, v.36 n.5, p.221-231, May 2001
Marjan Mernik , Jan Heering , Anthony M. Sloane, When and how to develop domain-specific languages, ACM Computing Surveys (CSUR), v.37 n.4, p.316-344, December 2005
trees;regular sets;strings;logic;domain-specific languages