Sciweavers

MPC
1995
Springer
91views Mathematics» more  MPC 1995»
14 years 2 months ago
A Refinement Relation Supporting the Transition from Unbounded to Bounded Communication Buffers
This paper proposes a refinement relation supporting the transition from unbounded to bounded communication buffers. Employing this refinement relation, a system specification base...
Ketil Stølen
MPC
1995
Springer
116views Mathematics» more  MPC 1995»
14 years 2 months ago
Computer-Aided Computing
PVS is a highly automated framework for speci cation and veri cation. We show how the language and deduction features of PVS can be used to formalize, mechanize, and apply some us...
Natarajan Shankar
MPC
1995
Springer
93views Mathematics» more  MPC 1995»
14 years 2 months ago
Extracting Programs with Exceptions in an Impredicative Type System
Abstract. This paper is about exceptions handling using classical techniques of program extraction. We propose an impredicative formalization in the calculus of constructions and w...
Jean-François Monin
MPC
1995
Springer
125views Mathematics» more  MPC 1995»
14 years 2 months ago
Synthesizing Proofs from Programs in the Calculus of Inductive Constructions
We want to prove \automatically" that a program is correct with respect to a set of given properties that is a speci cation. Proofs of speci cations contain logical parts and ...
Catherine Parent
MPC
1995
Springer
150views Mathematics» more  MPC 1995»
14 years 2 months ago
Architecture Independent Massive Parallelization of Divide-and-Conquer Algorithms
Abstract. We present a strategy to develop, in a functional setting, correct, e cient and portable Divide-and-Conquer (DC) programs for massively parallel architectures. Starting f...
Klaus Achatz, Wolfram Schulte