Paper Info
Title
Structural Embeddings: Mechanization with Method
Abstract
The most powerful tools for analysis of formal specifications are general-purpose theorem provers and model checkers, but these tools provide scant methodological support. Conversely, those approaches that do provide a well-developed method generally have less powerful automation. It is natural, therefore, to try to combine the better-developed methods with the more powerful general-purpose tools. An obstacle is that the methods and the tools often employ very different logics. We argue that methods are separable from their logics and are largely concerned with the structure and organization of specifications. We propose a technique called structural embedding that allows the structural elements of a method to be supported by a general-purpose tool, while substituting the logic of the tool for that of the method. We have found this technique quite effective and we provide some examples of its application. We also suggest how general-purpose systems could be restructured to support this activity better.
Year
DOI
Venue
1999
10.1007/3-540-48119-2_26
World Congress on Formal Methods
Keywords
Field
DocType
scant methodological support,general-purpose system,general-purpose theorem provers,powerful general-purpose tool,better-developed method,powerful tool,structural embeddings,structural element,well-developed method,powerful automation,general-purpose tool,coding,systems analysis,software engineering,high level languages,theorems,logic,embedding,mechanization,automation,semantics
Programming language,Computer science,Automated theorem proving,Systems analysis,Automation,Theoretical computer science,Formal specification,Formal methods,Abstract machine,Software development,Formal verification
Conference
Volume
ISSN
ISBN
1708
0302-9743
3-540-66587-0
Citations 
PageRank 
References 
8
0.64
25
Authors
2
Name
Order
Citations
PageRank
César Muñoz1495.83
John Rushby22459235.69