scientific article
From MaRDI portal
Publication:3997074
zbMath0743.68048MaRDI QIDQ3997074
Publication date: 17 September 1992
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)
Related Items (75)
Modelling and analysing neural networks using a hybrid process algebra ⋮ Impact of performance considerations on formal specification design ⋮ Proof movie -- a proof with the Boyer-Moore prover ⋮ Constraining interference in an object-based design method ⋮ Object organisation in software environments for formal methods ⋮ Invariant-driven specifications in Maude ⋮ Possible values: exploring a concept for concurrency ⋮ Natural 3-valued logics—characterization and proof theory ⋮ Panelist position statement: reasoning about the design of programs ⋮ Integrating formal specifications into applications: the ProB Java API ⋮ Proof by analogy in mural ⋮ Reasoning About Resources in the Embedded Systems Language Hume ⋮ An analysis of refinement in an abortive paradigm ⋮ Specification by interface separation ⋮ Applying abstraction and formal specification in numerical software design ⋮ Semantics, calculi, and analysis for object-oriented specifications ⋮ On simulation, subtyping and substitutability in sequential object systems ⋮ A theory of Orwellian specifications with NewThink ⋮ A generalization of ACP using Belnap's logic ⋮ Semantics of under-determined expressions ⋮ An approach to literate and structured formal developments ⋮ Reachability analysis and simulation for hybridised Event-B models ⋮ Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm ⋮ Sound and complete rules for data reification ⋮ Compositional verification of real-time systems with explicit clock temporal logic ⋮ Splitting atoms safely ⋮ Relations as abstract datatypes: An institution to specify relations between algebras ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ A temporal logic for real-time partial ordering with named transactions ⋮ Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Refining privacy-aware data flow diagrams ⋮ Review of Understanding Programming Languages ⋮ Temporal-logic property preservation under Z refinement ⋮ A functional framework for agent-based models of exchange ⋮ Experiments in program verification using Event-B ⋮ Connectors as designs: modeling, refinement and test case generation ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ A Practical Single Refinement Method for B ⋮ Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification ⋮ Proving Quicksort Correct in Event-B ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Modular structuring of VDM specifications in VVSL ⋮ Multi-relations in Z. A cross between multi-sets and binary relations ⋮ A program logic for resources ⋮ Linking Event-B and Concurrent Object-Oriented Programs ⋮ Service refinement ⋮ Modeling and visualizing object-oriented programs with Codecharts ⋮ An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems ⋮ Model-Checking View-Based Partial Specifications ⋮ The connection between two ways of reasoning about partial functions ⋮ Preservation of probabilistic information flow under refinement ⋮ Elucidating concurrent algorithms via layers of abstraction and reification ⋮ A Superposition Operator for the Refinement of Algebraic Models ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ A semantics for behavior trees using CSP with specification commands ⋮ ASM refinement and generalizations of forward simulation in data refinement: a comparison ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Refinement and state machine abstraction ⋮ Refinement and verification in component-based model-driven design ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ On integrating confidentiality and functionality in a formal method ⋮ HasCasl: integrated higher-order specification and program development ⋮ Process algebra with four-valued logic ⋮ Hoare's logic and VDM ⋮ Relational Decomposition ⋮ Mechanical Software Verification ⋮ Ours Is to Reason Why ⋮ AXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗ ⋮ Specifications in stochastic process algebra for a robot control problem ⋮ A Generalization of ACP Using Belnap's Logic ⋮ Formally verified tableau-based reasoners for a description logic ⋮ Reasoning about Separation Using Abstraction and Reification
This page was built for publication: