Formal verification of parallel programs

Cited in

(only showing first 100 items - show all)

Invariants, composition, and substitution
Reasoning about strategies: on the model-checking problem
Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction
Rough approximations based on bisimulations
Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?
Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
A verification-driven framework for iterative design of controllers
Composition of Model Programs
On the axiomatisability of priority. III: Priority strikes again
Verification, refinement and scheduling of real-time programs
Specification-oriented semantics for communicating processes
Concurrent transition systems
Minimizing the number of transitions with respect to observation equivalence
Verification and comparison of transition systems
Comparative semantics for flow of control in logic programming without logic
Specification and analysis of a data transfer protocol using systems of communicating machines
Branching bisimulation semantics enables noninterference analysis of reversible systems
When are prime formulae characteristic?
On reduction of asynchronous systems
Compositional weak metrics for group key update
A methodology for designing proof rules for fair parallel programs
Transition systems, metric spaces and ready sets in the semantics of uniform concurrency
Models for concurrency: Towards a classification
Causal reversibility implies time reversibility
scientific article; zbMATH DE number 7559474 (Why is no real title available?)
Automated synthesis of application-layer connectors from automata-based specifications
Automated synthesis of application-layer connectors from automata-based specifications
A fully abstract denotational model for observational precongruence
Eliminating the substitution axiom from UNITY logic
Towards general axiomatizations for bisimilarity and trace semantics
A deductive approach towards reasoning about algebraic transition systems
Probabilistic divide \& congruence: branching bisimilarity
When are prime formulae characteristic?
Mitigating covert channels based on analysis of the potential for communication
Automatic verification of distributed systems: the process algebra approach.
A new methodology for analyzing distributed systems modeled by petri nets
A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces
Functional behavior in data spaces
The metric linear-time branching-time spectrum on nondeterministic probabilistic processes
What good are digital clocks?
Fairness, distances and degrees
A dynamic evolution for the specifications of distributed systems
Of temporary coalitions in terms of concurrent game models, announcements, and temporal projection
Constructive logical characterizations of bisimilarity for reactive probabilistic systems
scientific article; zbMATH DE number 7471704 (Why is no real title available?)
Sometime = always + recursion always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
Bisimulations and abstraction homomorphisms
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
Deadlock and fairness in morphisms of transition systems
A fully abstract denotational model for observational precongruence
Bisimulation and effectiveness
Branching place bisimilarity: a decidable behavioral equivalence for finite Petri nets with silent moves
Composing model programs for analysis
Back to the format: a survey on SOS for probabilistic processes
Runners for interleaving algebraic effects
An axiomatic semantics for Esterel
The origins of structural operational semantics
Identification of biological transition systems using meta-interpreted logic programs
SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
Interleaving vs True Concurrency: Some Instructive Security Examples
Compositional semantics of spiking neural P systems
Mathematical programming approach to the Petri nets reachability problem
SOS specifications for uniformly continuous operators
Characteristic formulae for fixed-point semantics: a general framework
A complete equational axiomatization for MPA with string iteration
A characterization of finitary bisimulation
Deciding bisimilarity is P-complete
Structured operational semantics and bisimulation as a congruence
A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
Compositional semantics and behavioral equivalences for P systems
Validating safety arguments with Lean
GSOS and finite labelled transition systems
Homomorphisms between models of parallel computation
Analysis of Petri nets by stepwise refinements
Group-by-group probabilistic bisimilarities and their logical characterizations
Transition systems of Elementary Net Systems with inhibitor arcs
Equivalence checking 40 years after: a review of bisimulation tools
The temporal semantics of concurrent programs
Universal coalgebra: A theory of systems
Terminal metric spaces of finitely branching and image finite linear processes
Relating strong behavioral equivalences for processes with nondeterminism and probabilities
Nested semantics over finite trees are equationally hard
An algebraic semantics for structured transition systems and its application to logic programs
Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
Optimization bounds from decision diagrams in Haddock
Reasoning about graded strategy quantifiers
Logical characterization of branching metrics for nondeterministic probabilistic transition systems
Achieving distributed control through model checking
A characterization of systems derived from terminating concurrent histories
A linear algorithm to solve fixed-point equations on transition systems
A unified approach for studying the properties of transition systems
Parallel algorithms for the single source shortest path problem
On the design and specification of message oriented programs
Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
Reduction and covering of infinite reachability trees
Reaction Systems, Transition Systems, and Equivalences
CCS with Hennessy's merge has no finite-equational axiomatization
Bisimulation for probabilistic transition systems: A coalgebraic approach
Methods and means of parallel processing of information
An equational axiomatization for multi-exit iteration

This page was built for publication: Formal verification of parallel programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4095835)