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
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, Verification and comparison of transition systems, Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?, Interleaving vs True Concurrency: Some Instructive Security Examples, Validating safety arguments with Lean, ElixirST: a session-based type system for elixir modules, Optimization bounds from decision diagrams in Haddock, Back to the format: a survey on SOS for probabilistic processes, Reaction Systems, Transition Systems, and Equivalences, Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction, Equivalence checking 40 years after: a review of bisimulation tools, Runners for interleaving algebraic effects, Coherent modal transition systems refinement, Unnamed Item, A fully abstract denotational model for observational precongruence, A coalgebraic presentation of structured transition systems, An introduction to metric semantics: Operational and denotational models for programming and specification languages, Unnamed Item, An axiomatic semantics for Esterel, From Monadic Logic to PSL, What good are digital clocks?, Compositional weak metrics for group key update, NEW RESULTS ON COMPUTABILITY OF RECURRENCE EQUATIONS, Livelocks in parallel programs
