close
1.

電子ブック

EB
Cliff B. Jones, Takeo Kanade, Zhiming Liu, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2007
所蔵情報: loading…
2.

電子ブック

EB
Ana Cavalcanti, Takeo Kanade, Augusto Sampaio, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2006
所蔵情報: loading…
3.

電子ブック

EB
Natarajan Shankar, Takeo Kanade, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2008
所蔵情報: loading…
4.

電子ブック

EB
Bertrand Meyer, Takeo Kanade, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2008
所蔵情報: loading…
目次情報: 続きを見る
Introduction
Verified Software: Theories, Tools, Experiments: Vision of a Grand Challenge Project / Tony Hoare ; Jay Misra
Verification Tools
Towards a Worldwide Verification Technology / Wolfgang Paul
It Is Time to Mechanize Programming Language Metatheory / Benjamin C. Pierce ; Peter Sewell ; Stephanie Weirich ; Steve Zdancewic
Methods and Tools for Formal Software Engineering / Zhiming Liu ; R. Venkatesh
Guaranteeing Correctness
The Verified Software Challenge: A Call for a Holistic Approach to Reliability / Thomas Ball
A Mini Challenge: Build a Verifiable Filesystem / Rajeev Joshi ; Gerard J. Holzmann
A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets / Alessandro Coglio ; Cordell Green
Some Interdisciplinary Observations about Getting the "Right" Specification / Cliff B. Jones
Software Engineering Aspects
Software Verification and Software Engineering a Practitioner's Perspective / Anthony Hall
Decomposing Verification Around End-User Features / Kathi Fisler ; Shriram Krishnamurthi
Verifying Object-Oriented Programming
Automatic Verification of Strongly Dynamic Software Systems / 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 ; G. Yorsh
Reasoning about Object Structures Using Ownership / Peter Muller
Modular Reasoning in Object-Oriented Programming / David A. Naumann
Scalable Specification and Reasoning: Challenges for Program Logic / Peter W. O'Hearn
Programming Language and Methodology Aspects
Lessons from the JML Project / Gary T. Leavens ; Curtis Clifton
The Spec# Programming System: Challenges and Directions / Mike Barnett ; Robert DeLine ; Manuel Fahndrich ; Bart Jacobs ; K. Rustan M. Leino ; Wolfram Schulte ; Herman Venter
Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification / Joseph R. Kiniry ; Patrice Chalin ; Clement Hurlin
Components
Automated Test Generation and Verified Software / John Rushby
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler / Yves Bertot ; Laurent Thery
Generating Programs Plus Proofs by Refinement / Douglas R. Smith
Static Analysis
The Verification Grand Challenge and Abstract Interpretation / Patrick Cousot
WYSINWYX: What You See Is Not What You eXecute / G. Balakrishnan ; D. Melski ; T. Teitelbaum
Implications of a Data Structure Consistency Checking System / Viktor Kuncak ; Patrick Lam ; Karen Zee ; Martin Rinard
Towards the Integration of Symbolic and Numerical Static Analysis / Arnaud Venet
Design, Analysis and Tools
Reliable Software Systems Design: Defect Prevention, Detection, and Containment
Trends and Challenges in Algorithmic Software Verification / Rajeev Alur
Model Checking: Back and Forth between Hardware and Software / Edmund Clarke ; Anubhav Gupta ; Himanshu Jain ; Helmut Veith
Computational Logical Frameworks and Generic Program Analysis Technologies / Jose Meseguer ; Grigore Rosu
Formal Techniques
A Mechanized Program Verifier / J. Strother Moore
Verifying Design with Proof Scores / Kokichi Futatsugi ; Joseph A. Goguen ; Kazuhiro Ogata
Integrating Theories and Techniques for Program Modelling, Design and Verification: Positioning the Research at UNU-IIST in Collaborative Research on the Verified Software Challenge / Bernard K. Aichernig ; He Jifeng ; Mike Reed
Eiffel as a Framework for Verification / Bertrand Meyer
Position Papers
Can We Build an Automatic Program Verifier? Invariant Proofs and Other Challenges / Myla Archer
Verified Software: The Real Grand Challenge / Ramesh Bharadwaj
Linking the Meaning of Programs to What the Compiler Can Verify / Egon Borger
Scalable Software Model Checking Using Design for Verification / Tevfik Bultan ; Aysu Betin-Can
Model-Checking Software Using Precise Abstractions / Marsha Chechik ; Arie Gurfinkel
Toasters, Seat Belts, and Inferring Program Properties / David Evans
On the Formal Development of Safety-Critical Software / Andy Galloway ; Frantz Iwu ; John McDermid ; Ian Toyn
Verify Your Runs / Klaus Havelund ; Allen Goldberg
Specified Blocks / Eric C.R. Hehner
A Case for Specification Validation / Mats P.E. Heimdahl
Some Verification Issues at NASA Goddard Space Flight Center / Michael G. Hinchey ; James L. Rash ; Christopher A. Rouff
Performance Validation on Multicore Mobile Devices / Thomas Hubbard ; Raimondas Lencevicius ; Edu Metz ; Gopal Raghavan
Tool Integration for Reasoned Programming / Andrew Ireland
Decision Procedures for the Grand Challenge / Daniel Kroening
The Challenge of Hardware-Software Co-verification / Panagiotis Manolios
From the How to the What / Tiziana Margaria ; Bernhard Steffen
An Overview of Separation Logic / John C. Reynolds
A Perspective on Program Verification / Willem-Paul de Roever
Meta-Logical Frameworks and Formal Digital Libraries / Carsten Schurmann
Languages, Ambiguity, and Verification
The Importance of Non-theorems and Counterexamples in Program Verification / Graham Steel
Regression Verification - A Practical Way to Verify Programs / Ofer STrichman ; Benny Godlin
Programming with Proofs: Language-Based Approaches to Totally Correct Software / Aaron Stump
The Role of Model-Based Testing / Mark Utting
Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification / Mitsuharu Yamamoto ; Yoshinori Tanabe ; Koichi Takahashi ; Masami Hagiya
Program Verification by Using DISCOVERER / Lu Yang ; Naijun Zhan ; Bican Xia ; Chaochen Zhou
Constraint Solving and Symbolic Execution / Jian Zhang
Author Index
Introduction
Verified Software: Theories, Tools, Experiments: Vision of a Grand Challenge Project / Tony Hoare ; Jay Misra
Verification Tools
5.

電子ブック

EB
Marcel Vinícius Medeiros Oliveira, Takeo Kanade, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2009
所蔵情報: loading…
6.

電子ブック

EB
Chris W. George, Takeo Kanade, Zhiming Liu, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2007
所蔵情報: loading…
7.

電子ブック

EB
Cliff B. Jones, Dines Bjørner, Zhou Chaochen, Takeo Kanade, Zhiming Liu, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2007
所蔵情報: loading…
8.

電子ブック

EB
Ana Cavalcanti, David Deharbe, Marie-Claude Gaudel, Takeo Kanade, Jim Woodcock
出版情報: Springer eBooks Computer Science , Springer Berlin Heidelberg, 2010
所蔵情報: loading…
目次情報: 続きを見る
Invited Papers and Abstract
Invariants and Well-Foundedness in Program Algebra / Ian J. Hayes
A Theory of Software Product Line Refinement / Paulo Borba ; Leopoldo Teixeira ; Rohit Gheyi
Grammars / Kaustuv Chaudhuri ; Damien Doligez ; Leslie Lamport ; Stephan Merz
Subtyping Algorithm of Regular Tree Grammars with Disjoint Production Rules / Lei Chen ; Haiming Chen
Minimal Tree Language Extensions: A Keystone of XML Type Compatibility and Evolution / Jacques Chabin ; Mirian Halfeld-Ferrari ; Martin A. Musicante ; Pierre Réty
Tracking Down the Origins of Ambiguity in Context-Free Grammars / H.J.S. Basten
Semantics
Prioritized slotted-Circus / Pawel Gancarski ; Andrew Butterfield
A Denotational Semantical Model for Orc Language / Qin Li ; Huibiao Zhu ; Jifeng He
An Extended cCSP with Stable Failures Semantics / Zhenbang Chen ; Zhiming Liu
Preference and Non-deterministic Choice / Bill Stoddart ; Frank Zeyda ; Steve Dunne
Modelling
Material Flow Abstraction of Manufacturing Systems / Jewgenij Botaschanjan ; Benjamin Hummel
Specification and Verification of a MPI Implementation for a MP-SoC / Umberto Souza da Costa ; Ivan Soares de Medeiros Júnior ; Marcel Vinicius Medeiros Oliveira
Special Track: Formal Aspects of Software Testing and Grand Challenge in Verified Software
Testing of Abstract Components / Bilal Kanso ; Marc Aiguier ; Frédéric Boulanger ; Assia Touil
Scalable Distributed Concolic Testing: A Case Study on a Flash Storage Platform / Yunho Kim ; Moonzoo Kim ; Nam Dang
Analyzing a Formal Specification of Mondex Using Model Checking / Reng Zeng ; Xudong He
Formal Modelling of Separation Kernel Components / Andrius Velykis ; Leo Freitas
Mechanized Verification with Sharing / Gregory Malecha ; Greg Morrisett
Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking / Ashish Darbari ; Bernd Fischer ; João Marques-Silva
Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements / Mariano M. Moscato ; Carlos Gustavo López Pombo ; Marcelo Fabiùn Frias
Logics
Complete Calculi for Structured Specifications in Fork Algebra / Carlos Gustavo Lopez Pombo
Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting / Pablo F. Castro ; Nazareno M. Aguirre ; Carlos Gustavo L ópez Pombo ; Thomas S.E. Maibaum
Characterizing Locality (Encapsulation) with Bisimulation / Tom S.E. Maibaum
Justification Logic and History Based Computation / Francisco Bavera ; Eduardo Bonelli
Algorithms and Types
A Class of Greedy Algorithms and Its Relation to Greedoids / Srinivas Nedunuri ; Douglas R. Smith ; William R. Cook
On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types / Paul Tarau
A Modality for Safe Resource Sharing and Code Reentrancy / Rui Shi ; Dengping Zhu ; Hongwei Xi
Author Index
Invited Papers and Abstract
Invariants and Well-Foundedness in Program Algebra / Ian J. Hayes
A Theory of Software Product Line Refinement / Paulo Borba ; Leopoldo Teixeira ; Rohit Gheyi
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼