scientific article

Publication date: 17 September 1992

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Classical first-order logic (03B10) General topics in the theory of software (68N01) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science (68-00)

Related Items

Software Development in Relation Algebra with Ampersand, A case study in transformational design of concurrent systems, Unifying models, Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras, A completeness proof for a regular predicate logic with undefined truth value, An automatically verified prototype of the Android permissions system, A declarative approach to graph based modeling, Action systems in incremental and aspect-oriented modeling, Completeness of ASM Refinement, General Refinement, Part One: Interfaces, Determinism and Special Refinement, Alloy as a Refactoring Checker?, A Conceptual and Formal Framework for the Integration of Data Type and Process Modeling Techniques, Refinement-Preserving Plug-In Components, Verified Compilation and the B Method: A Proposal and a First Appraisal, A formal software development approach using refinement calculus, Reliable agent communication -- a pragmatic perspective, Using semantic correctness in multidatabases to achieve local autonomy, distribute coordination, and maintain global integrity, Compositionality: Ontology and Mereology of Domains, Unnamed Item, Extended Static Checking by Calculation Using the Pointfree Transform, Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}, Verifying Opacity of a Transactional Mutex Lock, Model-Based Testing for Functional and Security Test Generation, An Institution for Object-Z with Inheritance and Polymorphism, Understanding, Explaining, and Deriving Refinement, Modelling and analysing neural networks using a hybrid process algebra, FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY, Components as coalgebras: the refinement dimension, Formal software development in the Verification Support Environment (VSE), Formal specification synthesis for relational database model, Impact of performance considerations on formal specification design, Annotations in formal specifications and proofs, On definitions of constants and types in HOL, Defining relationships in ecology using object-oriented formal specifications, Invariant-driven specifications in Maude, Why mathematics needs engineering, From Boolean algebra to unified algebra, Selected MRP II Standard System requirements presented in Z‐notation, Levels of abstraction and the Turing test, Transformational vs reactive refinement in real-time systems, The formal specification of abstract data types and their implementation in Fortran 90, Unification: A case-study in data refinement, A formal model of explanation, Specification by interface separation, Interpreting message flow graphs, Semantics, calculi, and analysis for object-oriented specifications, On simulation, subtyping and substitutability in sequential object systems, A theory of Orwellian specifications with NewThink, Generalising the array split obfuscation, Verifying data- and control-oriented properties combining static and runtime verification: theory and tools, Model Checking Simulation Rules for Linearizability, A blocking model for reactive objects, The consistency theorem for free type definitions in \(Z\), On using data abstractions for model checking refinements, Stochastic modelling of diffusion equations on a parallel machine, Automated reasoning with restricted intensional sets, Designing a semantic model for a wide-spectrum language with concurrency, rCOS: Defining Meanings of Component-Based Software Architectures, A temporal logic for real-time partial ordering with named transactions, Determinisation of Relational Substitutions in Ordered Categories with Domain, Decidable Fragments of Many-Sorted Logic, Relating trace refinement and linearizability, Adding partial functions to Constraint Logic Programming with sets, Composition mechanisms for retrenchment, Categorical foundations for structured specifications in \(\mathsf{Z}\), Using formal reasoning on a model of tasks for FreeRTOS, Override and update, Model evolution and refinement, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, A Stepwise Approach to Linking Theories, A reification calculus for model-oriented software specification, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, Satisfiability in composition-nominative logics, Relational matching for graphical calculi of relations, Model checking RAISE applicative specifications, Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types, Guarded Operations, Refinement and Simulation, VDM and Z: A comparative case study, Multi-relations in Z. A cross between multi-sets and binary relations, The seven virtues of simple type theory, Higher-order equational logic for specification, simulation and testing, A metric for evaluating software architecture and communication models consistency, A heuristic method for generating large random expressions, Preservation of probabilistic information flow under refinement, Completeness of fair ASM refinement, A tactic language for refinement of state-rich concurrent specifications, Unifying theories of reactive design contracts, A note on the refinement of ontologies, A semantics for behavior trees using CSP with specification commands, Conservative extension concepts for nonmonotonic knowledge bases, The axiomatization of override and update, ASM refinement and generalizations of forward simulation in data refinement: a comparison, A theory of software product line refinement, Formalization of the UML Class Diagrams, Concept Management: Identification and Storage of Concepts in the Focus of Formal Z Specifications, Finding models through graph saturation, Relation algebra as programming language using the Ampersand compiler, Fifty years of Hoare's logic, Automated proof of Bell-LaPadula security properties, Modelling of Complex Software Systems: A Reasoned Overview, Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository, Mechanising a formal model of flash memory, POSIX file store in Z/Eves: An experiment in the verified software repository, An operational semantics for object-oriented concepts based on the class hierarchy, Compensation by design, HasCasl: integrated higher-order specification and program development, Automated verification of reactive and concurrent programs by calculation, Isabelle/UTP: A Mechanised Theory Engineering Framework, Abstract interface behavior of object-oriented languages with monitors, Trace-based derivation of a scalable lock-free stack algorithm, Z, Richer types for \(Z\), Integration of formal proof into unified assurance cases with Isabelle/SACM, An automatically verified prototype of the Tokeneer ID station specification, Decidable fragments of many-sorted logic, A calculus for schemas in Z, Semantic essence of AsmL, Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures, From Predicates to Programs: The Semantics of a Method Language, Mobile agent evolution computing, Viewing CSP Specifications with UML-RT Diagrams, Type Checking Specifications, Domain-specific Semantics and Data Refinement of Object Models, Model-based specification, Spot the difference: a detailed comparison between B and Event-B