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 |