Verified Software: Theories, Tools, Experiments [[electronic resource] ] : First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions / / edited by Bertrand Meyer, Jim Woodcock

• Record Nr.: UNISA996465307003316
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008
• ISBN: 3-540-69149-9
• Edizione: [1st ed. 2008.]
• Descrizione fisica: 1 online resource (XXIII, 546 p.)
• Collana: Programming and Software Engineering ; ; 4171
• Disciplina: 005.11
• Soggetti: Computer programming; Software engineering; Computer logic; Programming languages (Electronic computers); Operating systems (Computers); Artificial intelligence; Programming Techniques; Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Operating Systems; Artificial Intelligence
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: 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.
• Sommario/riassunto: 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.