Sökning: onr:"swepub:oai:research.chalmers.se:811550c1-9390-46aa-8588-e0e602071ed2" >
Verification of Obj...
Verification of Object-Oriented Software. The KeY Approach
-
Beckert, Bernhard (författare)
-
- Hähnle, Reiner, 1962 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
Schmitt, Peter (författare)
-
(creator_code:org_t)
- ISBN 9783540689775
- 2006
- Engelska.
- Relaterad länk:
-
https://research.cha...
Innehållsförteckning
Abstract
Recensioner
Ämnesord
Stäng
No table of content available
- The ultimate goal of program verification is not the theory behind the tools or the tools themselves, but the application of the theory and tools in the software engineering process. Our society relies on the correctness of a vast and growing amount of software. Improving the software engineering process is an important, long-term goal with many steps. Two of those steps are the KeY tool and this KeY book.The material is presented on an advanced level suitable for graduate courses and, of course, active researchers with an interest in verification. The underlying verification paradigm is deductive verification in an expressive program logic. The logic used for reasoning about programs is not a minimalist version suitable for theoretical investigations, but an industrial-strength version. The first-order part is equipped with a type system for modelling of object hierarchies, with underspecification, and with various built-in theories. The program logic covers full Java Card (plus a bit more such as multi-dimensional arrays, characters, and long integers). A lot of emphasis is thereby put on specification, including two widely-used object-oriented specification languages (OCL and JML) and even an interface to natural language generation. The generation of proof obligations from specified code is discussed at length. The book is rounded off by two substantial case studies that are included and presented in detail.
No review available
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Software Engineering (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- proof obligations
- OCL
- formal reasoning
- Java Card
- program verification
- specification languages
- natural language generation
- JML
- deductive verification
- Java
- theorem proving
- software security
- logic reasoning
- formal methods
- systems modeling
- AI logics
- object-oriented software
Publikations- och innehållstyp
- bok (ämneskategori)
- vet (ämneskategori)
Hitta via bibliotek
Till lärosätets databas