Home News About Us Contact Contributors Disclaimer Privacy Policy Help FAQ

Home
Search
Quick Search
Advanced
Fulltext
Browse
Collections
Persons
My eDoc
Session History
Login
Name:
Password:
Documentation
Help
Support Wiki
Direct access to
document ID:


          Institute: MPI für Informatik     Collection: Programming Logics Group     Display Documents



ID: 519683.0, MPI für Informatik / Programming Logics Group
LISA: A Specification Language Based on WS2S
Authors:Abdelwaheb, Ayari; Basin, David A.; Podelski, Andreas
Language:English
Publisher:Springer
Place of Publication:Berlin, Germany
Date of Publication (YYYY-MM-DD):1998
Title of Proceedings:Proceedings of the 11th International Workshop on Computer Science Logic (CSL-97)
Start Page:18
End Page:34
Title of Series:Lecture Notes in Computer Science
Place of Conference/Meeting:Aarhus, Denmark
(Start) Date of Conference/Meeting
 (YYYY-MM-DD):
1998
Audience:Experts Only
Intended Educational Use:No
Abstract / Description: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.
Last Change of the Resource (YYYY-MM-DD):2010-03-12
External Publication Status:published
Document Type:Conference-Paper
Communicated by:Andreas Podelski
Affiliations:MPI für Informatik/Programming Logics Group
Identifiers:LOCALID:C1256104005ECAFC-C031722D45D00184412566FD005946CA-...
ISBN:3-540-64570-5
The scope and number of records on eDoc is subject to the collection policies defined by each institute - see "info" button in the collection browse view.