The MONA Project

• Home
• Download
• Demo
• Publications

Manual

• MONA Version 1.4 User Manual
  Nils Klarlund and Anders Møller
  BRICS Notes Series
  
  This manual describes all features of MONA Version 1.4 through a number of examples. Both the classical decision procedure for the WS1S logic and the MONA approach are explained. Also the WS2S logic and the MONA concept of guided tree automata are presented.
  [ abstract | PDF | BibTeX ]

Concepts

• Mona: Monadic Second-Order Logic in Practice
  Jesper G. Henriksen, Jakob Jensen, Michael Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm
  TACAS '95
  
  Our first paper on the implementation of M2L on finite strings. We discuss data structures, algorithms, and an application to verification of safety and liveness properties of a parameterized distributed system.
  [ abstract | PDF | BibTeX ]
• Mona: Decidable Arithmetic in Practice
  Morten Biehl, Nils Klarlund, and Theis Rauhe
  FTSRTS '96 (short demo contribution)
  
  The new MONA semantics based on arithmetic and WS1S. We discuss algorithms and give an example showing that a recently proposed representation of queues is subsumed by MONA.
  [ abstract | PDF | BibTeX ]
• Mona & Fido: The Logic-Automaton Connection in Practice
  Nils Klarlund
  CSL '97 (invited paper)
  
  A survey paper on BDDs, BDD-represented automata, WS1S and WS2S, practical techniques for decision procedures, and applications of automaton-based symbolic reasoning.
  [ abstract | PDF | BibTeX ]
• Mona 1.x: New Techniques for WS1S and WS2S
  Jacob Elgaard, Nils Klarlund, and Anders Møller
  CAV '98 (tool paper)
  
  The first version of MONA to be released in its entirety. We argue that WS1S is preferable to M2L(Str), and we explain techniques for speeding up the decision procedure.
  [ abstract | PDF | BibTeX ]
• A Domain-Specific Language for Regular Sets of Strings and Trees
  Nils Klarlund and Michael I. Schwartzbach
  IEEE TSE (extended version of DSL '97)
  
  Introduction of Fido, a high-level language for expressing regularity.
  [ abstract | PDF | BibTeX ]
• A Theory of Restrictions for Logics and Automata
  Nils Klarlund
  CAV '99
  
  The mathematical framework MONA uses for handling first-order variables.
  [ abstract | PDF | BibTeX ]

Applications

• Automated Logical Verification Based on Trace Abstractions
  Nils Klarlund, Mogens Nielsen, and Kim Sunesen
  PODC '96
  
  A behavioral approach to the comparison of distributed systems. We formulate proof principles that can be expressed in M2L and that allow component-wise verification.
  [ abstract | PDF | BibTeX ]
• A Case Study in Verification Based on Trace Abstractions
  Nils Klarlund, Mogens Nielsen, and Kim Sunesen
  LNCS 1169
  
  A detailed account of the behavioral modeling of reactive systems in Fido according to the method in "Automated Logical Verification Based on Trace Abstractions".
  [ abstract | PDF | BibTeX ]
• Formal Design Constraints
  Nils Klarlund, Jari Koistinen, and Michael I. Schwartzbach
  OOPSLA '96
  
  Common design constraints on software architectures are formalized in a version of Fido, which enables automatic generation of programming environment tools.
  [ abstract | PDF | BibTeX ]
• Automatic Verification of Pointer Programs using Monadic Second-order Logic
  Jacob L. Jensen, Michael E. Jørgensen, Nils Klarlund, and Michael I. Schwartzbach
  PLDI '97
  
  A decidable Hoare logic is formulated for a fragment of Pascal that includes pointers and while loops. Using a decision procedure, we can answer detailed questions about pointer usage automatically.
  [ abstract | PDF | BibTeX ]
• Automata Based Symbolic Reasoning in Hardware Verification
  David A. Basin and Nils Klarlund
  Journal of Formal Methods in System Design, 1998 (extended version in CAV '95)
  
  Hardware verification based on formulating circuits and their specifications in M2L. We use MONA to verify parameterized circuits without induction, and we explain why it works.
  [ abstract | PDF | BibTeX ]
• Distributed Safety Controllers for Web Services
  Anders Sandholm and Michael I. Schwartzbach
  FASE '98
  
  Monadic second-order logic on finite strings is used to specify synchronization constraints for synthesis of safety controllers for interactive web services.
  [ abstract | PDF | BibTeX ]
• YakYak: Parsing with Logical Side Constraints
  Niels Damgaard, Nils Klarlund, and Michael I. Schwartzbach
  DLT '99
  
  About extending Yacc with first-order logic for specifying constraints that are regular tree languages.
  [ abstract | PDF | BibTeX ]
• Compile-Time Debugging of C Programs Working on Trees
  Jacob Elgaard, Anders Møller, and Michael I. Schwartzbach
  ESOP '00
  
  A technique for automatically verifying the safety of simple C programs working on tree-shaped data structures.
  [ abstract | PDF | BibTeX ]
• The Pointer Assertion Logic Engine
  Anders Møller and Michael I. Schwartzbach
  PLDI '01
  
  The program verification technique from "Compile-Time Debugging of C Programs Working on Trees" is extended to handle the whole class of data structures known as graph types.
  [ abstract | PDF | BibTeX ]

Algorithms

• BDD Algorithms and Cache Misses
  Nils Klarlund and Theis Rauhe
  BRICS Report Series
  
  Techniques for speeding up BDD operations five times compared to a standard package. We discuss how random memory access can be reduced by rethinking data structures for BDD algorithms.
  [ abstract | PDF | BibTeX ]
• Algorithms for Guided Tree Automata
  Morten Biehl, Nils Klarlund, and Theis Rauhe
  WIA '96
  
  Techniques for combatting state space explosions in tree automata.
  [ abstract | PDF | BibTeX ]
• An n log n Algorithm for Online BDD Refinement
  Nils Klarlund
  Journal of Algorithms, 1999 (extended version of CAV '97)
  
  A minimization construction for BDD-represented automata. The path compression of BDDs makes Hopcroft's algorithm unworkable, but some rather involved techniques make an n log n algorithm possible.
  [ abstract | PDF | BibTeX ]
• MONA Implementation Secrets
  Nils Klarlund, Anders Møller, and Michael I. Schwartzbach
  International Journal of Foundations of Computer Science, 2002 (extended version of CIAA '00)
  
  An overview of the techniques used in the MONA tool. The respective effects of the techniques are quantified by experiments on a number of benchmarks.
  [ abstract | PDF | BibTeX ]

Other

• Graph Types
  Nils Klarlund and Michael I. Schwartzbach
  POPL '93
  
  The notion of a recursive data structure is generalized so that common shapes, such as doubly-linked lists or threaded trees, can be expressed concisely.
  [ abstract | PDF | BibTeX ]
• Graphs and Decidable Transductions Based on Edge Constraints
  Nils Klarlund and Michael I. Schwartzbach
  CAAP '94
  
  Not even edNCE, the most general known notion of context-free graph grammar, is suited for the specification of some common data structures. To overcome this problem, monadic second-order logic is combined with our notion of edge constraints as a new means of specifying a large class of graph families.
  [ abstract | PDF | BibTeX ]