MONA 1.x: New techniques for WS1S and WS2S

Jacob Elgaard¹,
Nils Klarlund² &
Anders Møller³

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1427))

Included in the following conference series:

International Conference on Computer Aided Verification

325 Accesses

Abstract

In this note, we present the first version of the MONA tool to be released in its entirety. The tool now offers decision procedures for both WS1S and WS2S and a completely rewritten front-end. Here, we present some of our techniques, which make calculations couched in WS1S run up to five times faster than with our pre-release tool based on M2L(Str). This suggests that WS1S—with its better semantic properties—is preferable to M2L(Str).

Download to read the full chapter text

Chapter PDF

References

M. Biehl, N. Klarlund, and T. Rauhe. Mona: decidable arithmetic in practice (short contribution). In Formal Techniques in Real-Time and Fault-Tolerant Systems, 4th International Symposium, LNCS 1135 Springer Verlag, 1996.
Google Scholar
J. Glenn and W. Gasarch. Implementing WS1S via finite automata. In Automata Implementation, WIA '96, Proceedings, volume 1260 of LNCS, 1997.
Google Scholar
J.L. Jensen, M.E. Jørgensen, N. Klarlund, and M.I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In SIGPLAN '97 Conference on Programming Language Design and Implementation pages 226–234. SIGPLAN, 1997.
Google Scholar
P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. Mosel: a flexible toolset for Monadic Second-order Logic. In Computer Aided Verification, CAV '97, Proceedings, LNCS 1217, 1997.
Google Scholar
N. Klarlund. Mona & Fido: the logic-automaton connection in practice. In CSL '97 Proceedings, 1998. To appear in LNCS.
Google Scholar
F. Morawietz and T. Cornell. On the recognizability of relations over a tree definable in a monadic second order tree description language. Technical Report SFB 340, Seminar für Sprachwissenschaft Eberhard-Universität Tübingen, 1997.
Google Scholar

Download references

Author information

Authors and Affiliations

BRICS, University of Aarhus, Germany
Jacob Elgaard
AT&T Labs-Research, Germany
Nils Klarlund
BRICS, University of Aarhus, Germany
Anders Møller

Authors

Jacob Elgaard
View author publications
You can also search for this author in PubMed Google Scholar
Nils Klarlund
View author publications
You can also search for this author in PubMed Google Scholar
Anders Møller
View author publications
You can also search for this author in PubMed Google Scholar

Editor information

Alan J. Hu Moshe Y. Vardi

Rights and permissions

Reprints and permissions

Copyright information

About this paper

Cite this paper

Elgaard, J., Klarlund, N., Møller, A. (1998). MONA 1.x: New techniques for WS1S and WS2S. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028773

Download citation

DOI: https://doi.org/10.1007/BFb0028773
Published: 18 June 2005
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive

Publish with us

Policies and ethics