@INPROCEEDINGS{csl97,
AUTHOR        = {Abdelwaheb Ayari and David Basin and Andreas Podelski},
TITLE         = {LISA: A Specification Language Based on WS2S},
BOOKTITLE     = {11th International Conference of the European Association for Computer Science Logic (CSL '97)},
EDITORS       = {Mogens Neilsen and Wolfgang Thomas},
YEAR          = {1997},
PAGES         = {18 -- 34},
PUBLISHER = "Springer-Verlag",
SERIES = {LNCS},
VOLUME = "1414",
ABSTRACT = {
We integrate two concepts from programming languages into a
specification language based on WS2S, namely high-level data structures
such as records and recursively-defined datatypes (WS2S is the weak
second-order monadic logic of two successors).  Our integration is based
on a new logic whose variables range over record-like trees and an
algorithm for translating datatypes into tree automata.  We have
implemented Lisa, a prototype system based on these ideas, which, when
coupled with a decision procedure for WS2S like the Mona system, results
in a verification tool that supports both high-level specifications and
complexity estimations for the running time of the decision procedure.
}
}