IFIP TC6 Open Digital Library

1. VSTTE 2005: Zurich, Switzerland

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

Bertrand Meyer, Jim Woodcock

Springer, Lecture Notes in Computer Science 4171, ISBN: 978-3-540-69147-1



Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project.

Tony Hoare, Jayadev 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 0001, 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.

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


Reasoning about Object Structures Using Ownership.

Peter Müller


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.

Michael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs 0002, 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, Clément Hurlin



Automated Test Generation and Verified Software.

John M. Rushby


Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.

Yves Bertot, Laurent Théry


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.

Gogul Balakrishnan, Thomas W. Reps, David Melski, Tim Teitelbaum


Implications of a Data Structure Consistency Checking System.

Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. 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.

Gerard J. Holzmann, Rajeev Joshi


Trends and Challenges in Algorithmic Software Verification.

Rajeev Alur


Model Checking: Back and Forth between Hardware and Software.

Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith


Computational Logical Frameworks and Generic Program Analysis Technologies.

José 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.

Bernhard K. Aichernig, Jifeng He, Zhiming Liu 0001, 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 RealGrand Challenge.

Ramesh Bharadwaj


Linking the Meaning of Programs to What the Compiler Can Verify.

Egon Börger


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 A. McDermid, Ian Toyn


Verify Your Runs.

Klaus Havelund, Allen Goldberg


Specified Blocks.

Eric C. R. Hehner


A Case for Specification Validation.

Mats Per Erik 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 Schürmann


The SPARK Team: 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 0001