XMECHTowards Scalable Software Verification
Stc
ComputingScienceColloquium
Date: June 19
Time: 11am
Room: C008 AARD
* our usual room!! *
Speaker: Ade Azurat
Title: xMECH: towards scalable software verification.
Abstract
We will present the latest development of xMech verification
tools. The main two characterizing features of xMech would be its
scalability by classifying several language modules that can
be extended on top of each other; and
modularity by providing a collection of automated reduction
modules (we like to call them mechboxes),
each deals with a specific aspect of a specification. The
building of mechboxes is an interesting problem of its own.
From our experience, mechboxes tend to form loosely
independent groups, but within a group they have tighter
interdependency which is often delicate,
and thus error prone when programmed in the traditional
way, as it requires the programming of interwoven recursive
computations. For this reason xMech is developed using an
attribute grammar tool, which allows recursion weaving to
be programmed abstractly and modularly.
