Formal verification of parallel programs

Cited in

(only showing first 100 items - show all)

Cooperative concurrent games
Equivalence checking 40 years after: a review of bisimulation tools
Determining asynchronous test equivalence for probabilistic processes
Back to the format: a survey on SOS for probabilistic processes
scientific article; zbMATH DE number 7471704 (Why is no real title available?)
Constructive logical characterizations of bisimilarity for reactive probabilistic systems
scientific article; zbMATH DE number 7447772 (Why is no real title available?)
A verification-driven framework for iterative design of controllers
Validating safety arguments with Lean
Runners for interleaving algebraic effects
Branching place bisimilarity: a decidable behavioral equivalence for finite Petri nets with silent moves
Group-by-group probabilistic bisimilarities and their logical characterizations
Functional behavior in data spaces
Characteristic formulae for fixed-point semantics: a general framework
Automated synthesis of application-layer connectors from automata-based specifications
When are prime formulae characteristic?
A methodology for designing proof rules for fair parallel programs
Automated synthesis of application-layer connectors from automata-based specifications
Livelocks in parallel programs
An application of temporal projection to interleaving concurrency
A unified rule format for bounded nondeterminism in SOS with terms as labels
The metric linear-time branching-time spectrum on nondeterministic probabilistic processes
Causal reversibility implies time reversibility
A new methodology for analyzing distributed systems modeled by petri nets
Interleaving vs True Concurrency: Some Instructive Security Examples
Optimization bounds from decision diagrams in Haddock
Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction
Determinizing monitors for HML with recursion
Reasoning about graded strategy quantifiers
An agent calculus with simple actions where the enabling and disabling are derived operators
When are prime formulae characteristic?
Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?
Identification of biological transition systems using meta-interpreted logic programs
A characterization of systems derived from terminating concurrent histories
Terminal metric spaces of finitely branching and image finite linear processes
Branching bisimulation semantics enables noninterference analysis of reversible systems
\textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics
On the design and specification of message oriented programs
scientific article; zbMATH DE number 7559474 (Why is no real title available?)
Methods and means of parallel processing of information
Coherent modal transition systems refinement
On the axiomatisability of priority. III: Priority strikes again
Transition systems of Elementary Net Systems with inhibitor arcs
Current methods for proving program correctness
Reasoning About Substructures and Games
Invariants, composition, and substitution
From Philosophical to Industrial Logics
A fully abstract denotational model for observational precongruence
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
New results on computability of recurrence equations
Team bisimilarity, and its associated modal logic, for BPP nets
A complete equational axiomatization for MPA with string iteration
A dynamic evolution for the specifications of distributed systems
Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
Of temporary coalitions in terms of concurrent game models, announcements, and temporal projection
The temporal semantics of concurrent programs
A coalgebraic presentation of structured transition systems
Homomorphisms between models of parallel computation
SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
A dynamic logic for deductive verification of multi-threaded programs
Verification of reactive systems using temporal logic with clocks
GSOS and finite labelled transition systems
Towards general axiomatizations for bisimilarity and trace semantics
A unified approach for studying the properties of transition systems
Parallel algorithms for the single source shortest path problem
A fully abstract denotational model for observational precongruence
An introduction to metric semantics: Operational and denotational models for programming and specification languages
Minimizing the number of transitions with respect to observation equivalence
Sometime = always + recursion \(\equiv\) always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
Bisimulation and effectiveness
Compositional semantics of spiking neural P systems
Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
Compositional bisimulation metric reasoning with Probabilistic Process Calculi
An equational axiomatization for multi-exit iteration
A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces
Reaction Systems, Transition Systems, and Equivalences
Verification and comparison of transition systems
A characterization of finitary bisimulation
Additive models of probabilistic processes
Structured operational semantics and bisimulation as a congruence
Reduction and covering of infinite reachability trees
Bisimulations and abstraction homomorphisms
Logical characterization of branching metrics for nondeterministic probabilistic transition systems
Trace, failure and testing equivalences for communicating processes
Specification-oriented semantics for communicating processes
Deciding bisimilarity is P-complete
A deductive approach towards reasoning about algebraic transition systems
Raiders of the lost equivalence: probabilistic branching bisimilarity
Bisimulation for probabilistic transition systems: A coalgebraic approach
Concurrent transition systems
The origins of structural operational semantics
CCS with Hennessy's merge has no finite-equational axiomatization
Universal coalgebra: A theory of systems
Compositional weak metrics for group key update
Probabilistic divide \& congruence: branching bisimilarity
SOS specifications for uniformly continuous operators
Formal derivation of strongly correct concurrent programs
Analysis of Petri nets by stepwise refinements
A cylinder computation model for many-core parallel computing
Comparative semantics for flow of control in logic programming without logic

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)