| Introduction |
| Verified Software: Theories, Tools, Experiments: Vision of a Grand Challenge Project / Tony Hoare ; Jay Misra |
| Verification Tools |
| Towards a Worldwide Verification Technology / Wolfgang Paul |
| It Is Time to Mechanize Programming Language Metatheory / Benjamin C. Pierce ; Peter Sewell ; Stephanie Weirich ; Steve Zdancewic |
| Methods and Tools for Formal Software Engineering / Zhiming Liu ; R. Venkatesh |
| Guaranteeing Correctness |
| The Verified Software Challenge: A Call for a Holistic Approach to Reliability / Thomas Ball |
| A Mini Challenge: Build a Verifiable Filesystem / Rajeev Joshi ; Gerard J. Holzmann |
| A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets / Alessandro Coglio ; Cordell Green |
| Some Interdisciplinary Observations about Getting the "Right" Specification / Cliff B. Jones |
| Software Engineering Aspects |
| Software Verification and Software Engineering a Practitioner's Perspective / Anthony Hall |
| Decomposing Verification Around End-User Features / Kathi Fisler ; Shriram Krishnamurthi |
| Verifying Object-Oriented Programming |
| Automatic Verification of Strongly Dynamic Software Systems / N. Dor ; J. Field ; D. Gopan ; T. Lev-Ami ; A. Loginov ; R. Manevich ; G. Ramalingam ; T. Reps ; N. Rinetzky ; M. Sagiv ; R. Wilhelm ; E. Yahav ; G. Yorsh |
| Reasoning about Object Structures Using Ownership / Peter Muller |
| Modular Reasoning in Object-Oriented Programming / David A. Naumann |
| Scalable Specification and Reasoning: Challenges for Program Logic / Peter W. O'Hearn |
| Programming Language and Methodology Aspects |
| Lessons from the JML Project / Gary T. Leavens ; Curtis Clifton |
| The Spec# Programming System: Challenges and Directions / Mike Barnett ; Robert DeLine ; Manuel Fahndrich ; Bart Jacobs ; K. Rustan M. Leino ; Wolfram Schulte ; Herman Venter |
| Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification / Joseph R. Kiniry ; Patrice Chalin ; Clement Hurlin |
| Components |
| Automated Test Generation and Verified Software / John Rushby |
| Dependent Types, Theorem Proving, and Applications for a Verifying Compiler / Yves Bertot ; Laurent Thery |
| Generating Programs Plus Proofs by Refinement / Douglas R. Smith |
| Static Analysis |
| The Verification Grand Challenge and Abstract Interpretation / Patrick Cousot |
| WYSINWYX: What You See Is Not What You eXecute / G. Balakrishnan ; D. Melski ; T. Teitelbaum |
| Implications of a Data Structure Consistency Checking System / Viktor Kuncak ; Patrick Lam ; Karen Zee ; Martin Rinard |
| Towards the Integration of Symbolic and Numerical Static Analysis / Arnaud Venet |
| Design, Analysis and Tools |
| Reliable Software Systems Design: Defect Prevention, Detection, and Containment |
| Trends and Challenges in Algorithmic Software Verification / Rajeev Alur |
| Model Checking: Back and Forth between Hardware and Software / Edmund Clarke ; Anubhav Gupta ; Himanshu Jain ; Helmut Veith |
| Computational Logical Frameworks and Generic Program Analysis Technologies / Jose Meseguer ; Grigore Rosu |
| Formal Techniques |
| A Mechanized Program Verifier / J. Strother Moore |
| Verifying Design with Proof Scores / Kokichi Futatsugi ; Joseph A. Goguen ; Kazuhiro Ogata |
| Integrating Theories and Techniques for Program Modelling, Design and Verification: Positioning the Research at UNU-IIST in Collaborative Research on the Verified Software Challenge / Bernard K. Aichernig ; He Jifeng ; Mike Reed |
| Eiffel as a Framework for Verification / Bertrand Meyer |
| Position Papers |
| Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges / Myla Archer |
| Verified Software: The Real Grand Challenge / Ramesh Bharadwaj |
| Linking the Meaning of Programs to What the Compiler Can Verify / Egon Borger |
| Scalable Software Model Checking Using Design for Verification / Tevfik Bultan ; Aysu Betin-Can |
| Model-Checking Software Using Precise Abstractions / Marsha Chechik ; Arie Gurfinkel |
| Toasters, Seat Belts, and Inferring Program Properties / David Evans |
| On the Formal Development of Safety-Critical Software / Andy Galloway ; Frantz Iwu ; John McDermid ; Ian Toyn |
| Verify Your Runs / Klaus Havelund ; Allen Goldberg |
| Specified Blocks / Eric C.R. Hehner |
| A Case for Specification Validation / Mats P.E. Heimdahl |
| Some Verification Issues at NASA Goddard Space Flight Center / Michael G. Hinchey ; James L. Rash ; Christopher A. Rouff |
| Performance Validation on Multicore Mobile Devices / Thomas Hubbard ; Raimondas Lencevicius ; Edu Metz ; Gopal Raghavan |
| Tool Integration for Reasoned Programming / Andrew Ireland |
| Decision Procedures for the Grand Challenge / Daniel Kroening |
| The Challenge of Hardware-Software Co-verification / Panagiotis Manolios |
| From the How to the What / Tiziana Margaria ; Bernhard Steffen |
| An Overview of Separation Logic / John C. Reynolds |
| A Perspective on Program Verification / Willem-Paul de Roever |
| Meta-Logical Frameworks and Formal Digital Libraries / Carsten Schurmann |
| Languages, Ambiguity, and Verification |
| The Importance of Non-theorems and Counterexamples in Program Verification / Graham Steel |
| Regression Verification - A Practical Way to Verify Programs / Ofer STrichman ; Benny Godlin |
| Programming with Proofs: Language-Based Approaches to Totally Correct Software / Aaron Stump |
| The Role of Model-Based Testing / Mark Utting |
| Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification / Mitsuharu Yamamoto ; Yoshinori Tanabe ; Koichi Takahashi ; Masami Hagiya |
| Program Verification by Using DISCOVERER / Lu Yang ; Naijun Zhan ; Bican Xia ; Chaochen Zhou |
| Constraint Solving and Symbolic Execution / Jian Zhang |
| Author Index |
| Introduction |
| Verified Software: Theories, Tools, Experiments: Vision of a Grand Challenge Project / Tony Hoare ; Jay Misra |
| Verification Tools |
ＥＢ
