Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Sele (Paperback)

Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project.- Verification Tools.- Towards a Worldwide Verification Technology.- It Is Time to Mechanize Programming Language Metatheory.- Methods and Tools for Formal Software Engineering.- Guaranteeing Correctness.- The Verified Software Challenge: A Call for a Holistic Approach to Reliability.- A Mini Challenge: Build a Verifiable Filesystem.- A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets.- Some Interdisciplinary Observations about Getting the “Right” Specification.- Software Engineering Aspects.- Software Verification and Software Engineering a Practitioner’s Perspective.- Decomposing Verification Around End-User Features.- Verifying Object-Oriented Programming.- Automatic Verification of Strongly Dynamic Software Systems.- Reasoning about Object Structures Using Ownership.- Modular Reasoning in Object-Oriented Programming.- Scalable Specification and Reasoning: Challenges for Program Logic.- Programming Language and Methodology Aspects.- Lessons from the JML Project.- The Spec# Programming System: Challenges and Directions.- Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification.- Components.- Automated Test Generation and Verified Software.- Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.- Generating Programs Plus Proofs by Refinement.- Static Analysis.- The Verification Grand Challenge and Abstract Interpretation.- WYSINWYX: What You See Is Not What You eXecute.- Implications of a Data Structure Consistency Checking System.- Towards the Integration of Symbolic and Numerical Static Analysis.- Design, Analysis and Tools.- Reliable Software Systems Design: Defect Prevention, Detection, and Containment.- Trends and Challenges in Algorithmic Software Verification.- Model Checking: Back and Forth between Hardware and Software.- Computational Logical Frameworks and Generic Program Analysis Technologies.- Formal Techniques.- A Mechanized Program Verifier.- Verifying Design with Proof Scores.- Integrating Theories and Techniques for Program Modelling, Design and Verification.- Eiffel as a Framework for Verification.- Position Papers.- Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges.- Verified Software: The Real Grand Challenge.- Linking the Meaning of Programs to What the Compiler Can Verify.- Scalable Software Model Checking Using Design for Verification.- Model-Checking Software Using Precise Abstractions.- Toasters, Seat Belts, and Inferring Program Properties.- On the Formal Development of Safety-Critical Software.- Verify Your Runs.- Specified Blocks.- A Case for Specification Validation.- Some Verification Issues at NASA Goddard Space Flight Center.- Performance Validation on Multicore Mobile Devices.- Tool Integration for Reasoned Programming.- Decision Procedures for the Grand Challenge.- The Challenge of Hardware-Software Co-verification.- From the How to the What.- An Overview of Separation Logic.- A Perspective on Program Verification.- Meta-Logical Frameworks and Formal Digital Libraries.- Languages, Ambiguity, and Verification.- The Importance of Non-theorems and Counterexamples in Program Verification.- Regression Verification - A Practical Way to Verify Programs.- Programming with Proofs: Language-Based Approaches to Totally Correct Software.- The Role of Model-Based Testing.- Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification.- Program Verification by Using DISCOVERER.- Constraint Solving and Symbolic Execution.