English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. View item / 
  2. Item Summary

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Conference Paper

LISA: A Specification Language Based on WS2S

MPS-Authors
/persons/resource/persons44075

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

/persons/resource/persons45201

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

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

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: https://hdl.handle.net/11858/00-001M-0000-000F-384F-8
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.