The KeY platform for verification and analysis of Java programs

被引：32

作者：

Ahrendt, Wolfgang ^{[1
]}

Beckert, Bernhard ^{[2
]}

Bruns, Daniel ^{[2
]}

Bubel, Richard ^{[3
]}

Gladisch, Christoph ^{[2
]}

Grebing, Sarah ^{[2
]}

Hähnle, Reiner ^{[3
]}

Hentschel, Martin ^{[3
]}

Herda, Mihai ^{[2
]}

Klebanov, Vladimir ^{[2
]}

Mostowski, Wojciech ^{[4
]}

Scheben, Christoph ^{[2
]}

Schmitt, Peter H. ^{[2
]}

Ulbrich, Mattias ^{[2
]}

机构：

[1] Chalmers University of Technology, Gothenburg, Sweden

[2] Karlsruhe Institute of Technology, Karlsruhe, Germany

[3] Technische Universität Darmstadt, Darmstadt, Germany

[4] University of Twente, Enschede, Netherlands

来源：

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8471卷

基金：

欧洲研究理事会;

关键词：

!text type='Java']Java[!/text] programming language - Program debugging - Modular construction - Software testing - Modeling languages;

D O I：

10.1007/978-3-319-12154-3_4

中图分类号：

学科分类号：

摘要：

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. © Springer International Publishing Switzerland 2014.

引用

页码：55 / 71