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 DiscussionsBertrand Meyer, Jim Woodcock A Step Towards Verified Software Worries about the reliability of software are as old as software itself; techniques for allaying these worries predate even James King’s 1969 thesis on “A program verifier. ” What gives the whole topic a new urgency is the conjunction of three phenomena: the blitz-like spread of software-rich systems to control ever more facets of our world and our lives; our growing impatience with deficiencies; and the development—proceeding more slowly, alas, than the other two trends—of techniques to ensure and verify software quality. In 2002 Tony Hoare, one of the most distinguished contributors to these advances over the past four decades, came to the conclusion that piecemeal efforts are no longer sufficient and proposed a “Grand Challenge” intended to achieve, over 15 years, the production of a verifying compiler: a tool that while processing programs would also guarantee their adherence to specified properties of correctness, robustness, safety, security and other desirable properties. As Hoare sees it, this endeavor is not a mere research project, as might normally be carried out by one team or a small consortium of teams, but a momentous endeavor, comparable in its scope to the successful mission to send a man to the moon or to the sequencing of the human genome. |
Contents
| 1 | |
Towards a Worldwide Verification Technology | 19 |
It Is Time to Mechanize Programming Language Metatheory | 26 |
Methods and Tools for Formal Software Engineering | 31 |
A Call for a Holistic Approach to Reliability | 42 |
Build a Verifiable Filesystem | 49 |
A Constructive Approach to Correctness Exemplified by a Generator for Certified Java Card Applets | 57 |
Some Interdisciplinary Observations about Getting the Right Specification | 64 |
Eiffel as a Framework for Verification | 301 |
Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges | 308 |
The Real Grand Challenge | 318 |
Linking the Meaning of Programs to What the Compiler Can Verify | 325 |
Scalable Software Model Checking Using Design for Verification | 337 |
ModelChecking Software Using Precise Abstractions | 347 |
Toasters Seat Belts and Inferring Program Properties | 354 |
On the Formal Development of SafetyCritical Software | 362 |
Software Verification and Software Engineeringa Practitioners Perspective | 70 |
Decomposing Verification Around EndUser Features | 74 |
Automatic Verification of Strongly Dynamic Software Systems | 82 |
Reasoning about Object Structures Using Ownership | 93 |
Modular Reasoning in ObjectOriented Programming | 105 |
Challenges for Program Logic | 116 |
Lessons from the JML Project | 134 |
Challenges and Directions | 144 |
Supporting Multiple Theories and Provers in Verification | 153 |
Automated Test Generation and Verified Software | 161 |
Dependent Types Theorem Proving and Applications for a Verifying Compiler | 173 |
Generating Programs Plus Proofs by Refinement | 182 |
The Verification Grand Challenge and Abstract Interpretation | 189 |
What You See Is NotWhat You eXecute | 202 |
Implications of a Data Structure Consistency Checking System | 214 |
Towards the Integration of Symbolic and Numerical Static Analysis | 227 |
Defect Prevention Detection and Containment | 237 |
Trends and Challenges in Algorithmic Softwar eVerification | 245 |
Back and Forth between Hardware and Software | 251 |
Computational Logical Frameworks and Generic Program Analysis Technologies | 256 |
A Mechanized Program Verifier | 268 |
Verifying Design with Proof Scores | 277 |
Integrating Theories and Techniques for Program Modelling Design and Verification Positioning the Research at UNUIIST in Collaborative Research... | 291 |
Verify Your Runs | 374 |
Specified Blocks | 384 |
A Case for Specification Validation | 392 |
Some Verification Issues at NASA Goddard Space Flight Center | 403 |
Performance Validation on Multicore Mobile Devices | 413 |
Tool Integration for Reasoned Programming | 422 |
Decision Procedures for the Grand Challenge | 428 |
The Challenge of HardwareSoftware Coverification | 438 |
From the How to the What | 448 |
An Overview of Separation Logic | 460 |
A Perspective on Program Verification | 470 |
MetaLogical Frameworks and Formal Digital Libraries | 478 |
Languages Ambiguity and Verification | 486 |
The Importance of Nontheorems and Counterexamples in Program Verification | 491 |
Regression Verification A Practical Way to Verify Programs | 496 |
LanguageBased Approaches to Totally Correct Software | 502 |
The Role of ModelBased Testing | 510 |
| 518 | |
Program Verification by Using DISCOVERER | 528 |
Constraint Solving and Symbolic Execution | 539 |
| 545 | |
Other editions - View all
Common terms and phrases
abstract interpretation algorithms analyze application approach assertions Astrée automated automatic behavior checker complex components Computer Science concurrent constraints construction correctness counterexamples Cousot data structures decision procedures domain dynamic embedded encoding environment errors ESC/Java2 example execution Federation for Information formal methods formal specification formal verification framework functions goal Grand Challenge heap Heidelberg Heidelberg 2005 Hoare IEEE IFIP International Federation implementation Information Processing 2008 input integration interactive interface invariants Java Java Card Leino LNCS machine mathematical Meyer model checking model-based testing modular module node object object-oriented programs pointer predicate problem Proc program analysis program verification programming language proof scores properties proving reasoning refinement requirements rewriting scalable semantics separation logic Software Engineering software verification Spec specification language Springer static analysis techniques temporal logic theorem prover theory tion UNU-IIST validation variables verification tools Verified Software verifying compiler Woodcock Eds