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

Tony Hoare, Jayadev Misra

 1-18

Towards a Worldwide Verification Technology.

Wolfgang Paul

 19-25

It Is Time to Mechanize Programming Language Metatheory.

Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic

 26-30

Methods and Tools for Formal Software Engineering.

Zhiming Liu 0001, R. Venkatesh

 31-41

The Verified Software Challenge: A Call for a Holistic Approach to Reliability.

Thomas Ball

 42-48

A Mini Challenge: Build a Verifiable Filesystem.

Rajeev Joshi, Gerard J. Holzmann

 49-56

A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets.

Alessandro Coglio, Cordell Green

 57-63

Some Interdisciplinary Observations about Getting the "Right" Specification.

Cliff B. Jones

 64-69

Software Verification and Software Engineering a Practitioner's Perspective.

Anthony Hall

 70-73

Decomposing Verification Around End-User Features.

Kathi Fisler, Shriram Krishnamurthi

 74-81

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

 82-92

Reasoning about Object Structures Using Ownership.

Peter Müller

 93-104

Modular Reasoning in Object-Oriented Programming.

David A. Naumann

 105-115

Scalable Specification and Reasoning: Challenges for Program Logic.

Peter W. O'Hearn

 116-133

Lessons from the JML Project.

Gary T. Leavens, Curtis Clifton

 134-143

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

 144-152

Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification.

Joseph R. Kiniry, Patrice Chalin, Clément Hurlin

 153-160

Automated Test Generation and Verified Software.

John M. Rushby

 161-172

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

Yves Bertot, Laurent Théry

 173-181

Generating Programs Plus Proofs by Refinement.

Douglas R. Smith

 182-188

The Verification Grand Challenge and Abstract Interpretation.

Patrick Cousot

 189-201

WYSINWYX: What You See Is Not What You eXecute.

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

 202-213

Implications of a Data Structure Consistency Checking System.

Viktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard

 214-226

Towards the Integration of Symbolic and Numerical Static Analysis.

Arnaud Venet

 227-236

Reliable Software Systems Design: Defect Prevention, Detection, and Containment.

Gerard J. Holzmann, Rajeev Joshi

 237-244

Trends and Challenges in Algorithmic Software Verification.

Rajeev Alur

 245-250

Model Checking: Back and Forth between Hardware and Software.

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

 251-255

Computational Logical Frameworks and Generic Program Analysis Technologies.

José Meseguer, Grigore Rosu

 256-267

A Mechanized Program Verifier.

J. Strother Moore

 268-276

Verifying Design with Proof Scores.

Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata

 277-290

Integrating Theories and Techniques for Program Modelling, Design and Verification.

Bernhard K. Aichernig, Jifeng He, Zhiming Liu 0001, Mike Reed

 291-300

Eiffel as a Framework for Verification.

Bertrand Meyer

 301-307

Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges.

Myla Archer

 308-317

Verified Software: The RealGrand Challenge.

Ramesh Bharadwaj

 318-324

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

Egon Börger

 325-336

Scalable Software Model Checking Using Design for Verification.

Tevfik Bultan, Aysu Betin-Can

 337-346

Model-Checking Software Using Precise Abstractions.

Marsha Chechik, Arie Gurfinkel

 347-353

Toasters, Seat Belts, and Inferring Program Properties.

David Evans

 354-361

On the Formal Development of Safety-Critical Software.

Andy Galloway, Frantz Iwu, John A. McDermid, Ian Toyn

 362-373

Verify Your Runs.

Klaus Havelund, Allen Goldberg

 374-383

Specified Blocks.

Eric C. R. Hehner

 384-391

A Case for Specification Validation.

Mats Per Erik Heimdahl

 392-402

Some Verification Issues at NASA Goddard Space Flight Center.

Michael G. Hinchey, James L. Rash, Christopher A. Rouff

 403-412

Performance Validation on Multicore Mobile Devices.

Thomas Hubbard, Raimondas Lencevicius, Edu Metz, Gopal Raghavan

 413-421

Tool Integration for Reasoned Programming.

Andrew Ireland

 422-427

Decision Procedures for the Grand Challenge.

Daniel Kroening

 428-437

The Challenge of Hardware-Software Co-verification.

Panagiotis Manolios

 438-447

From the How to the What.

Tiziana Margaria, Bernhard Steffen

 448-459

An Overview of Separation Logic.

John C. Reynolds

 460-469

A Perspective on Program Verification.

Willem-Paul de Roever

 470-477

Meta-Logical Frameworks and Formal Digital Libraries.

Carsten Schürmann

 478-485

The SPARK Team: Languages, Ambiguity, and Verification.

 486-490

The Importance of Non-theorems and Counterexamples in Program Verification.

Graham Steel

 491-495

Regression Verification - A Practical Way to Verify Programs.

Ofer Strichman, Benny Godlin

 496-501

Programming with Proofs: Language-Based Approaches to Totally Correct Software.

Aaron Stump

 502-509

The Role of Model-Based Testing.

Mark Utting

 510-517

Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification.

Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, Masami Hagiya

 518-527

Program Verification by Using DISCOVERER.

Lu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou

 528-538

Constraint Solving and Symbolic Execution.

Jian Zhang 0001

 539-544