On the bisimulation proof method
From MaRDI portal
Publication:4236205
Recommendations
Cited in
(71)- (Bi)simulations up-to characterise process semantics
- Some congruence properties for \(\pi\)-calculus bisimilarities
- Process calculus based upon evaluation to committed form
- Bisimulation is two-way simulation
- A fully abstract model for the \(\pi\)-calculus.
- A hierarchy of equivalences for asynchronous calculi
- Distinguishing and relating higher-order and first-order processes by expressiveness
- Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus
- CoCon: a conference management system with formally verified document confidentiality
- Corecursion up-to via causal transformations
- A symbolic decision procedure for symbolic alternating finite automata
- Diacritical companions
- Bisimulation and coinduction enhancements: a historical perspective
- New up-to techniques for weak bisimulation
- Linear forwarders
- Processes as formal power series: a coinductive approach to denotational semantics
- GSOS for probabilistic transition systems (extended abstract)
- Concise graphs and functional bisimulations
- An effective coalgebraic bisimulation proof method
- Simulations up-to and canonical preorders (extended abstract)
- Proving the validity of equations in GSOS languages using rule-matching bisimilarity
- Extracting proofs from tabled proof search
- Companions, codensity and causality
- Metric reasoning about -terms: the general case
- Algorithms for Kleene algebra with converse
- A Testing Theory for a Higher-Order Cryptographic Language
- SPEC: an equivalence checker for security protocols
- Encoding Asynchronous Interactions Using Open Petri Nets
- Structural congruence for bialgebraic semantics
- Complete Lattices and Up-To Techniques
- On Bisimulation Proofs for the Analysis of Distributed Abstract Machines
- scientific article; zbMATH DE number 177532 (Why is no real title available?)
- scientific article; zbMATH DE number 2038740 (Why is no real title available?)
- Generalised coinduction
- Elements of stream calculus (an extensive exercise in coinduction)
- On parameterization of higher-order processes
- Up-to techniques for behavioural metrics via fibrations
- Higher-order processes with parameterization over names and processes
- Conditional bisimilarity for reactive systems
- The theory of traces for systems with nondeterminism, probability, and termination
- Parameterizing higher-order processes on names and processes
- A bisimulation-based method for proving the validity of equations in GSOS languages
- scientific article; zbMATH DE number 7407797 (Why is no real title available?)
- A general account of coinduction up-to
- Bisimulation and co-induction: some problems
- Tower induction and up-to techniques for CCS with fixed points
- Enhanced coalgebraic bisimulation
- Bisimulations for delimited-control operators
- Enhancements of the bisimulation proof method
- On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems
- The largest respectful function
- Higher-order psi-calculi
- Bisimulation proof methods in a path-based specification language for polynomial coalgebras
- Coinduction: automata, formal proof, companions (invited paper)
- Coinduction in Flow: The Later Modality in Fibrations
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
- Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
- Up-to techniques for behavioural metrics via fibrations
- Preorder-constrained simulations for program refinement with effects
- Locality and interleaving semantics in calculi for mobile processes
- Conditional bisimilarity for reactive systems
- A complete normal-form bisimilarity for algebraic effects and handlers
- Relative security: (dis)proving resilience against semantic optimization vulnerabilities in Isabelle/HOL. Extended version
- Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq
- Bisimulations and logics for higher-dimensional automata
- Strong induction is an up-to technique
- Proving language inclusion and equivalence by coinduction
- Using bisimulation proof techniques for the analysis of distributed abstract machines
- A process calculus for mobile ad hoc networks
- On the observational theory of the CPS-calculus
This page was built for publication: On the bisimulation proof method
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4236205)
