LISA: A Specification Language Based on WS2S

Abdelwaheb, Ayari; Basin, David A.; Podelski, Andreas

Datensatz

DATENSATZ AKTIONENEXPORT

Zur Ablage hinzufügen

Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben

Konferenzbeitrag

LISA: A Specification Language Based on WS2S

MPG-Autoren

/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;

Externe Ressourcen

Es sind keine externen Ressourcen hinterlegt

Volltexte (beschränkter Zugriff)

Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.

Volltexte (frei zugänglich)

Es sind keine frei zugänglichen Volltexte in PuRe verfügbar

Ergänzendes Material (frei zugänglich)

Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Zitation

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.

Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-384F-8

Zusammenfassung

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.