Abstract is missing.
- Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge ProjectTony Hoare, Jayadev Misra. 1-18 [doi]
- Towards a Worldwide Verification TechnologyWolfgang Paul. 19-25 [doi]
- It Is Time to Mechanize Programming Language MetatheoryBenjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic. 26-30 [doi]
- Methods and Tools for Formal Software EngineeringZhiming Liu, R. Venkatesh. 31-41 [doi]
- The Verified Software Challenge: A Call for a Holistic Approach to ReliabilityThomas Ball. 42-48 [doi]
- A Mini Challenge: Build a Verifiable FilesystemRajeev Joshi, Gerard J. Holzmann. 49-56 [doi]
- A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card AppletsAlessandro Coglio, Cordell Green. 57-63 [doi]
- Some Interdisciplinary Observations about Getting the Right SpecificationCliff B. Jones. 64-69 [doi]
- Software Verification and Software Engineering a Practitioner s PerspectiveAnthony Hall. 70-73 [doi]
- Decomposing Verification Around End-User FeaturesKathi Fisler, Shriram Krishnamurthi. 74-81 [doi]
- Automatic Verification of Strongly Dynamic Software SystemsNurit Dor, John Field, Denis Gopan, Tal Lev-Ami, Alexey Loginov, Roman Manevich, Ganesan Ramalingam, Thomas W. Reps, Noam Rinetzky, Mooly Sagiv, Reinhard Wilhelm, Eran Yahav, Greta Yorsh. 82-92 [doi]
- Reasoning about Object Structures Using OwnershipPeter Müller. 93-104 [doi]
- Modular Reasoning in Object-Oriented ProgrammingDavid A. Naumann. 105-115 [doi]
- Scalable Specification and Reasoning: Challenges for Program LogicPeter W. O Hearn. 116-133 [doi]
- Lessons from the JML ProjectGary T. Leavens, Curtis Clifton. 134-143 [doi]
- The Spec# Programming System: Challenges and DirectionsMichael Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs 0002, K. Rustan M. Leino, Wolfram Schulte, Herman Venter. 144-152 [doi]
- Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in VerificationJoseph R. Kiniry, Patrice Chalin, Clément Hurlin. 153-160 [doi]
- Automated Test Generation and Verified SoftwareJohn Rushby. 161-172 [doi]
- Dependent Types, Theorem Proving, and Applications for a Verifying CompilerYves Bertot, Laurent Théry. 173-181 [doi]
- Generating Programs Plus Proofs by RefinementDouglas R. Smith. 182-188 [doi]
- The Verification Grand Challenge and Abstract InterpretationPatrick Cousot. 189-201 [doi]
- WYSINWYX: What You See Is Not What You eXecuteGogul Balakrishnan, Thomas W. Reps, David Melski, Tim Teitelbaum. 202-213 [doi]
- Implications of a Data Structure Consistency Checking SystemViktor Kuncak, Patrick Lam, Karen Zee, Martin C. Rinard. 214-226 [doi]
- Towards the Integration of Symbolic and Numerical Static AnalysisArnaud Venet. 227-236 [doi]
- Reliable Software Systems Design: Defect Prevention, Detection, and ContainmentGerard J. Holzmann, Rajeev Joshi. 237-244 [doi]
- Trends and Challenges in Algorithmic Software VerificationRajeev Alur. 245-250 [doi]
- Model Checking: Back and Forth between Hardware and SoftwareEdmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith. 251-255 [doi]
- Computational Logical Frameworks and Generic Program Analysis TechnologiesJosé Meseguer, Grigore Rosu. 256-267 [doi]
- A Mechanized Program VerifierJ. Strother Moore. 268-276 [doi]
- Verifying Design with Proof ScoresKokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata. 277-290 [doi]
- Integrating Theories and Techniques for Program Modelling, Design and VerificationBernhard K. Aichernig, Jifeng He, Zhiming Liu, Mike Reed. 291-300 [doi]
- Eiffel as a Framework for VerificationBertrand Meyer. 301-307 [doi]
- Can We Build an Automatic Program Verifier? Invariant Proofs and Other ChallengesMyla Archer. 308-317 [doi]
- Verified Software: The RealGrand ChallengeRamesh Bharadwaj. 318-324 [doi]
- Linking the Meaning of Programs to What the Compiler Can VerifyEgon Börger. 325-336 [doi]
- Scalable Software Model Checking Using Design for VerificationTevfik Bultan, Aysu Betin-Can. 337-346 [doi]
- Model-Checking Software Using Precise AbstractionsMarsha Chechik, Arie Gurfinkel. 347-353 [doi]
- Toasters, Seat Belts, and Inferring Program PropertiesDavid Evans. 354-361 [doi]
- On the Formal Development of Safety-Critical SoftwareAndy Galloway, Frantz Iwu, John McDermid, Ian Toyn. 362-373 [doi]
- Verify Your RunsKlaus Havelund, Allen Goldberg. 374-383 [doi]
- Specified BlocksEric C. R. Hehner. 384-391 [doi]
- A Case for Specification ValidationMats Per Erik Heimdahl. 392-402 [doi]
- Some Verification Issues at NASA Goddard Space Flight CenterMichael G. Hinchey, James L. Rash, Christopher A. Rouff. 403-412 [doi]
- Performance Validation on Multicore Mobile DevicesThomas Hubbard, Raimondas Lencevicius, Edu Metz, Gopal Raghavan. 413-421 [doi]
- Tool Integration for Reasoned ProgrammingAndrew Ireland. 422-427 [doi]
- Decision Procedures for the Grand ChallengeDaniel Kroening. 428-437 [doi]
- The Challenge of Hardware-Software Co-verificationPanagiotis Manolios. 438-447 [doi]
- From the How to the WhatTiziana Margaria, Bernhard Steffen. 448-459 [doi]
- An Overview of Separation LogicJohn C. Reynolds. 460-469 [doi]
- A Perspective on Program VerificationWillem-Paul de Roever. 470-477 [doi]
- Meta-Logical Frameworks and Formal Digital LibrariesCarsten Schürmann. 478-485 [doi]
- The SPARK Team: Languages, Ambiguity, and Verification486-490 [doi]
- The Importance of Non-theorems and Counterexamples in Program VerificationGraham Steel. 491-495 [doi]
- Regression Verification - A Practical Way to Verify ProgramsOfer Strichman, Benny Godlin. 496-501 [doi]
- Programming with Proofs: Language-Based Approaches to Totally Correct SoftwareAaron Stump. 502-509 [doi]
- The Role of Model-Based TestingMark Utting. 510-517 [doi]
- Abstraction of Graph Transformation Systems by Temporal Logic and Its VerificationMitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, Masami Hagiya. 518-527 [doi]
- Program Verification by Using DISCOVERERLu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou. 528-538 [doi]
- Constraint Solving and Symbolic ExecutionJian Zhang. 539-544 [doi]