• 1153 Citations
  • 18 h-Index
1987 …2020

Research output per year

If you made any changes in Pure these will be visible here soon.

Research Outputs

2010

An expectation transformer approach to predicate abstraction and data independence for probabilistic programs

Ndukwu, U. & McIver, A. K., 2010, Proceedings of the 8th Workshop on Quantitative Aspects of Programming Languages. Di Pierro, A. & Norman, G. (eds.). Electronic Proceedings in Theoretical Computer Science (EPTCS), p. 129-143 15 p.

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

6 Citations (Scopus)

Compositional closure for Bayes risk in probabilistic noninterference

McIver, A., Meinicke, L. & Morgan, C., 2010, Automata, Languages and Programming - 37th International Colloquium, ICALP 2010, Proceedings. Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F. & Spirakis, P. G. (eds.). PART 2 ed. Berlin; Heidelberg: Springer, Springer Nature, Vol. 6199 LNCS. p. 223-235 13 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6199 LNCS, no. PART 2).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

46 Citations (Scopus)

Linear-invariant generation for probabilistic programs: Automated support for proof-based methods

Katoen, J. P., McIver, A. K., Meinicke, L. A. & Morgan, C. C., 2010, Static Analysis - 17th International Symposium, SAS 2010, Proceedings. Cousot, R. & Martel, M. (eds.). Berlin: Springer, Springer Nature, Vol. 6337 LNCS. p. 390-406 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6337 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

43 Citations (Scopus)

The thousand-and-one cryptographers

McIver, A. K. & Morgan, C. C., 2010, Reflections on the work of C.A.R. Hoare. Roscoe, A. W., Jones, C. B. & Wood, K. B. (eds.). London: Springer, Springer Nature, p. 255-282 28 p. (History of computing).

Research output: Chapter in Book/Report/Conference proceedingChapter

YAGA: automated analysis of quantitative safety specifications in probabilistic B

Ndukwu, U. & McIver, A. K., 2010, Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Proceedings. Bouajjani, A. & Chin, W-N. (eds.). Berlin; Heidelberg: Springer, Springer Nature, Vol. 6252 LNCS. p. 378-386 9 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6252 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

2 Citations (Scopus)
2009
13 Citations (Scopus)

Security, probability and nearly fair coins in the cryptographers' café

McIver, A., Meinicke, L. & Morgan, C., 2009, FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. Cavalcanti, A. & Dams, D. R. (eds.). Berlin: Springer, Springer Nature, p. 41-71 31 p. (Lecture Notes in Computer Science; vol. 5850).

Research output: Chapter in Book/Report/Conference proceedingChapter

4 Citations (Scopus)

Sums and lovers: Case studies in security, compositionality and refinement

McIver, A. K. & Morgan, C. C., 2009, FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. Cavalcanti, A. & Dams, D. R. (eds.). Berlin: Springer, Springer Nature, p. 289-304 16 p. (Lecture Notes in Computer Science; vol. 5850).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

8 Citations (Scopus)

The secret art of computer programming

McIver, A. K., 2009, Theoretical aspects of computing - ICTAC 2009: 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009, proceedings. Leucker, M. & Morgan, C. (eds.). Berlin: Springer, Springer Nature, p. 61-78 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5684 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

3 Citations (Scopus)
2008

CaVi - Simulation and model checking for wireless sensor networks

Boulis, A., Fehnker, A., Fruth, M. & McIver, A., 2008, Proceedings - 5th International Conference on the Quantitative Evaluation of Systems, QEST 2008. G., R. (ed.). Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), p. 37-38 2 p. 4634949

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

Open Access
File
6 Citations (Scopus)
4 Citations (Scopus)

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 journalArticle

11 Citations (Scopus)
2007

Automating refinement checking in probabilistic system design

Gonzalia, C. & McIver, A., 2007, Formal Methods and Software Engineering - 9th International Conference on Formal Engineenng Methods, ICFEM 2007, Proceedings. Butler, M., Hinchey, M. G. & Larrondo-Petrie, M. M. (eds.). Berlin; New York: Springer, Springer Nature, Vol. 4789 LNCS. p. 212-231 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4789 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

Formal techniques for the analysis of wireless networks

McIver, A. K. & Fehnker, A., 2007, Proceedings - ISoLA 2006: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), p. 263-270 8 p. 4463722

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

17 Citations (Scopus)

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 journalArticle

29 Citations (Scopus)
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 journalArticle

3 Citations (Scopus)

Developing and reasoning about probabilistic programs in pGCL

McIver, A. & Morgan, C., 2006, Refinement Techniques in Software Engineering - First Pernambuco Summer School on Software Engineering, PSSE 2004, Revised Lectures. Berlin; New York: Springer, Springer Nature, Vol. 3167 LNCS. p. 123-155 33 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 3167 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

14 Citations (Scopus)

Programming-logic analysis of fault tolerance: expected performance of self-stabilisation

Morgan, C. C. & McIver, A., 2006, RIGOROUS DEVELOPMENT OF COMPLEX FAULT-TOLERANT SYSTEMS. Butler, M., Jones, C., Romanovsky, A. & Troubitsyna, E. (eds.). Berlin; New York: Springer, Springer Nature, p. 288-305 18 p. (Lecture Notes in Computer Science; vol. 4157).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

Open Access

Quantitative refinement and model checking for the analysis of probabilistic systems

McIver, A. K., 2006, FM 2006: Formal Methods - 14th International Symposium on Formal Methods, Proceedings. Misra, J., Nipkow, T. & Sekerinski, E. (eds.). Berlin; New York: Springer, Springer Nature, Vol. 4085 LNCS. p. 131-146 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4085 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

5 Citations (Scopus)

Quantitative μ-calculus analysis of power management in wireless networks

McIver, A. K., 2006, Theoretical Aspects of Computing - ICTAC 2006 Third International Colloquium, Proceedings. Barkaoui, K., Cavalcanti, A. & Cerone, A. (eds.). Berlin; New York: Springer, Springer Nature, Vol. 4281 LNCS. p. 50-64 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4281 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

1 Citation (Scopus)

Using probabilistic kleene algebra for protocol verification

McIver, A. K., Cohen, E. & Morgan, C. C., 2006, Relations and Kleene Algebra in Computer Science - 9th Int. Conf. on Relational Methods in Computer Science and 4th Int. Workshop on Applications of Kleene Algebra, RelMiCS/AKA 2006, Proceedings. Berlin; New York: Springer, Springer Nature, Vol. 4136 LNCS. p. 296-310 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4136 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

22 Citations (Scopus)
2005

Abstraction, refinement and proof for probabilistic systems

McIver, A. & Morgan, C., 2005, New York, USA: Springer, Springer Nature.

Research output: Book/ReportBook

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 journalArticle

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 journalArticle

12 Citations (Scopus)

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 journalArticle

4 Citations (Scopus)

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 journalArticle

1 Citation (Scopus)

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 journalArticle

1 Citation (Scopus)

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 journalArticle

40 Citations (Scopus)

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 journalArticle

9 Citations (Scopus)
13 Citations (Scopus)
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 journalArticle

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 journalArticle

2 Citations (Scopus)

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 journalArticle

14 Citations (Scopus)
11 Citations (Scopus)

Programming Methodology

McIver, A. (ed.) & Morgan, C. (ed.), 2003, Springer, Springer Nature.

Research output: Book/ReportEdited Book/Anthology

2002

Games, probability, and the quantitative μ-calculus qMμ

McIver, A. K. & Morgan, C. C., 2002, Logic for Programming, Artificial Intelligence, and Reasoning - 9th International Conference, LPAR 2002, Proceedings. Baaz, M. & Voronkov, A. (eds.). Berlin; Heidelberg: Springer, Springer Nature, Vol. 2514. p. 292-310 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 2514).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

30 Citations (Scopus)

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 journalArticle

3 Citations (Scopus)
2001
5 Citations (Scopus)

A Generalisation of Stationary Distributions and Probabilistic Program Algebra

McIver, AK., 2001, Electronic Notes in Theoretical Computer Science, Vol 45. Brooks, S. & Mislove, M. (eds.). Amsterdam, The Netherlands: Elsevier, p. 1-11 11 p.

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

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 journalArticle

1 Citation (Scopus)

Cost analysis of games, using program logic

Morgan, C. & McIver, A., Dec 2001, Proceedings of the Asia-Pacific Software Engineering Conference and International Computer Science Conference, APSEC and ICSC. Piscataway, N.J.: Institute of Electrical and Electronics Engineers (IEEE), p. 351 1 p. 991501

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

8 Citations (Scopus)

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 journalArticle

19 Citations (Scopus)

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 journalArticle

32 Citations (Scopus)
1999

Quantitative program logic and performance in probabilistic distributed algorithms

McIver, A. K., 1999, Formal Methods for Real-Time and Probabilistic Systems: 5th International AMAST Workshop, ARTS'99, Bamberg, Germany, May 26-28, 1999, Proceedings. Katoen, J-P. (ed.). 1 ed. Berlin: Springer, Springer Nature, Vol. 1601. p. 19-33 15 p. (Lecture Notes in Computer Science; vol. 1601).

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

2 Citations (Scopus)

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 journalArticle

3 Citations (Scopus)
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 journalArticle

105 Citations (Scopus)
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 journalArticle

163 Citations (Scopus)

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 journalArticle

51 Citations (Scopus)

Software, who needs it?

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

Research output: Contribution to journalArticle

1 Citation (Scopus)