Z

swMATH10291MaRDI QIDQ22253FDOQ22253

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• A temporal logic for real-time partial ordering with named transactions
• Model-based specification
• A relational approach to an algebraic community: from Paul Erdős to He Jifeng
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Mini-workshop: Chromatic phenomena and duality in homotopy theory and representation theory. Abstracts from the mini-workshop held March 4--10, 2018
• 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
• Towards leveraging domain knowledge in state-based formal methods
• Spot the difference: a detailed comparison between B and Event-B
• Software Development in Relation Algebra with Ampersand
• Unifying theories of reactive design contracts
• Sound reasoning in \textit{tock}-CSP
• Manipulating algebraic specifications with term-based and graph-based representations
• A new roadmap for linking theories of programming
• Fifty years of Hoare's logic
• Circus Time with Reactive Designs
• ZUM '95: The Z formal specification notation. 9th International Conference of Z Users, Limerick, Ireland, September 7-9, 1995. Proceedings
• A formal model of explanation
• Angelic processes for CSP via the UTP
• RCOS: a formal model-driven engineering method for component-based software
• Override and update
• Simulink timed models for program verification
• Curves and Jacobians over function fields
• A theory of Orwellian specifications with NewThink
• Automated proof of Bell-LaPadula security properties
• Loop invariants: analysis, classification, and examples
• From Boolean algebra to unified algebra
• A blocking model for reactive objects
• The consistency theorem for free type definitions in \(Z\)
• Relation algebra as programming language using the Ampersand compiler
• Unifying models
• A stepwise approach to linking theories
• \textsc{Conjure}: automatic generation of constraint models from problem specifications
• An abstract model for proving safety of autonomous urban traffic
• An abstract model for proving safety of autonomous urban traffic
• Special issue: Perturbation methods and formal modeling for dynamic systems
• Proving safety of traffic manoeuvres on country roads
• No need knowing numerous neighbours. Towards a realizable interpretation of MLSL
• Unifying theories of programming in Isabelle
• From relational specifications to logic programs
• Stepwise refinement of heap-manipulating code in Chalice
• A sound and complete proof technique for linearizability of concurrent data structures
• Designing a semantic model for a wide-spectrum language with concurrency
• Combining relation algebra and data refinement to develop rectangle-based functional programs for reflexive-transitive closures
• Why mathematics needs engineering
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• An automatically verified prototype of the Tokeneer ID station specification
• Using semantic correctness in multidatabases to achieve local autonomy, distribute coordination, and maintain global integrity
• Model-Based Testing for Functional and Security Test Generation
• Richer types for \(Z\)
• Safety-critical Java programs from \textsf{Circus} models
• Automated reasoning with restricted intensional sets
• Automated verification of reactive and concurrent programs by calculation
• Unification: A case-study in data refinement
• An Event-B based approach for cloud composite services verification
• Modelling Divergence in Relational Concurrent Refinement
• A case study in transformational design of concurrent systems
• A logical system based on rules and its application in teaching mathematical logic
• Laws of mission-based programming
• Guarded operations, refinement and simulation
• Verifying a signature architecture: a comparative case study
• The seven virtues of simple type theory
• Abstract interface behavior of object-oriented languages with monitors
• Verifying data refinements using a model checker
• A theory of software product line refinement
• Generalising the array split obfuscation
• Refinement and verification in component-based model-driven design
• Transformational vs reactive refinement in real-time systems
• Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository
• The formal specification of abstract data types and their implementation in Fortran 90
• On using data abstractions for model checking refinements
• Object oriented concepts identification from formal \(B\) specifications
• An operational semantics for object-oriented concepts based on the class hierarchy
• Compensation by design
• Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
• On integrating confidentiality and functionality in a formal method
• Introducing extra operations in refinement
• Relational concurrent refinement. III: Traces, partial relations and automata
• Test-data generation for control coverage by proof
• FDR explorer
• Model checking action system refinements
• Semantics, calculi, and analysis for object-oriented specifications
• Mobile agent evolution computing
• BOX: Browsing objects in XML
• Correct hardware synthesis
• Categorical foundations for structured specifications in \(\mathsf{Z}\)
• Using formal reasoning on a model of tasks for FreeRTOS
• Annotations in formal specifications and proofs
• More relational concurrent refinement: traces and partial relations
• Satisfiability in composition-nominative logics
• VDM and Z: A comparative case study
• Multi-relations in Z. A cross between multi-sets and binary relations
• Defining relationships in ecology using object-oriented formal specifications
• A process algebraic framework for specification and validation of real-time systems
• A calculus for schemas in Z
• A formal framework for modeling and validating simulink diagrams
• Atomic actions, and their refinements to isolated protocols
• Semantic inheritance in unifying theories of programming
• Preservation of probabilistic information flow under refinement
• Unifying theories in ProofPower-Z

This page was built for software: Z