scientific article; zbMATH DE number 605917
From MaRDI portal
Publication:4301167
Recommendations
- Refactoring in maintenance and development of Z specifications and proofs
- scientific article; zbMATH DE number 50069
- The specification logic \(\nu\mathsf{Z}\)
- Automated Technology for Verification and Analysis
- The specification logic \(\nu \)Z
- scientific article; zbMATH DE number 795671
- scientific article; zbMATH DE number 977451
- Specifying and refining internal operations in \(Z\)
- scientific article; zbMATH DE number 2080003
- Refinement and the Z schema calculus
Cited in
(only showing first 100 items - show all)- 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
- POSIX file store in Z/Eves: An experiment in the verified software repository
- A UTP semantics for \textsf{Circus}
- Relational concurrent refinement. II: Internal operations and outputs
- FDR explorer
- A formal framework for modeling and validating simulink diagrams
- ZRC -- A refinement calculus for Z
- A calculus for schemas in Z
- Special issue: Perturbation methods and formal modeling for dynamic systems
- Designing a semantic model for a wide-spectrum language with concurrency
- Angelic processes for CSP via the UTP
- Abstract state machines: a unifying view of models of computation and of system design frameworks
- An abstract model for proving safety of autonomous urban traffic
- Temporal-logic property preservation under Z refinement
- Stepwise refinement of heap-manipulating code in Chalice
- Unifying theories in ProofPower-Z
- Moded and continuous abstract state machines
- Sound reasoning in \textit{tock}-CSP
- \textsc{Conjure}: automatic generation of constraint models from problem specifications
- Modelling temporal behaviour in complex systems with Timebands
- Extended transitive separation logic
- Laws of mission-based programming
- Efficient symbolic computation of process expressions
- Semantics, calculi, and analysis for object-oriented specifications
- Composition mechanisms for retrenchment
- Safety-critical Java programs from \textsf{Circus} models
- Domain science and engineering from computer science to the sciences of informatics. I: Engineering
- A formal framework for Hybrid Event B
- Automated reasoning with restricted intensional sets
- Towards Algebraic Semantics of Circus Time
- Simulink timed models for program verification
- Proving safety of traffic manoeuvres on country roads
- Type checking \textsf{Circus} specifications
- Generic tools via general refinement
- A sound and complete proof technique for linearizability of concurrent data structures
- Unifying theories of programming in Isabelle
- A stepwise approach to linking theories
- Relational concurrent refinement: automata
- On the semantics of unified modeling language diagrams using Z notation
- Behavioural models for FMI co-simulations
- An abstract model for proving safety of autonomous urban traffic
- No need knowing numerous neighbours. Towards a realizable interpretation of MLSL
- Circus Time with Reactive Designs
- Lazy Relations
- Property transformation under specification change
- On the Purpose of Event-B Proof Obligations
- A Practical Single Refinement Method for B
- Modelling Divergence in Relational Concurrent Refinement
- An observationally complete program logic for imperative higher-order functions
- 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
- Refinement-oriented models of Stateflow charts
- Putting logic-based distributed systems on stable grounds
- Domain science and engineering from computer science to the sciences of informatics. II: Science
- Model checking RAISE applicative specifications
- Refinement modal logic
- Test selection for traces refinement
- scientific article; zbMATH DE number 795671 (Why is no real title available?)
- A Unary Semigroup Trace Algebra
- A relative timed semantics for BPMN
- Stateflow diagrams in Circus
- Specification and runtime verification of Java card programs
- Checking Z Data Refinements Using Traces Refinement
- Compositionality: ontology and mereology of domains. Some clarifying observations in the context of software engineering
- Extended Static Checking by Calculation Using the Pointfree Transform
- Manifest domains: analysis and description
- On the purpose of Event-B proof obligations
- Completeness of ASM refinement
- More relational concurrent refinement: traces and partial relations
- General refinement. I: Interfaces, determinism and special refinement
- Completeness of fair ASM refinement
- A tactic language for refinement of state-rich concurrent specifications
- Formalisations and applications of BPMN
- ASM refinement and generalizations of forward simulation in data refinement: a comparison
- Understanding, Explaining, and Deriving Refinement
- Sound and relaxed behavioural inheritance
- Testing using CSP Models: Time, Inputs, and Outputs
- Refinement and state machine abstraction
- Type inference for set theory
- Refining privacy-aware data flow diagrams
- Incompleteness of relational simulations in the blocking paradigm
- Automatic generation of verified concurrent hardware using VHDL
- Spatial and timing properties in highway traffic
- From control law diagrams to Ada via \textsf{Circus}
- Evolution of Formal Model-Based Assurance Cases for Autonomous Robots
- UTP, \textsf{\textit{Circus}}, and Isabelle
- Domain modelling: a foundation for software development
- Towards a model-checker for \textit{\textsf{Circus}}
- \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
- Extending rely-guarantee thinking to handle real-time scheduling
- Modelling and verifying robotic software that uses neural networks
- Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
- Multifaceted formal methods and their interdisciplinary role -- from the cathedral of `components as coalgebras' to the HCI context and the open source software bazaar
- A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
- Automating Event-B invariant proofs by rippling and proof patching
- Formal verification of BDI agents
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4301167)
