Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Conference Paper

LISA: A Specification Language Based on WS2S


Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Abdelwaheb, A., Basin, D. A., & Podelski, A. (1998). LISA: A Specification Language Based on WS2S. In M. Nielsen, & W. Thomas (Eds.), Proceedings of the 11th International Workshop on Computer Science Logic (CSL-97) (pp. 18-34). Berlin, Germany: Springer.

Cite as:
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.