Position Papers

Jean-Raymond Abrial
On Constructing Large Computerized Systems (a position paper)
PDF

Bernard K Aichernig, He Jifeng, Zhiming Liu, and Mike Reed
Integrating Theories and Techniques for Program Modelling, Design and Verification
PDF

Rajeev Alur
Trends and Challenges in Algorithmic Software Verification
PDF

Myla Archer
The Role of Invariants in an Automatic Program Verifier
PDF

G. Balakrishnan, T. Reps, D. Melski, and T. Teitelbaum
WYSINWYX: What You See Is Not What You eXecute
PDF

Thomas Ball
The Verified Software Challenge: A Call for a Holistic Approach to Reliability
PDF

Mike Barnett, Robert DeLine, Bart Jacobs, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter
The Spec# Programmin System: Challenges and Directions
PDF

Yves Bertot and Laurent Théry
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler
PDF

Ramesh Bharadwaj
Whither Verified Software?
PDF

Egon Börger
Linking Content Definition and Analysis to What the Compiler Can Verify
PDF

Tevfik Bultan and Aysu Betin-Can
Scalable Software Model Checking Using Design for Verification
PDF

Marsha Chechik and Arie Gurfinkel
Model-Checking Software Using Precise Abstactions
PDF

Edmund Clarke, Anubhav Gupta, Himanshu Jain, and Helmut Veith
Model Checking: Back and Forth Between Hardware and Software
PDF

Alessandro Coglio and Cordell Green
A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets
PDF

Patrick Cousot
The Verification Grand Challenge and Abstract Interpretation
PDF

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, and G. Yorsh
Automatic Verification of Strongly Dynamic Software Systems
PDF

David Evans
Toasters, Seat Belts, and Inferring Program Properties
PDF

Kathi Fisler and Shriram Krishnamurthi
Decomposing Verification by Features
PDF

Kokichi Futatsugi, Joseph A. Goguen, and Kazuhiro Ogata
Verifying Design with Proof Scores
PDF

Andy Galloway, Frantz Iwu, John McDermid, and Ian Toyn
On the Formal Development of Safety-Critical Software
PDF

Klaus Havelund and Allen Goldberg
Verify Your Runs
PDF

Anthony Hall
Software Verification and Software Engineering: A Practitioner's Perspective
PDF

Eric C. R. Hehner
Specified Blocks
PDF

Mats P. E. Heimdahl
Let's Not Forget Validation
PDF

Michael G. Hinchey, James L. Rash, and Christopher A. Rouff
Some Verification Issues at NASA Goddard Space Flight Center
PDF

Tony Hoare and Jay Misra
Verified software: theories, tools, experiments - Vision of a Grand Challenge project
PDF

Gerard J. Holzmann and Rajeev Joshi
Reliable Software Systems Design: Defect Prevention, Detection, and Containment
PDF

Thomas Hubbard, Raimondas Lencevicius, Edu Metz, and Gopal Raghavan
Performance Validation on Multicore Mobile Devices
PDF

Andrew Ireland
Tool Integration for Reasoned Programming
PDF

Cliff B. Jones
What can we do (technically) to get "the right specification?"
PDF

Rajeev Joshi and Gerard J. Holzmann
A Mini Challange: Build a Verifiable Filesystem
PDF

Joseph R. Kiniry, Patrice Chalin, and Clément Hurlin
Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification
PDF

Daniel Kroening
Decision Procedures for the Grand Challenge
PDF

Viktor Kuncak, Patrick Lam, Karan Zee, and Martin Rinard
Implications of a Data Structure Consistency Checking System
PDF

Gary T. Leavens and Curtis Clifton
Lessons from the JML Project
PDF

Zhiming Liu and R. Venkatesh
Tools for Formal Software Engineeering
PDF

Panagiotis Manolios
The Challenge of Hardware-Software Co-Verification
PDF

Tiziana Margaria and Bernhard Steffen
From the How to the What
PDF

José Meseguer and Grigore Rosu
Computational Logical Frameworks and Generic Program Analysis Technologies
PDF

J Strother Moore
A Mechanized Program Verifier
PDF

Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, and Natarajan Shankar
Integrating Verification Components
PDF

Peter Müller
Reasoning about Object Structures Using Ownership
PDF

David A. Naumann
Modular reasoning in object-oriented programming
PDF

Colin O'Halloran
Where is the value in a Program Verifier?
PDF

Peter W. O'Hearn
Scalable Specification and Reasoning: Technical Challenges for Program Logic
PDF

Wolfgang Paul
Towards a Worldwide Verification Technology
PDF

Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, and Steve Zdancewic
It is Time to Mechanize Programming Language Metatheory
PDF

John C. Reynolds
An Overview of Separation Logic
PDF

Willem-Paul de Roever
A Perspective on Program Verification
PDF

John Rushby
Automated Test Generation And Verified Software
PDF

Carsten Schürmann
Meta-Logical Frameworks and Formal Digital Libraries
PDF

Douglas R. Smith
Generating Programs plus Proofs by Refinement
PDF

The SPARK Team
Languages, Ambiguity, and Verification
PDF

Graham Steel
The Importance of Non-theorems and Counterexamples in Program Verification
PDF

Ofer Strichman and Benny Godlin
Regression Verification - a practical way to verify programs
PDF

Aaron Stump
Programming with Proofs: Language-Based Approaches to Totally Correct Software
PDF

Mark Utting
Position Paper: Model-Based Testing
PDF

Arnaud Venet
Toward the Integration of Symbolic and Numerical Static Analysis
PDF

Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, and Masami Hagiya
Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification
PDF

Lu Yang, Naijun Zhan, Bican Xia, and Chaochen Zhou
Program Verification by Using DISCOVERER
PDF

Jian Zhang
Constraint Solving and Symbolic Execution
PDF