Formal verification of parallel programs
From MaRDI portal
Publication:4095835
DOI10.1145/360248.360251zbMath0329.68016OpenAlexW1994350081MaRDI QIDQ4095835
Publication date: 1976
Published in: Communications of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/360248.360251
Related Items (only showing first 100 items - show all)
Characteristic formulae for fixed-point semantics: a general framework ⋮ GSOS and finite labelled transition systems ⋮ The origins of structural operational semantics ⋮ Rule formats for compositional non-interference properties ⋮ Identification of biological transition systems using meta-interpreted logic programs ⋮ A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces ⋮ A characterization of finitary bisimulation ⋮ Bisimulations and abstraction homomorphisms ⋮ Invariants, composition, and substitution ⋮ Trace, failure and testing equivalences for communicating processes ⋮ Deadlock and fairness in morphisms of transition systems ⋮ Mathematical programming approach to the Petri nets reachability problem ⋮ Transition systems, metric spaces and ready sets in the semantics of uniform concurrency ⋮ An equational axiomatization for multi-exit iteration ⋮ A linear algorithm to solve fixed-point equations on transition systems ⋮ Bisimulation and effectiveness ⋮ A deductive approach towards reasoning about algebraic transition systems ⋮ Concurrent transition systems ⋮ A new methodology for analyzing distributed systems modeled by petri nets ⋮ Nested semantics over finite trees are equationally hard ⋮ An application of temporal projection to interleaving concurrency ⋮ A unified rule format for bounded nondeterminism in SOS with terms as labels ⋮ A methodology for designing proof rules for fair parallel programs ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Terminal metric spaces of finitely branching and image finite linear processes ⋮ SOS specifications for uniformly continuous operators ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ When Are Prime Formulae Characteristic? ⋮ Determining asynchronous test equivalence for probabilistic processes ⋮ Reasoning About Strategies ⋮ A cylinder computation model for many-core parallel computing ⋮ \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics ⋮ When are prime formulae characteristic? ⋮ Cooperative concurrent games ⋮ The temporal semantics of concurrent programs ⋮ A characterization of systems derived from terminating concurrent histories ⋮ On the axiomatisability of priority. III: Priority strikes again ⋮ Reasoning About Substructures and Games ⋮ Automated synthesis of application-layer connectors from automata-based specifications ⋮ SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR ⋮ Methods and means of parallel processing of information ⋮ Reasoning about graded strategy quantifiers ⋮ Compositional bisimulation metric reasoning with Probabilistic Process Calculi ⋮ A unified approach for studying the properties of transition systems ⋮ Parallel algorithms for the single source shortest path problem ⋮ Unnamed Item ⋮ Achieving distributed control through model checking ⋮ Bisimulation for probabilistic transition systems: A coalgebraic approach ⋮ Compositional semantics and behavioral equivalences for P systems ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ Reduction and covering of infinite reachability trees ⋮ Constructive logical characterizations of bisimilarity for reactive probabilistic systems ⋮ Minimizing the number of transitions with respect to observation equivalence ⋮ Team bisimilarity, and its associated modal logic, for BPP nets ⋮ An agent calculus with simple actions where the enabling and disabling are derived operators ⋮ Characteristic Formulae for Timed Automata ⋮ Models for concurrency: Towards a classification ⋮ Towards general axiomatizations for bisimilarity and trace semantics ⋮ Rough approximations based on bisimulations ⋮ Fairness, distances and degrees ⋮ The metric linear-time branching-time spectrum on nondeterministic probabilistic processes ⋮ Structured operational semantics and bisimulation as a congruence ⋮ An algebraic semantics for structured transition systems and its application to logic programs ⋮ Automatic verification of distributed systems: the process algebra approach. ⋮ Deciding bisimilarity is P-complete ⋮ Relating strong behavioral equivalences for processes with nondeterminism and probabilities ⋮ Mitigating covert channels based on analysis of the potential for communication ⋮ Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes ⋮ CCS with Hennessy's merge has no finite-equational axiomatization ⋮ Probabilistic divide \& congruence: branching bisimilarity ⋮ Composing model programs for analysis ⋮ Logical characterization of branching metrics for nondeterministic probabilistic transition systems ⋮ Compositional semantics of spiking neural P systems ⋮ From Philosophical to Industrial Logics ⋮ On reduction of asynchronous systems ⋮ Functional behavior in data spaces ⋮ Automated Synthesis of Application-Layer Connectors from Automata-Based Specifications ⋮ Composition of Model Programs ⋮ Formal derivation of strongly correct concurrent programs ⋮ Determinizing monitors for HML with recursion ⋮ Analysis of Petri nets by stepwise refinements ⋮ On the design and specification of message oriented programs ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Eliminating the substitution axiom from UNITY logic ⋮ A complete equational axiomatization for MPA with string iteration ⋮ Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations ⋮ Current methods for proving program correctness ⋮ Verification of reactive systems using temporal logic with clocks ⋮ Homomorphisms between models of parallel computation ⋮ Raiders of the lost equivalence: probabilistic branching bisimilarity ⋮ Universal coalgebra: A theory of systems ⋮ A verification-driven framework for iterative design of controllers ⋮ Verification, refinement and scheduling of real-time programs ⋮ Specification-oriented semantics for communicating processes ⋮ Comparative semantics for flow of control in logic programming without logic ⋮ Specification and analysis of a data transfer protocol using systems of communicating machines ⋮ Additive models of probabilistic processes ⋮ Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs ⋮ Comparing logics for rewriting: Rewriting logic, action calculi and tile logic ⋮ Branching place bisimilarity: a decidable behavioral equivalence for finite Petri nets with silent moves
This page was built for publication: Formal verification of parallel programs
