CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

The KeY platform for verification and analysis of java programs

Wolfgang Ahrendt (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; B. Beckert ; D. Bruns ; R. Bubel ; C.D. Gladisch ; S. Grebing ; R. Hähnle ; M. Hentschel ; M. Herda ; V. Klebanov ; W.I. Mostowski ; C. Scheben ; P.H. Schmitt ; M. Ulbrich
Lecture notes in Computer Science: 6th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2014; Vienna; Austria; 17 July 2014 through 18 July 2014 8471, p. 55-71. (2014)
[Konferensbidrag, refereegranskat]

The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flowsecurity, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.

Nyckelord: Java program; Verification and analysis

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-12-22. Senast ändrad 2015-04-29.
CPL Pubid: 208839


Läs direkt!

Länk till annan sajt (kan kräva inloggning)