Formal Aspects of Computing, Volume 4

Volume 4, Number 1, 1992

C. A. Middelburg: Modular Structuring of VDM Specifications in VVSL. 13-47 BibTeX
Chris George: The NDB Database Specified in the RAISE Specification Language. 48-75 BibTeX
Ian J. Hayes: VDM and Z: A Comparative Case Study. 76-99 BibTeX , further work
Edmund Kazmierczak: Modularising the Specification of a Small Database System in Extended ML. 100-142 BibTeX

Parosh Aziz Abdulla: Automatic Verification of a Class Systolic Circuits. 149-194 BibTeX
Johan J. Lukkien, Jan L. A. van de Snepscheut: Weakest Preconditions for Progress. 195-236 BibTeX

José Luiz Fiadeiro, T. S. E. Maibaum: Temporal Theories as Modularisation Units for Concurrent System Specification. 239-272 BibTeX
James H. Anderson, Mohamed G. Gouda: A Criterion for Atomicity. 273-298 BibTeX
Michael Fisher: A Model Checker for Linear Time Temporal Logic. 299-319 BibTeX

Olaf Owe: Axiomatic Treatment of Processes with shared Variables Revisited. 323-340 BibTeX , further work
Heinz Faßbender, Heiko Vogler: An Implementation of Syntax Directed Functional Programming on Nested-Stack Machines. 341-375 BibTeX
Pierre America, Jan J. M. M. Rutten: A Layered Semantics for a Parallel Object-Oriented Language. 376-408 BibTeX

Lambert G. L. T. Meertens: Paramorphisms. 413-424 BibTeX
Jonathan P. Seldin: Coquand's Calculus of Constructions: A Mathematical Foundation for a Proof Development System. 425-441 BibTeX , further work
Zhiming Liu, Mathai Joseph: Transformation of Programs for Fault-Tolerance. 442-469 BibTeX , further work
J. Roger Hindley: Types with Intersection: An Introduction. 470-486 BibTeX , further work
Andrew Kay, Peter Lupton: Sequential to Parallel Buffer Refinement (Short Communication). 487-492 BibTeX

Fredrik Orava, Joachim Parrow: An Algebraic Verification of a Mobile Network. 497-543 BibTeX
Noureddine Boudriga, Fathi Elloumi, Ali Mili: On the Lattice of Specifications: Applications to a Specification Methodology. 544-571 BibTeX
Eike Best, Ludmila Cherkasova, Jörg Desel: Compositional Generation of Home States in Free Choice Nets. 572-581 BibTeX
Nissim Francez, Ralph-Johan Back, Reino Kurki-Suonio: On Equivalence-Completions of Fairness Assumtions. 582-591 BibTeX

David M. Russinoff: A Verification System for Current Programs Based on the Boyer-Moore Prover. 597-611 BibTeX
Lucia Pomello, Carla Simone: An Algebraic Characterisation of Elementary Net System (Observable) State Space. 612-637 BibTeX
José L. Balcázar, Joaquim Gabarró, Miklos Santha: Deciding Bisimilarity is P-Complete. 638-648 BibTeX
M. W. Shields: Multitraces, Hypertraces and Partial Order Semantics. 649-672 BibTeX
Maarten M. Fokkinga: Calculate Categorically! 673-692 BibTeX
C. T. P. Burton: Program Morphisms. 693-726 BibTeX
Masaaki Mizuno, David A. Schmidt: A Security Flow Control Algorithm and Its Denotational Semantics Correctness Proof. 727-754 BibTeX
William R. Bevier, William D. Young: Machine Checked Proofs of the Design of a Fault-Tolerance Circuit. 755-775 BibTeX
Jeroen Fokker: The Systematic Construction of a One-Combinator Basis for Lambda-Terms. 776-780 BibTeX