On the bisimulation proof method
From MaRDI portal
Publication:4236205
DOI10.1017/S0960129598002527zbMATH Open0916.68057OpenAlexW2128995870MaRDI QIDQ4236205FDOQ4236205
Authors: Davide Sangiorgi 
Publication date: 22 March 1999
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129598002527
Recommendations
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (65)
- When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
- Coinduction in Flow: The Later Modality in Fibrations
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- Up-to techniques for behavioural metrics via fibrations
- Bisimulation proof methods in a path-based specification language for polynomial coalgebras
- Preorder-constrained simulations for program refinement with effects
- Proving the validity of equations in GSOS languages using rule-matching bisimilarity
- CoCon: a conference management system with formally verified document confidentiality
- A Testing Theory for a Higher-Order Cryptographic Language
- Corecursion up-to via causal transformations
- Bisimulation and coinduction enhancements: a historical perspective
- On the observational theory of the CPS-calculus
- Up-to techniques for behavioural metrics via fibrations
- Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
- On parameterization of higher-order processes
- (Bi)simulations up-to characterise process semantics
- Parameterizing higher-order processes on names and processes
- Bisimulations for delimited-control operators
- A fully abstract model for the \(\pi\)-calculus.
- Process calculus based upon evaluation to committed form
- Concise graphs and functional bisimulations
- Tower induction and up-to techniques for CCS with fixed points
- Some congruence properties for \(\pi\)-calculus bisimilarities
- Title not available (Why is that?)
- A symbolic decision procedure for symbolic alternating finite automata
- Metric reasoning about \(\lambda\)-terms: the general case
- Algorithms for Kleene algebra with converse
- Title not available (Why is that?)
- Diacritical companions
- Enhancements of the bisimulation proof method
- Bisimulation and co-induction: some problems
- Elements of stream calculus (an extensive exercise in coinduction)
- A process calculus for mobile ad hoc networks
- On Bisimulation Proofs for the Analysis of Distributed Abstract Machines
- Title not available (Why is that?)
- Encoding Asynchronous Interactions Using Open Petri Nets
- Linear forwarders
- Generalised coinduction
- A bisimulation-based method for proving the validity of equations in GSOS languages
- An effective coalgebraic bisimulation proof method
- Higher-order psi-calculi
- Proving language inclusion and equivalence by coinduction
- Structural congruence for bialgebraic semantics
- New up-to techniques for weak bisimulation
- Complete Lattices and Up-To Techniques
- Title not available (Why is that?)
- Processes as formal power series: a coinductive approach to denotational semantics
- Simulations up-to and canonical preorders (extended abstract)
- A hierarchy of equivalences for asynchronous calculi
- GSOS for probabilistic transition systems (extended abstract)
- Bisimulation is two-way simulation
- Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus
- On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems
- Title not available (Why is that?)
- Distinguishing and relating higher-order and first-order processes by expressiveness
- Using bisimulation proof techniques for the analysis of distributed abstract machines
- Title not available (Why is that?)
- Higher-order processes with parameterization over names and processes
- SPEC: an equivalence checker for security protocols
- Enhanced coalgebraic bisimulation
- Locality and interleaving semantics in calculi for mobile processes
- Extracting proofs from tabled proof search
- A general account of coinduction up-to
- The largest respectful function
- Companions, codensity and causality
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)
