Search: onr:"swepub:oai:research.chalmers.se:89bffef6-9ad7-4256-84dd-80225d6a7719" >
Automatic Validatio...
Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics
-
- Ahrendt, Wolfgang, 1967 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Roth, Andreas (author)
- Karlsruher Institut für Technologie (KIT),Karlsruhe Institute of Technology (KIT)
-
- Sasse, Ralf (author)
- University of Illinois
-
(creator_code:org_t)
- ISBN 354030553X
- Berlin, Heidelberg : Springer Berlin Heidelberg, 2005
- 2005
- English.
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 354030553X ; LNCS 3835, s. 412 - 426
- Related links:
-
http://dx.doi.org/10...
-
show more...
-
https://doi.org/10.1...
-
https://research.cha...
-
show less...
Table of contents
Abstract
Subject headings
Close
No table of content available
- This paper presents a methodology for automatically validating program transformation rules that are part of a calculus for Java source code verification. We target the Java Dynamic Logic calculus which is implemented in the interactive prover of the KeY system. As a basis for validation, we take an existing SOS style rewriting logic semantics for Java, formalized in the input language of the Maude system. That semantics is `lifted' to cope with schematic programs like the ones appearing in program transformation rules. The rewriting theory is further extended to generate valid initial states for involved program fragments, and to check the final states for equivalence. The result is used in frequent validation runs over the relevant fragment of the calculus in the KeY system.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Keyword
- program logic
- programming language semantics
- Java
Publication and Content Type
- kon (subject category)
- ref (subject category)
Find in a library
To the university's database