1. VSTTE 2005: Zurich, Switzerland

Introduction

• Tony Hoare, Jayadev Misra:
  Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project. 1-18
  

Verification Tools

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

Guaranteeing Correctness

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

Software Engineering Aspects

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

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
  
• Peter Müller:
  Reasoning about Object Structures Using Ownership. 93-104
  
• David A. Naumann:
  Modular Reasoning in Object-Oriented Programming. 105-115
  
• Peter W. O'Hearn:
  Scalable Specification and Reasoning: Challenges for Program Logic. 116-133
  

Programming Language and Methodology Aspects

• Gary T. Leavens, Curtis Clifton:
  Lessons from the JML Project. 134-143
  
• 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
  
• Joseph R. Kiniry, Patrice Chalin, Clément Hurlin:
  Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. 153-160
  

Components

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

Static Analysis

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

Design, Analysis and Tools

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

Formal Techniques

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

Position Papers

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

Last update Sat May 18 19:54:13 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page