Verification of Concurrent Programs Using the Coq Proof Assistant : A Case Study
スポンサーリンク
概要
- 論文の詳細を見る
We show how to model and verify a concurrent program using the Coq proof assistant. The program in question is an existing mail server written in Java. The approach we take is to use an original library that provides a language for modeling, a logic, and lemmas for verification of concurrent programs. First, we report on the modeling of the mail server. Using the language provided by the library, we build a model by (1) translating the original program and (2) building appropriate abstractions to model its environment. Second, we report on the verification of a property of the mail server. We compare this library-based approach with an alternative approach that directly appeals to the Coq language and logic for modeling and specification. We show that the library-based approach has many advantages. In particular, non-functional aspects (communications, non-determinism, multi-threading) are handled directly by the library and therefore do not require complicated modeling. Also, the model can be directly run using existing compilers or virtual machines, thus providing us with a certified implementation of the mail server.
- 一般社団法人情報処理学会の論文
- 2005-01-15
著者
-
KOBAYASHI Naoki
Department of Physics, Chuo University
-
Yonezawa A
Department Of Computer Science The University Of Tokyo
-
Yonezawa Akinori
Department Of Information Science Tokyo Institute Of Technology
-
AFFELDT REYNALD
Department of Computer Science, The University of Tokyo
-
Kobayashi N
Department Of Computer Science Tokyo Institute Of Technology
-
Kobayashi Naoki
Department Of Orthopaedic Surgery Dokkyo University School Of Medicine
-
Affeldt Reynald
Department Of Computer Science The University Of Tokyo
-
Kobayashi Naoki
Department Of Applied Physics And Chemistry The University Of Electro-communications
-
Yonezawa Akinori
Department of Computer Science, The University of Tokyo
関連論文
- Reconstruction and Extension of the Family-Vicsek Scaling Hypothesis for Growing Rough Interfaces(General)
- Multi-Affinity for Growing Rough Interfaces of Bacterial Colonies(Oscillation, Chaos and Network Dynamics in Nonlinear Science)
- Extended Dynamic Scaling for Growing Interfaces(General)
- Patterns of Expansion produced by a Structured Cell Population of Serratia marcescens in Response to Different Media
- Modelling and Numerical Analysis of the Colony Formation of Bacteria
- Dream of Sanetomo : His Portrait in the Azuma Kagami and the Legends of Prince Shotoku
- Allogeneic Bone Marrow Transplantation as a Therapeutic Modality for Hematological Disorders : A Report Based on 39 Cases
- Fractal Structure and Statistics of Computer-simulated and Real Landforms(Cross-disciplinary physics and related areas of science and technology)
- Fabrication of GaN/Alumina/GaN Structure to Reduce Dislocations in GaN
- Association of the Japanese Orthopaedic Association Score With the Oswestry Disability Index, Roland-Morris Disability Questionnaire, and Short-Form 36
- Novel Degradation of Sugar Skeleton by Diazidation
- Photoacoustic and Photoelectrochemical Characterization of Inverse Opal TiO_2 Sensitized with CdSe Quantum Dots
- Intravenous gamma-globulin therapy improves hypercytokinemia in the acute phase of Kawasaki disease
- Phosphory lated Sites of M_r 25,000 Protein, a Putative Protein Phosphatase 2A Modulator, and Phosphorylation of the Synthetic Peptide Containing These Sites by Protein Kinase C^1
- Modelling and Numerical Analysis of the Colony Formation of Bacteria
- Effect of EOS on Break-Up of Shoemaker-Levy 9 Entering Jovian Atmosphere
- Dynamic Scaling of the Growing Rough Surfaces(General)
- Morphologic Changes in the Cervical Neural Foramen due to Flexion and Extension : In Vivo Imaging Study
- D-galactosamine/Lipopolysaccharide による肝障害モデルで cytochrome c はミトコンドリアから細胞質そして循環血液中へ移行する
- Effect of a Platelet-Activating Factor Receptor Antagonist, E5880, on Cerebral Vasospasm after Aneurysmal Subarachnoid Hemorrhage : Open Clinical Trial to Investigate Efficacy and Safety
- 1P096 Long time folding simulations of a three-stranded antiparallel β-sheet peptide and a ββα-folded peptide(3. Protein folding and misfolding (I),Poster Session,Abstract,Meeting Program of EABS & BSJ 2006)
- Electric Characteristics of Li2O-Doped TiO2 Nanocrystalline Film and Its Application to Dye-Sensitized Solar Cells
- Room-Temperature Absorption Edge of InGaN/GaN Quantum Wells Characterized by Photoacoustic Measurement
- Reduction of Acyl Enolates of α-Substituted β-Keto Esters by Bakers' Yeast(Organic Chemistry)
- TOWARDS OBJECT ORIENTED CONCURRENT PROGRAMMING(Software Science and Engineering)
- A Complete Type Inference System for Subtyped Recursive Types
- Comments on Monitors and Path-Expressions
- Concurrent Programming in Linear Logic
- Verification of Concurrent Programs Using the Coq Proof Assistant : A Case Study
- EFFECT OF KANJI AND KANA READING ON CEREBRAL BLOOD FLOW PATTERNS MEASURED BY PET
- Hydrogen Evolution from p-GaN Cathode in Water under UV Light Irradiation
- Influence of Thickeners on the Fragmentation of Fish Meat Sausage by Mastication
- p-GaN Cathode Degradation Correlated with Hydrogen Passivation during Water Photolysis under UV Light
- Fractal Structure of Isothermal Lines and Loops on the Cosmic Microwave Background
- Repeated donor lymphocyte infusions overcome a myeloid sarcoma of the stomach resulting from a relapse of acute myeloid leukemia after allogeneic cell transplantation in long-term survival of more than 10 years
- Comparison of Forward and Reverse Reactions in Hydrogen Generation between GaN, InGaN, Nanocrystalline TiO2 and Pt Electrodes during Water Electrolysis
- Characterization of Conduction Band Offset in Nanocrystalline TiO2/p-InGaN for Application to Water Photolysis Using Visible Light
- An Incremental Variational Principle Minimizing Experimental Measurement Errors and Its Application to an Intelligent Hybrid Experimental-Numerical Method : Case of Nonlinear Elastic-Plastic Deformation Field
- Outcome of medium-dose VP-16/CY/TBI superior to CY/TBI as a conditioning regimen for allogeneic stem cell transplantation in adult patients with acute lymphoblastic leukemia
- Design and Implementation of A Highly Modularized Functional language
- Influence of Thickeners on the Fragmentation of Fish Meat Sausage by Mastication
- Fragmentation of a Viscoelastic Food by Human Mastication
- Multi-Affinity for Growing Rough Interfaces of Bacterial Colonies
- Statistical Features of Complex Systems ---Toward Establishing Sociological Physics---
- Crystal Growth of CdSe Quantum Dots Adsorbed on Nanoparticle, Inverse Opal, and Nanotube TiO2 Photoelectrodes Characterized by Photoacoustic Spectroscopy
- Effect of Ligand Carboxylation on Adsorption and Photosensitization in Ru(II)-Complex Dye-Sensitized Nanocrystalline TiO2 Solar Cell
- Simultaneous Monitoring of Hydrogen Generation and Flat-Band Potential by Measuring Bias Dependent Photoluminescence of n-Type GaN/Electrolyte System
- Monophotonic ionization mechanism of N,N,N',N'-tetramethyl-1,6-pyrenediamine in acetonitrile solution.
- Verification of Concurrent Programs Using the Coq Proof Assistant: A Case Study
- A Comparative Study of Mobilization Efficiency with Three Regimens to Harvest Peripheral Blood Stem Cells(Symposium 1: Stem Cell Harvest)