|
|
Departmental Colloquia
(2004-2005)
October 22, 2004
3-4:00, LH102
The logic-automata connection and applications
Nils Klarlund
Clairgrove, LLC
Abstract:
This talk is a survey of the Mona tool and its applications. Mona
is a tool for building powerful specification languages that
"compile into" automata. Driven by sometimes very large formulas
in Monadic Second-order Logic, the Mona tool carries out
intensive automata-theoretic calculations. Problems in
high-level notations in a variety of application areas can be
crunched by Mona after a suitable translation. We will mention
- assertion languages for pointers and automated reasoning
- protocol specification languages
- languages for generation of fast parsers enforcing tree constraints
Mona is used to generate automata from these languages, and these
automata can be used both at runtime and to do static analysis at
compile time. I will discuss the BDD-representation of automata
and the three-valued logic behind a practical engine for automata
calculations expressed by formulas in Mona's internal languages.
The Mona tool is in use in research applications ranging from
hardware verification to linguistics.
Biography:
Nils Klarlund has worked in a variety of areas in computer science.
His current focus on software quality improvement is shaped through
extensive industrial experience with XML, verification, and telephony
applications. Earlier, Nils Klarlund has contributed to automata-based
symbolic reasoning, shape analysis in programming languages, and to
the understanding of infinite computations. Nils Klarlund is also an
inventor of devices and speech recognition user interfaces. They
comprise the Q10 keyboard (RIM SureType), scroll wheels on keyboards,
and the ShortStep and ShortTalk input technologies recently donated to
Carnegie Mellon University.
|
