UNITY

From MaRDI portal
Revision as of 20:24, 5 March 2024 by Import240305080343 (talk | contribs) (Created automatically from import240305080343)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Software:25375



swMATH13461MaRDI QIDQ25375


No author found.





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

Conditional rewriting logic: Deduction, models and concurrencyComposite registersDistributed maximum maintenance on hierarchically divided graphsA case study in transformational design of concurrent systemsConstraining interference in an object-based design methodApplication of the composition principle to unity-like specificationsProperty preserving abstractions under parallel compositionGeneric systolic arrays: A methodology for systolic designA verification framework for agent programming with declarative goalsTemporal Logic and Fair Discrete SystemsCombining Model Checking and DeductionOn the correctness of a distributed memory Gröbner basis algorithmUnnamed ItemInvariants, composition, and substitutionConstructive Polychronous SystemsA Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based ProtocolsA new explanation of the glitch phenomenonBounded delay for a free addressDUALITY: A simple formalism for the analysis of UNITYApplying abstraction and formal specification in numerical software designSpecification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigmSuperposition refinement of reactive systemsProgram composition via unificationGeneric Proof Scores for Generate & Check Method in CafeOBJTournaments for mutual exclusion: verification and concurrent complexityrCOS: Defining Meanings of Component-Based Software ArchitecturesSimulation relations for fault-toleranceA framework for automated distributed implementation of component-based modelsUsing refinement calculus techniques to prove linearizabilitySecurity invariants in discrete transition systemsComputing with multiple discrete flowsPreserving stabilization while \textit{practically} bounding state space using incorruptible partially synchronized clocksConcurrent maintenance of ringsCompositional Verification for Component-Based Systems and ApplicationAdaptive solutions to the mutual exclusion problemNaming symmetric processes using shared variablesWait-free linearization with an assertional proofWait-free linearization with a mechanical proofA fast, scalable mutual exclusion algorithmKnowledge-based programsAutomatic verification for a class of distributed systemsA note on knowledge-based programs and specificationsAsynchronous group mutual exclusionSafety assurance via on-line monitoringUnnamed ItemFormal Reasoning About Causality AnalysisDecidability of a partial order based temporal logicReasoning about programs by exploiting the environmentDistributed consensus, revisitedKnowledge-Based Synthesis of Distributed Systems Using Event StructuresFormalism and methodTowards a Combination of CafeOBJ and PATTheorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSsAn Algebraic Approach to Refinement with Fair ChoiceA Rewriting-Based Model Checker for the Linear Temporal Logic of RewritingStreamlining progress-based derivations of concurrent programsUnnamed ItemMechanizing UNITY in IsabelleAlgebra Transformation Systems as a Unifying FrameworkAutomatic Verification of Bossa Scheduler PropertiesEnsuring completeness of symbolic verification methods for infinite-state systemsAbstract state machines: a unifying view of models of computation and of system design frameworksLinearization in parallel pCRLUNITY and Büchi automataPartial correctness for probabilistic demonic programsA pragmatic behavior subtyping relation based on both states and actionsRefinement verification of the lazy caching algorithmWeb CubeInterfaces between languages for communicating systemsPacket efficient implementation of the Omega failure detectorSpecification and analysis of a composition of protocolsThe sliding-window protocol revisitedA simple proof of a simple consensus algorithmGenerate & Check Method for Verifying Transition Systems in CafeOBJFactorizing fault tolerance.Specification and verification of concurrent programs through refinementsA walk over the shortest path: Dijkstra's algorithm viewed as fixed-point computation.The shortest path in parallelEvent-based proof of the mutual exclusion property of Peterson's algorithmA compositional framework for fault tolerance by specification transformationProgram composition via unificationMechanizing a process algebra for network protocolsCorrect translation of data parallel assignment onto array processorsError in the UNITY substitution rule for subscripted operatorsProgress properties for empty \textsc{Unity} programsProperties of concurrent programsA principle for sequential reasoning about distributed algorithmsProperty preserving abstractions for the verification of concurrent systemsFocus points and convergent process operators: A proof strategy for protocol verificationVerifying a distributed list system: A case historyCones and foci: A mechanical framework for protocol verificationFoundations for using linear temporal logic in Event-B refinementA mechanical proof of Segall's PIF algorithmFormal and incremental construction of distributed algorithms: on the distributed reference counting algorithmA basic algebra of stateless connectorsA verifiable low-level concurrent programming model based on colored Petri netsParallel elementwise processable functions in concurrent cleanA methodology for designing proof rules for fair parallel programsPetri net based verification of distributed algorithms: An exampleA predicate transformer for the progress property `to-always'


This page was built for software: UNITY