Formal verification of parallel programs

Cited In (only showing first 100 items - show all)

Towards general axiomatizations for bisimilarity and trace semantics
A deductive approach towards reasoning about algebraic transition systems
Probabilistic divide \& congruence: branching bisimilarity
What good are digital clocks?
Mitigating covert channels based on analysis of the potential for communication
Automatic verification of distributed systems: the process algebra approach.
A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces
Fairness, distances and degrees
A fully abstract denotational model for observational precongruence
Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
Bisimulations and abstraction homomorphisms
Deadlock and fairness in morphisms of transition systems
Bisimulation and effectiveness
An axiomatic semantics for Esterel
Composing model programs for analysis
SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
The origins of structural operational semantics
Compositional semantics of spiking neural P systems
SOS specifications for uniformly continuous operators
Mathematical programming approach to the Petri nets reachability problem
Structured operational semantics and bisimulation as a congruence
A characterization of finitary bisimulation
Deciding bisimilarity is P-complete
Compositional semantics and behavioral equivalences for P systems
A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
Homomorphisms between models of parallel computation
GSOS and finite labelled transition systems
Analysis of Petri nets by stepwise refinements
The temporal semantics of concurrent programs
Universal coalgebra: A theory of systems
Relating strong behavioral equivalences for processes with nondeterminism and probabilities
Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
An algebraic semantics for structured transition systems and its application to logic programs
Nested semantics over finite trees are equationally hard
Logical characterization of branching metrics for nondeterministic probabilistic transition systems
Achieving distributed control through model checking
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
Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
Reaction Systems, Transition Systems, and Equivalences
Reduction and covering of infinite reachability trees
Bisimulation for probabilistic transition systems: A coalgebraic approach
CCS with Hennessy's merge has no finite-equational axiomatization
An equational axiomatization for multi-exit iteration
From Monadic Logic to PSL
A dynamic logic for deductive verification of multi-threaded programs
Compositional bisimulation metric reasoning with Probabilistic Process Calculi
Rule formats for compositional non-interference properties
Characteristic formulae for timed autoamta
A cylinder computation model for many-core parallel computing
An introduction to metric semantics: Operational and denotational models for programming and specification languages
A coalgebraic presentation of structured transition systems
Verification of reactive systems using temporal logic with clocks
Additive models of probabilistic processes
Formal derivation of strongly correct concurrent programs
Trace, failure and testing equivalences for communicating processes
Raiders of the lost equivalence: probabilistic branching bisimilarity
Reasoning about strategies: on the model-checking problem
Rough approximations based on bisimulations
Composition of Model Programs
Verification, refinement and scheduling of real-time programs
Verification and comparison of transition systems
Specification-oriented semantics for communicating processes
Concurrent transition systems
Minimizing the number of transitions with respect to observation equivalence
Comparative semantics for flow of control in logic programming without logic
Specification and analysis of a data transfer protocol using systems of communicating machines
Compositional weak metrics for group key update
On reduction of asynchronous systems
Transition systems, metric spaces and ready sets in the semantics of uniform concurrency
Models for concurrency: Towards a classification
Eliminating the substitution axiom from UNITY logic
When are prime formulae characteristic?
A new methodology for analyzing distributed systems modeled by petri nets
A dynamic evolution for the specifications of distributed systems
Of temporary coalitions in terms of concurrent game models, announcements, and temporal projection
Functional behavior in data spaces
The metric linear-time branching-time spectrum on nondeterministic probabilistic processes
Title not available (Why is that?)
Constructive logical characterizations of bisimilarity for reactive probabilistic systems
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
Back to the format: a survey on SOS for probabilistic processes
Runners for interleaving algebraic effects
Branching place bisimilarity: a decidable behavioral equivalence for finite Petri nets with silent moves
Interleaving vs True Concurrency: Some Instructive Security Examples
Identification of biological transition systems using meta-interpreted logic programs
Characteristic formulae for fixed-point semantics: a general framework
A complete equational axiomatization for MPA with string iteration
Validating safety arguments with Lean
Transition systems of Elementary Net Systems with inhibitor arcs
Equivalence checking 40 years after: a review of bisimulation tools
Group-by-group probabilistic bisimilarities and their logical characterizations
Terminal metric spaces of finitely branching and image finite linear processes
Optimization bounds from decision diagrams in Haddock
ElixirST: a session-based type system for elixir modules
Reasoning about graded strategy quantifiers
A characterization of systems derived from terminating concurrent histories
On the design and specification of message oriented programs
Methods and means of parallel processing of information

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)