scientific article

From MaRDI portal
Publication:3997074

zbMath0743.68048MaRDI QIDQ3997074

Cliff B. Jones

Publication date: 17 September 1992


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



Related Items (75)

Modelling and analysing neural networks using a hybrid process algebraImpact of performance considerations on formal specification designProof movie -- a proof with the Boyer-Moore proverConstraining interference in an object-based design methodObject organisation in software environments for formal methodsInvariant-driven specifications in MaudePossible values: exploring a concept for concurrencyNatural 3-valued logics—characterization and proof theoryPanelist position statement: reasoning about the design of programsIntegrating formal specifications into applications: the ProB Java APIProof by analogy in muralReasoning About Resources in the Embedded Systems Language HumeAn analysis of refinement in an abortive paradigmSpecification by interface separationApplying abstraction and formal specification in numerical software designSemantics, calculi, and analysis for object-oriented specificationsOn simulation, subtyping and substitutability in sequential object systemsA theory of Orwellian specifications with NewThinkA generalization of ACP using Belnap's logicSemantics of under-determined expressionsAn approach to literate and structured formal developmentsReachability analysis and simulation for hybridised Event-B modelsSpecification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigmSound and complete rules for data reificationCompositional verification of real-time systems with explicit clock temporal logicSplitting atoms safelyRelations as abstract datatypes: An institution to specify relations between algebrasrCOS: Defining Meanings of Component-Based Software ArchitecturesA temporal logic for real-time partial ordering with named transactionsInvestigating the limits of rely/guarantee relations based on a concurrent garbage collector exampleBalancing expressiveness in formal approaches to concurrencyRefining privacy-aware data flow diagramsReview of Understanding Programming LanguagesTemporal-logic property preservation under Z refinementA functional framework for agent-based models of exchangeExperiments in program verification using Event-BConnectors as designs: modeling, refinement and test case generationDeriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of controlA Practical Single Refinement Method for BSplitting Atoms with Rely/Guarantee Conditions Coupled with Data ReificationProving Quicksort Correct in Event-BAutomating Event-B invariant proofs by rippling and proof patchingBridging arrays and ADTs in recursive proofsModular structuring of VDM specifications in VVSLMulti-relations in Z. A cross between multi-sets and binary relationsA program logic for resourcesLinking Event-B and Concurrent Object-Oriented ProgramsService refinementModeling and visualizing object-oriented programs with CodechartsAn empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systemsModel-Checking View-Based Partial SpecificationsThe connection between two ways of reasoning about partial functionsPreservation of probabilistic information flow under refinementElucidating concurrent algorithms via layers of abstraction and reificationA Superposition Operator for the Refinement of Algebraic ModelsPartiality and recursion in interactive theorem provers – an overviewA semantics for behavior trees using CSP with specification commandsASM refinement and generalizations of forward simulation in data refinement: a comparisonUnnamed ItemUnnamed ItemRefinement and state machine abstractionRefinement and verification in component-based model-driven designAn operational semantics for object-oriented concepts based on the class hierarchyOn integrating confidentiality and functionality in a formal methodHasCasl: integrated higher-order specification and program developmentProcess algebra with four-valued logicHoare's logic and VDMRelational DecompositionMechanical Software VerificationOurs Is to Reason WhyAXIOMATIC FRAMEWORKS FOR DEVELOPING BSP-STYLE PROGRAMS∗Specifications in stochastic process algebra for a robot control problemA Generalization of ACP Using Belnap's LogicFormally verified tableau-based reasoners for a description logicReasoning about Separation Using Abstraction and Reification




This page was built for publication: