@InProceedings{ ayari.ea:lisa:1997, 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)}, year = 1997, series = {LNCS}, number = 1414, pages = {18 -- 34}, publisher = {Springer-Verlag}, editor = {Mogens Neilsen and Wolfgang Thomas}, language = {USenglish}, ps = {papers/1997/lisa.ps.gz}, 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.} }