Formal verification of parallel programs
From MaRDI portal
Publication:4095835
Cited in
(only showing first 100 items - show all)- 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
- An axiomatic semantics for Esterel
- Mathematical programming approach to the Petri nets reachability problem
- Specification and analysis of a data transfer protocol using systems of communicating machines
- Relating strong behavioral equivalences for processes with nondeterminism and probabilities
- Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
- Transition systems, metric spaces and ready sets in the semantics of uniform concurrency
- Rule formats for compositional non-interference properties
- Characteristic formulae for timed autoamta
- Deadlock and fairness in morphisms of transition systems
- On reduction of asynchronous systems
- Composing model programs for analysis
- Reasoning about strategies: on the model-checking problem
- Models for concurrency: Towards a classification
- Rough approximations based on bisimulations
- What good are digital clocks?
- Mitigating covert channels based on analysis of the potential for communication
- A linear algorithm to solve fixed-point equations on transition systems
- An algebraic semantics for structured transition systems and its application to logic programs
- Compositional semantics and behavioral equivalences for P systems
- Achieving distributed control through model checking
- Automatic verification of distributed systems: the process algebra approach.
- Fairness, distances and degrees
- Composition of Model Programs
- A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
- Nested semantics over finite trees are equationally hard
- From Monadic Logic to PSL
- Verification, refinement and scheduling of real-time programs
- Eliminating the substitution axiom from UNITY logic
- 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
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)
