Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions

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 -