default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID1. VSTTE 2005: Zurich, Switzerland
- Bertrand Meyer, Jim Woodcock
:
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 Discussions. Lecture Notes in Computer Science 4171, Springer 2008, ISBN 978-3-540-69147-1
Introduction
- Tony Hoare, Jayadev Misra:
Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project. 1-18
Verification Tools
- Wolfgang J. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-05 22:22 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
