Z

swMATH10291MaRDI QIDQ22253

No author found.

Related Items (only showing first 100 items - show all)

Modelling and analysing neural networks using a hybrid process algebra ⋮ Components as coalgebras: the refinement dimension ⋮ An Event-B based approach for cloud composite services verification ⋮ Annotations in formal specifications and proofs ⋮ On definitions of constants and types in HOL ⋮ A fixpoint theory for non-monotonic parallelism ⋮ Manipulating algebraic specifications with term-based and graph-based representations ⋮ Defining relationships in ecology using object-oriented formal specifications ⋮ From Boolean algebra to unified algebra ⋮ Transformational vs reactive refinement in real-time systems ⋮ The formal specification of abstract data types and their implementation in Fortran 90 ⋮ Verifying data refinements using a model checker ⋮ An analysis of refinement in an abortive paradigm ⋮ Transposing partial components--an exercise on coalgebraic refinement ⋮ Property transformation under specification change ⋮ Generalising the array split obfuscation ⋮ Special issue: Perturbation methods and formal modeling for dynamic systems ⋮ Verifying a signature architecture: a comparative case study ⋮ Determinisation of relational substitutions in ordered categories with domain ⋮ On using data abstractions for model checking refinements ⋮ Incompleteness of relational simulations in the blocking paradigm ⋮ Object oriented concepts identification from formal \(B\) specifications ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ A temporal logic for real-time partial ordering with named transactions ⋮ Relating trace refinement and linearizability ⋮ Categorical foundations for structured specifications in \(\mathsf{Z}\) ⋮ Using formal reasoning on a model of tasks for FreeRTOS ⋮ Mechanised support for sound refinement tactics ⋮ Experiments in program verification using Event-B ⋮ Model evolution and refinement ⋮ Mechanical reasoning about families of UTP theories ⋮ JCML: A specification language for the runtime verification of Java card programs ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Refinement-oriented models of Stateflow charts ⋮ From control law diagrams to Ada via \textsf{Circus} ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Domain science and engineering from computer science to the sciences of informatics. II: Science ⋮ Model checking RAISE applicative specifications ⋮ Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types ⋮ Refinement modal logic ⋮ Data refinement and singleton failures refinement are not equivalent ⋮ Test selection for traces refinement ⋮ Spectral structures and topological methods in mathematical quasicrystals. Abstracts from the workshop held October 1--7, 2017 ⋮ Working session: Additive combinatorics, entropy, and fractal geometry. Abstracts from the working session held October 8--13, 2017 ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Computability theory. Abstracts from the workshop held January 7--13, 2018 ⋮ Mini-workshop: Chromatic phenomena and duality in homotopy theory and representation theory. Abstracts from the mini-workshop held March 4--10, 2018 ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ 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 ⋮ Manifest domains: analysis and description ⋮ Angelic processes for CSP via the UTP ⋮ A heuristic method for generating large random expressions ⋮ RCOS: a formal model-driven engineering method for component-based software ⋮ Z2SAL: a translation-based model checker for Z ⋮ On the purpose of Event-B proof obligations ⋮ A process algebraic framework for specification and validation of real-time systems ⋮ Completeness of fair ASM refinement ⋮ A tactic language for refinement of state-rich concurrent specifications ⋮ Formalisations and applications of BPMN ⋮ A semantics for behavior trees using CSP with specification commands ⋮ The axiomatization of override and update ⋮ ASM refinement and generalizations of forward simulation in data refinement: a comparison ⋮ Abstract state machines: a unifying view of models of computation and of system design frameworks ⋮ A theory of software product line refinement ⋮ A timeband framework for modelling real-time systems ⋮ Finding models through graph saturation ⋮ Relation algebra as programming language using the Ampersand compiler ⋮ An abstract model for proving safety of autonomous urban traffic ⋮ Refinement and verification in component-based model-driven design ⋮ 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 ⋮ Test-data generation for control coverage by proof ⋮ On integrating confidentiality and functionality in a formal method ⋮ The behavioural semantics of Event-B refinement ⋮ Introducing extra operations in refinement ⋮ Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application ⋮ Relational concurrent refinement. III: Traces, partial relations and automata ⋮ HasCasl: integrated higher-order specification and program development ⋮ Abstract interface behavior of object-oriented languages with monitors ⋮ A UTP semantics for \textsf{Circus} ⋮ Model checking action system refinements ⋮ Relational concurrent refinement. II: Internal operations and outputs ⋮ FDR explorer ⋮ Trace-based derivation of a scalable lock-free stack algorithm ⋮ Richer types for \(Z\) ⋮ Testing for refinement in \textsf{Circus} ⋮ Correct hardware synthesis ⋮ A formal framework for modeling and validating simulink diagrams ⋮ Decidable fragments of many-sorted logic ⋮ A calculus for schemas in Z ⋮ Mobile agent evolution computing ⋮ Model-based specification ⋮ FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY ⋮ Sound reasoning in \textit{tock}-CSP

This page was built for software: Z