• 1080 Citations
  • 18 h-Index
1987 …2021
If you made any changes in Pure these will be visible here soon.

Research Outputs 1987 2019

Filter
Article
2019

Abstract Hidden Markov Models: a monadic account of quantitative information flow

McIver, A., Morgan, C. & Rabehaja, T., 29 Mar 2019, In : Logical Methods in Computer Science. 15, 1, p. 1-50 50 p., 36.

Research output: Contribution to journalArticleResearchpeer-review

Open Access
File
Information Flow
Hidden Markov models
Markov Model
Semantics
Transformer

An axiomatization of information flow measures

Alvim, M. S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C. & Smith, G., 19 Jul 2019, In : Theoretical Computer Science. 777, p. 32-54 23 p.

Research output: Contribution to journalArticleResearchpeer-review

Axiomatization
Information Flow
Leakage
Computer systems
Axioms
2018

A new proof rule for almost-sure termination

McIver, A., Morgan, C., Kaminski, B. L. & Katoen, J-P., 5 Jan 2018, In : Proceedings of the ACM on Programming Languages. 2, POPL, p. 1-28 28 p., 33.

Research output: Contribution to journalArticleResearchpeer-review

Markov processes
Innovation

Conditioning in probabilistic programming

Olmedo, F., Gretz, F., Jansen, N., Kaminski, B. L., Katoen, J. P. & McIver, A., 1 Jan 2018, In : ACM Transactions on Programming Languages and Systems. 40, 1, p. 1-50 50 p., 4.

Research output: Contribution to journalArticleResearchpeer-review

Computer programming
Semantics
Hoists
Markov processes
Sampling

Schedulers and finishers: on generating and filtering the behaviours of an event structure

McIver, A., Rabehaja, T. & Struth, G., 5 Oct 2018, In : Theoretical Computer Science. 744, p. 97-112 16 p.

Research output: Contribution to journalArticleResearchpeer-review

Event Structures
Regain
Model structures
Scheduler
Filtering
2017

Privacy in elections: How small is “small”?

McIver, A., Rabehaja, T., Wen, R. & Morgan, C., 1 Oct 2017, In : Journal of Information Security and Applications. 36, p. 112-126 15 p.

Research output: Contribution to journalArticleResearchpeer-review

Transparency
2016

Probabilistic rely-guarantee calculus

McIver, A., Rabehaja, T. & Struth, G., 6 Dec 2016, In : Theoretical Computer Science. 655, p. 120-134 15 p.

Research output: Contribution to journalArticleResearchpeer-review

Algebra
Calculus
Kleene Algebra
Semantics
Eratosthenes
2015

Hidden-Markov program algebra with iteration

McIver, A., Meinicke, L. & Morgan, C., 19 Feb 2015, In : Mathematical Structures in Computer Science. 25, 2, p. 320-360 41 p.

Research output: Contribution to journalArticleResearchpeer-review

Algebra
Iteration
Hidden Markov models
Noninterference
Semantics
2014

Abstractions of non-interference security: Probabilistic versus possibilistic

Hoang, T. S., McIver, A. K., Meinicke, L., Morgan, C. C., Sloane, A. & Susatyo, E., Jan 2014, In : Formal Aspects of Computing. 26, 1, p. 169-194 26 p.

Research output: Contribution to journalArticleResearchpeer-review

Noninterference
Semantics
Semantic Analysis
Refinement
Network protocols

Hopscotch - reaching the target hop by hop

Höfner, P. & McIver, A., 7 Aug 2014, In : Journal of Logical and Algebraic Methods in Programming. 83, 2, p. 212-224 13 p., 397.

Research output: Contribution to journalArticleResearchpeer-review

graph theory
computer science
Algebra
Path
Target

Operational versus weakest pre-expectation semantics for the probabilistic guarded command language

Gretz, F., Katoen, J. P. & McIver, A., Mar 2014, In : Performance Evaluation. 73, p. 110-132 23 p.

Research output: Contribution to journalArticleResearchpeer-review

Semantics
Reward
Operational Semantics
Markov Decision Process
Correspondence
2011

Compositional refinement in agent-based security protocols

McIver, A. K. & Morgan, C. C., Nov 2011, In : Formal Aspects of Computing. 23, 6, p. 711-737 27 p.

Research output: Contribution to journalArticleResearchpeer-review

Security Protocols
Refinement
Semantics
Network protocols
Model checking
2009
Graphical Modeling
Network Protocols
Formal Analysis
Simulation Analysis
Wireless Networks
2008

Proofs and refutations for probabilistic refinement

McIver, A. K., Morgan, C. C. & Gonzalia, C., 2008, In : Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5014 LNCS, p. 100-115 16 p.

Research output: Contribution to journalArticleResearchpeer-review

Surface mount technology
Semantics
Counterexample
Refinement
Certificate

Using probabilistic Kleene algebra pKA for protocol verification

McIver, A. K., Gonzalia, C., Cohen, E. & Morgan, C. C., May 2008, In : Journal of Logic and Algebraic Programming. 76, 1, p. 90-111 22 p.

Research output: Contribution to journalArticleResearchpeer-review

Protocol Verification
Kleene Algebra
Algebra
Network protocols
Mutual Exclusion
2007

Results on the quantitative μ-calculus qMμ

McIver, A. & Morgan, C., 1 Jan 2007, In : ACM Transactions on Computational Logic. 8, 1, p. 1-43 43 p., 3.

Research output: Contribution to journalArticleResearchpeer-review

μ-calculus
Positive ions
Game
Gambling
Transition Systems
2006

A Novel Stochastic Game Via the Quantitative μ-calculus

McIver, A. & Morgan, C., 23 May 2006, In : Electronic Notes in Theoretical Computer Science. 153, 2 SPEC. ISS., p. 195-212 18 p.

Research output: Contribution to journalArticleResearchpeer-review

μ-calculus
Stochastic Games
Computer science
Computer Science
Game
2005

Abstraction and refinement in probabilistic systems

McIver, A. K. & Morgan, C., 2005, In : Performance Evaluation Review. 32, 4, p. 41-47 7 p.

Research output: Contribution to journalArticleResearchpeer-review

An elementary proof that Herman's Ring is Θ(N2)

McIver, A. & Morgan, C., 30 Apr 2005, In : Information Processing Letters. 94, 2, p. 79-84 6 p.

Research output: Contribution to journalArticleResearchpeer-review

Ring
Stabilization
Self-stabilization
Worst-case Analysis
Nondeterminism

Compositional specification and analysis of cost-based properties in probabilistic programs

Celiku, O. & McIver, A., 2005, In : Lecture Notes in Computer Science. 3582, p. 107-122 16 p.

Research output: Contribution to journalArticleResearchpeer-review

Specification
Specifications
Program Verification
Costs
Reuse

Development via refinement in probabilistic B - Foundation and case study

Hoang, T. S., Jin, Z., Robinson, K., McIver, A. & Morgan, C., 2005, In : Lecture Notes in Computer Science. 3455, p. 355-373 19 p.

Research output: Contribution to journalArticleResearchpeer-review

Refinement
Substitution reactions
Specifications
Semantics
Substitution

Memoryless strategies for stochastic games via domain theory

Morgan, C. & McIver, A., 12 May 2005, In : Electronic Notes in Theoretical Computer Science. 130, p. 23-37 15 p.

Research output: Contribution to journalArticleResearchpeer-review

Domain Theory
Stochastic Games
Game Theory
Game
Formal methods

Probabilistic guarded commands mechanized in HOL

Hurd, J., McIver, A. & Morgan, C., 23 Nov 2005, In : Theoretical Computer Science. 346, 1, p. 96-112 17 p.

Research output: Contribution to journalArticleResearchpeer-review

Mechanization
Semantics
Specifications
Correctness
Logic

Probabilistic Guarded Commands Mechanized in HOL

Hurd, J., McIver, A. & Morgan, C., 2 Jan 2005, In : Electronic Notes in Theoretical Computer Science. 112, SPEC. ISS., p. 95-111 17 p.

Research output: Contribution to journalArticleResearchpeer-review

Mechanization
Correctness
Logic
Partial
Mutual Exclusion
Distributed Systems
Kleene Algebra
Mechanization
Concurrency control
Concurrency Control
2004

Cost-based analysis of probabilistic programs mechanised in HOL

Celiku, O. & McIver, A., 2004, In : Nordic Journal of Computing. 11, 2, p. 102-128 27 p.

Research output: Contribution to journalArticleResearchpeer-review

Deriving probabilistic semantics via the 'weakest completion'

Jifeng, H., Morgan, C. & McIver, A., 2004, In : Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 3308, p. 131-145 15 p.

Research output: Contribution to journalArticleResearchpeer-review

2003

Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL

McIver, A. & Morgan, C., 9 Feb 2003, In : Theoretical Computer Science. 293, 3, p. 507-534 28 p.

Research output: Contribution to journalArticleResearchpeer-review

Temporal logic
Temporal Logic
Logic
Bibliographies
μ-calculus

Probabilistic invariants for probabilistic machines

Hoang, T. S., Jin, Z., Robinson, K., McIver, A. & Morgan, C., 2003, In : Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2651, p. 240-259 20 p.

Research output: Contribution to journalArticleResearchpeer-review

Substitution reactions
Invariant
Substitution
Large-scale Structure
Predicate

Probabilistic termination in B

McIver, A., Morgan, C. & Hoang, T. S., 2003, In : Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2651, p. 216-239 24 p.

Research output: Contribution to journalArticleResearchpeer-review

Termination
Substitution
Substitution reactions
Probabilistic Algorithms
Contention
2002

Quantitative program logic and expected time bounds in probabilistic distributed algorithms

McIver, A. K., 7 Jun 2002, In : Theoretical Computer Science. 282, 1, p. 191-219 29 p.

Research output: Contribution to journalArticleResearchpeer-review

Probabilistic Algorithms
Distributed Algorithms
Logic Programs
Parallel algorithms
Computer programming languages
2001

A generalisation of stationary distributions, and probabilistic program Algebra

McIver, A. K., Nov 2001, In : Electronic Notes in Theoretical Computer Science. 45, p. 279-289 11 p.

Research output: Contribution to journalArticleResearchpeer-review

Stationary Distribution
Markov processes
Algebra
Nondeterminism
Stationarity

Almost-certain eventualities and abstract probabilities in quantitative temporal logic

McIver, A. & Morgan, C., Jan 2001, In : Electronic Notes in Theoretical Computer Science. 42, p. 15-43 29 p.

Research output: Contribution to journalArticleResearchpeer-review

Temporal logic
Temporal Logic
Logic
Linear Temporal Logic
Liveness

Demonic, angelic and unbounded probabilistic choices in sequential programs

McIver, A. K. & Morgan, C., Jan 2001, In : Acta Informatica. 37, 4-5, p. 329-354 26 p.

Research output: Contribution to journalArticleResearchpeer-review

Set theory

Partial correctness for probabilistic demonic programs

McIver, A. K. & Morgan, C., 6 Sep 2001, In : Theoretical Computer Science. 266, 1-2, p. 513-541 29 p.

Research output: Contribution to journalArticleResearchpeer-review

Computer programming languages
Correctness
Semantics
Partial
Programming
1999

Reasoning about efficiency within a probabilistic μ-calculus

McIver, A. K., 1999, In : Electronic Notes in Theoretical Computer Science. 22, p. 138-155 18 p.

Research output: Contribution to journalArticleResearchpeer-review

Sanders
μ-calculus
Reasoning
Predicate
Expected Length
1997

Probabilistic models for the guarded command language

Jifeng, H., Seidel, K. & McIver, A., Apr 1997, In : Science of Computer Programming. 28, 2-3, p. 171-192 22 p.

Research output: Contribution to journalArticleResearchpeer-review

Statistical Models
Semantics
Specifications
1996

Probabilistic Predicate Transformers

Morgan, C., McIver, A. & Seidel, K., May 1996, In : ACM Transactions on Programming Languages and Systems. 18, 3, p. 325-353 29 p.

Research output: Contribution to journalArticleResearchpeer-review

Refinement-oriented probability for CSP

Morgan, C., McIver, A., Seidel, K. & Sanders, J. W., 1996, In : Formal Aspects of Computing. 8, 6, p. 617-647 31 p.

Research output: Contribution to journalArticleResearchpeer-review

Refinement
Nondeterminism
Syntactics
Operator
Probabilistic Model

Software, who needs it?

McIver, A., 1996, In : New Scientist. 152, 2054, p. 40-43 4 p.

Research output: Contribution to journalArticleResearchpeer-review

Unifying wp and wlp

Morgan, C. & McIver, A., 12 Aug 1996, In : Information Processing Letters. 59, 3, p. 159-163 5 p.

Research output: Contribution to journalArticleResearchpeer-review

Predicate
Subadditivity
Transformer
Characteristic Function
State Space
1990

Finitely generated non-Hopf modules

McIver, A., Jun 1990, In : Archiv der Mathematik. 54, 6, p. 533-538 6 p.

Research output: Contribution to journalArticleResearchpeer-review

1987

Enumerating finite groups

Mciver, A. & Neumann, P. M., Dec 1987, In : Quarterly Journal of Mathematics. 38, 4, p. 473-488 16 p.

Research output: Contribution to journalArticleResearchpeer-review