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 /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Meyer, Bertrand (Επιμελητής έκδοσης), Woodcock, Jim (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2008.
• Σειρά: Lecture Notes in Computer Science, 4171
• Θέματα: Computer science.; Computer programming.; Software engineering.; Programming languages (Electronic computers).; Operating systems (Computers).; Computer logic.; Artificial intelligence.; Computer Science.; Programming Techniques.; Software Engineering.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.; Operating Systems.; Artificial Intelligence (incl. Robotics).

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 speci...

Πίνακας περιεχομένων:

• 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.