1. VSTTE 2005: Zurich, Switzerland

Bertrand Meyer, Jim Woodcock (Eds.): 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. Lecture Notes in Computer Science 4171 Springer 2008, ISBN 978-3-540-69147-1 BibTeX

Introduction

Tony Hoare, Jayadev Misra:
Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project. 1-18
Electronic Edition (link) BibTeX

Verification Tools

Wolfgang Paul:
Towards a Worldwide Verification Technology. 19-25
Electronic Edition (link) BibTeX
Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic:
It Is Time to Mechanize Programming Language Metatheory. 26-30
Electronic Edition (link) BibTeX
Zhiming Liu, R. Venkatesh:
Methods and Tools for Formal Software Engineering. 31-41
Electronic Edition (link) BibTeX

Guaranteeing Correctness

Thomas Ball:
The Verified Software Challenge: A Call for a Holistic Approach to Reliability. 42-48
Electronic Edition (link) BibTeX
Rajeev Joshi, Gerard J. Holzmann:
A Mini Challenge: Build a Verifiable Filesystem. 49-56
Electronic Edition (link) BibTeX
Alessandro Coglio, Cordell Green:
A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets. 57-63
Electronic Edition (link) BibTeX
Cliff B. Jones:
Some Interdisciplinary Observations about Getting the "Right" Specification. 64-69
Electronic Edition (link) BibTeX

Software Engineering Aspects

Anthony Hall:
Software Verification and Software Engineering a Practitioner's Perspective. 70-73
Electronic Edition (link) BibTeX
Kathi Fisler, Shriram Krishnamurthi:
Decomposing Verification Around End-User Features. 74-81
Electronic Edition (link) BibTeX

Verifying Object-Oriented Programming

Nurit Dor, John Field, Denis Gopan, Tal Lev-Ami, Alexey Loginov, Roman Manevich, G. Ramalingam, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav, Greta Yorsh:
Automatic Verification of Strongly Dynamic Software Systems. 82-92
Electronic Edition (link) BibTeX
Peter Müller:
Reasoning about Object Structures Using Ownership. 93-104
Electronic Edition (link) BibTeX
David A. Naumann:
Modular Reasoning in Object-Oriented Programming. 105-115
Electronic Edition (link) BibTeX
Peter W. O'Hearn:
Scalable Specification and Reasoning: Challenges for Program Logic. 116-133
Electronic Edition (link) BibTeX

Programming Language and Methodology Aspects

Gary T. Leavens, Curtis Clifton:
Lessons from the JML Project. 134-143
Electronic Edition (link) BibTeX
Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte, Herman Venter:
The Spec# Programming System: Challenges and Directions. 144-152
Electronic Edition (link) BibTeX
Joseph R. Kiniry, Patrice Chalin, Clément Hurlin:
Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. 153-160
Electronic Edition (link) BibTeX

Components

John Rushby:
Automated Test Generation and Verified Software. 161-172
Electronic Edition (link) BibTeX
Yves Bertot, Laurent Théry:
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. 173-181
Electronic Edition (link) BibTeX
Douglas R. Smith:
Generating Programs Plus Proofs by Refinement. 182-188
Electronic Edition (link) BibTeX

Static Analysis

Patrick Cousot:
The Verification Grand Challenge and Abstract Interpretation. 189-201
Electronic Edition (link) BibTeX
Gogul Balakrishnan, Thomas W. Reps, David Melski, Tim Teitelbaum:
WYSINWYX: What You See Is Not What You eXecute. 202-213
Electronic Edition (link) BibTeX
Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard:
Implications of a Data Structure Consistency Checking System. 214-226
Electronic Edition (link) BibTeX
Arnaud Venet:
Towards the Integration of Symbolic and Numerical Static Analysis. 227-236
Electronic Edition (link) BibTeX

Design, Analysis and Tools

Gerard J. Holzmann, Rajeev Joshi:
Reliable Software Systems Design: Defect Prevention, Detection, and Containment. 237-244
Electronic Edition (link) BibTeX
Rajeev Alur:
Trends and Challenges in Algorithmic Software Verification. 245-250
Electronic Edition (link) BibTeX
Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith:
Model Checking: Back and Forth between Hardware and Software. 251-255
Electronic Edition (link) BibTeX
José Meseguer, Grigore Rosu:
Computational Logical Frameworks and Generic Program Analysis Technologies. 256-267
Electronic Edition (link) BibTeX

Formal Techniques

J. Strother Moore:
A Mechanized Program Verifier. 268-276
Electronic Edition (link) BibTeX
Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata:
Verifying Design with Proof Scores. 277-290
Electronic Edition (link) BibTeX
Bernhard K. Aichernig, Jifeng He, Zhiming Liu, Mike Reed:
Integrating Theories and Techniques for Program Modelling, Design and Verification. 291-300
Electronic Edition (link) BibTeX
Bertrand Meyer:
Eiffel as a Framework for Verification. 301-307
Electronic Edition (link) BibTeX

Position Papers

Myla Archer:
Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges. 308-317
Electronic Edition (link) BibTeX
Ramesh Bharadwaj:
Verified Software: The RealGrand Challenge. 318-324
Electronic Edition (link) BibTeX
Egon Börger:
Linking the Meaning of Programs to What the Compiler Can Verify. 325-336
Electronic Edition (link) BibTeX
Tevfik Bultan, Aysu Betin-Can:
Scalable Software Model Checking Using Design for Verification. 337-346
Electronic Edition (link) BibTeX
Marsha Chechik, Arie Gurfinkel:
Model-Checking Software Using Precise Abstractions. 347-353
Electronic Edition (link) BibTeX
David Evans:
Toasters, Seat Belts, and Inferring Program Properties. 354-361
Electronic Edition (link) BibTeX
Andy Galloway, Frantz Iwu, John McDermid, Ian Toyn:
On the Formal Development of Safety-Critical Software. 362-373
Electronic Edition (link) BibTeX
Klaus Havelund, Allen Goldberg:
Verify Your Runs. 374-383
Electronic Edition (link) BibTeX
Eric C. R. Hehner:
Specified Blocks. 384-391
Electronic Edition (link) BibTeX
Mats Per Erik Heimdahl:
A Case for Specification Validation. 392-402
Electronic Edition (link) BibTeX
Michael G. Hinchey, James L. Rash, Christopher A. Rouff:
Some Verification Issues at NASA Goddard Space Flight Center. 403-412
Electronic Edition (link) BibTeX
Thomas Hubbard, Raimondas Lencevicius, Edu Metz, Gopal Raghavan:
Performance Validation on Multicore Mobile Devices. 413-421
Electronic Edition (link) BibTeX
Andrew Ireland:
Tool Integration for Reasoned Programming. 422-427
Electronic Edition (link) BibTeX
Daniel Kroening:
Decision Procedures for the Grand Challenge. 428-437
Electronic Edition (link) BibTeX
Panagiotis Manolios:
The Challenge of Hardware-Software Co-verification. 438-447
Electronic Edition (link) BibTeX
Tiziana Margaria, Bernhard Steffen:
From the How to the What. 448-459
Electronic Edition (link) BibTeX
John C. Reynolds:
An Overview of Separation Logic. 460-469
Electronic Edition (link) BibTeX
Willem-Paul de Roever:
A Perspective on Program Verification. 470-477
Electronic Edition (link) BibTeX
Carsten Schürmann:
Meta-Logical Frameworks and Formal Digital Libraries. 478-485
Electronic Edition (link) BibTeX
The SPARK Team: Languages, Ambiguity, and Verification. 486-490
Electronic Edition (link) BibTeX
Graham Steel:
The Importance of Non-theorems and Counterexamples in Program Verification. 491-495
Electronic Edition (link) BibTeX
Ofer Strichman, Benny Godlin:
Regression Verification - A Practical Way to Verify Programs. 496-501
Electronic Edition (link) BibTeX
Aaron Stump:
Programming with Proofs: Language-Based Approaches to Totally Correct Software. 502-509
Electronic Edition (link) BibTeX
Mark Utting:
The Role of Model-Based Testing. 510-517
Electronic Edition (link) BibTeX
Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, Masami Hagiya:
Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification. 518-527
Electronic Edition (link) BibTeX
Lu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou:
Program Verification by Using DISCOVERER. 528-538
Electronic Edition (link) BibTeX
Jian Zhang:
Constraint Solving and Symbolic Execution. 539-544
Electronic Edition (link) BibTeX