Tony Hoare, Jay Misra (auth.), Bertrand Meyer, Jim Woodcock (eds.)3540691472, 9783540691471
This state-of-the-art survey is an outcome of the first IFIP TC 2/WG 2.3 working conference on Verified Software: Theories, Tools, Experiments, VSTTE 2005, held in Zurich, Switzerland, in October 2005. This was a historic event gathering many top international experts on systematic methods for specifying, building and verifying high-quality software.
The book includes 32 revised full papers and 27 revised position papers, preceded by a general introduction to the area, which also presents the vision of a grand challenge project: the “verifying compiler”. Most contributions are followed by a transcription of the vivid discussion that ensued between the author and the audience. The papers have been organized in topical sections on verification tools, guaranteeing correctness, software engineering aspects, verifying object-oriented programming, programming language and methodology aspects, components, static analysis, design, analysis and tools, as well as formal techniques.
Table of contents :
Front Matter….Pages –
Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project….Pages 1-18
Towards a Worldwide Verification Technology….Pages 19-25
It Is Time to Mechanize Programming Language Metatheory….Pages 26-30
Methods and Tools for Formal Software Engineering….Pages 31-41
The Verified Software Challenge: A Call for a Holistic Approach to Reliability….Pages 42-48
A Mini Challenge: Build a Verifiable Filesystem….Pages 49-56
A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets….Pages 57-63
Some Interdisciplinary Observations about Getting the “Right” Specification….Pages 64-69
Software Verification and Software Engineering a Practitioner’s Perspective….Pages 70-73
Decomposing Verification Around End-User Features….Pages 74-81
Automatic Verification of Strongly Dynamic Software Systems….Pages 82-92
Reasoning about Object Structures Using Ownership….Pages 93-104
Modular Reasoning in Object-Oriented Programming….Pages 105-115
Scalable Specification and Reasoning: Challenges for Program Logic….Pages 116-133
Lessons from the JML Project….Pages 134-143
The Spec# Programming System: Challenges and Directions….Pages 144-152
Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification….Pages 153-160
Automated Test Generation and Verified Software….Pages 161-172
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler….Pages 173-181
Generating Programs Plus Proofs by Refinement….Pages 182-188
The Verification Grand Challenge and Abstract Interpretation….Pages 189-201
WYSINWYX: What You See Is Not What You eXecute….Pages 202-213
Implications of a Data Structure Consistency Checking System….Pages 214-226
Towards the Integration of Symbolic and Numerical Static Analysis….Pages 227-236
Reliable Software Systems Design: Defect Prevention, Detection, and Containment….Pages 237-244
Trends and Challenges in Algorithmic Software Verification….Pages 245-250
Model Checking: Back and Forth between Hardware and Software….Pages 251-255
Computational Logical Frameworks and Generic Program Analysis Technologies….Pages 256-267
A Mechanized Program Verifier….Pages 268-276
Verifying Design with Proof Scores….Pages 277-290
Integrating Theories and Techniques for Program Modelling, Design and Verification….Pages 291-300
Eiffel as a Framework for Verification….Pages 301-307
Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges….Pages 308-317
Verified Software: The Real Grand Challenge….Pages 318-324
Linking the Meaning of Programs to What the Compiler Can Verify….Pages 325-336
Scalable Software Model Checking Using Design for Verification….Pages 337-346
Model-Checking Software Using Precise Abstractions….Pages 347-353
Toasters, Seat Belts, and Inferring Program Properties….Pages 354-361
On the Formal Development of Safety-Critical Software….Pages 362-373
Verify Your Runs….Pages 374-383
Specified Blocks….Pages 384-391
A Case for Specification Validation….Pages 392-402
Some Verification Issues at NASA Goddard Space Flight Center….Pages 403-412
Performance Validation on Multicore Mobile Devices….Pages 413-421
Tool Integration for Reasoned Programming….Pages 422-427
Decision Procedures for the Grand Challenge….Pages 428-437
The Challenge of Hardware-Software Co-verification….Pages 438-447
From the How to the What….Pages 448-459
An Overview of Separation Logic….Pages 460-469
A Perspective on Program Verification….Pages 470-477
Meta-Logical Frameworks and Formal Digital Libraries….Pages 478-485
Languages, Ambiguity, and Verification….Pages 486-490
The Importance of Non-theorems and Counterexamples in Program Verification….Pages 491-495
Regression Verification – A Practical Way to Verify Programs….Pages 496-501
Programming with Proofs: Language-Based Approaches to Totally Correct Software….Pages 502-509
The Role of Model-Based Testing….Pages 510-517
Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification….Pages 518-527
Program Verification by Using DISCOVERER….Pages 528-538
Constraint Solving and Symbolic Execution….Pages 539-544
Back Matter….Pages –
Reviews
There are no reviews yet.