The MONA Project

[Massimo Dentico]

The MONA Project homepage:
- http://www.brics.dk/mona/

Excerpt from “Introduction to MONA”:
- http://www.brics.dk/mona/introduction.html

==================================================================
                       Introduction to MONA

In  practice,  the fundamental concept of regularity (finite-state
acceptance  of strings) is often exceedingly hard to express.  For
example,  regular expressions (as used in scanners,  text  editors
and  UNIX  shell  programming) are elegant when expressing  simple
patterns,  but  often  unreadable  for  patterns  of  even  modest
complexity.

For  trees, it is even harder to express regular sets,  since  the
only  means  used  in  practice are  tedious  programming  of  the
information  flow up and down the tree (in terms of attributes  or
recursive procedures).

The  aim  of the MONA project is to devise new practical means  of
describing  finite-state systems in formal logics  that  naturally
capture informal requirements.

We  are pursuing the use of the massive combinatorial calculations
behind   these   logics  in  verification,  software  engineering,
programming languages, and theorem proving.

                           What is MONA?

MONA  is  a  logic-based  programming language  and  a  tool  that
translates programs, that is, formulas, to finite-state  automata.
The  formulas may express search patterns, temporal properties  of
reactive  systems, parse tree constraints, etc. MONA analyses  the
automaton resulting from the compilation, and it either prints out
"valid" or a counter-example to the statement of the program.

MONA  implements  decision procedures for  the  Weak  Second-order
Theory of One or Two succesors. The theory of one successor, known
as  WS1S,  is a fragment of arithmetic augmented with second-order
quantification  over  finite sets of natural numbers.  Its  first-
order  terms  denote  just  natural numbers.  The  theory  has  no
addition, since that would make it undecidable, but it has a unary
operation +1, known as the successor function. Since the theory is
a monadic second-order logic, we call our tool MONA.

[...]
==================================================================

Here papers on MONA:
- http://www.brics.dk/mona/papers.html

In particular these two on program verification:

“Automatic Verification of Pointer Programs using Monadic  Second-
order Logic”

“Compile-Time Debugging of C Programs Working on Trees”


-- 
Massimo Dentico