ORCID as entered in ROS
https://orcid.org/0000-0002-8535-9068
Select Publications
Conference Papers
, 2023, 'A Novel Analysis of Utility in Privacy Pipelines, Using Kronecker Products and Quantitative Information Flow', in CCS 2023 - Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, pp. 1718 - 1731, http://dx.doi.org/10.1145/3576915.3623081
, 2022, 'How to Develop an Intuition for Risk. . . and Other Invisible Phenomena', in Leibniz International Proceedings in Informatics, LIPIcs, http://dx.doi.org/10.4230/LIPIcs.CSL.2022.2
, 2020, 'Correctness by Construction for Probabilistic Programs', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 216 - 239, http://dx.doi.org/10.1007/978-3-030-61362-4_12
, 2019, 'Proving that programs are differentially private', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bali, Indonesia, pp. 3 - 18, presented at
, 2017, 'Reasoning about distributed secrets', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Neuchâtel, Switzerland, pp. 156 - 170, presented at
, 2017, 'Algebra for quantitative information flow', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Lyon, France, pp. 3 - 23, presented at
, 2016, 'Proof of OS scheduling behavior in the presence of interrupt-induced concurrency', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France, pp. 52 - 68, presented at
, 2016, 'Axioms for information leakage', in Proceedings - IEEE Computer Security Foundations Symposium, Lisbon, Portugal, presented at
, 2015, 'Controlled owicki-gries concurrency: Reasoning about the preemptible eChronos embedded operating system', in Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association, pp. 10 - 24, http://dx.doi.org/10.4204/EPTCS.196.2
, 2015, 'Abstract hidden markov models: A monadic account of quantitative information flow', in Proceedings - Symposium on Logic in Computer Science, pp. 597 - 608, http://dx.doi.org/10.1109/LICS.2015.61
, 2015, 'A nondeterministic lattice of information', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 9 - 10
, 2014, 'Additive and multiplicative notions of leakage, and their capacities', in Proceedings of the Computer Security Foundations Workshop, pp. 308 - 322, http://dx.doi.org/10.1109/CSF.2014.29
, 2014, '(In-)formal methods: The lost art a users’ manual', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Chongqing, China, pp. 1 - 79, presented at
, 2014, 'Abstract channels and their robust information-leakage ordering', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 83 - 102, http://dx.doi.org/10.1007/978-3-642-54792-8_5
, 2014, 'Towards a formal analysis of information leakage for signature attacks in preferential elections', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 595 - 610, http://dx.doi.org/10.1007/978-3-319-06410-9_40
, 2012, 'Elementary probability theory in the Eindhoven style', in 11th International Conference, MPC 2012, Springer, Heidelberg, pp. 48 - 73, presented at
, 2012, 'A Kantorovich-monadic powerdomain for information hiding, with probability and nondeterminism', in Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, New Jersey, pp. 461 - 470, presented at
, 2010, 'Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods', in Cousot R; Martel M (ed.), STATIC ANALYSIS, SPRINGER, FRANCE, Perpignan, pp. 390 - +, presented at
, 2010, 'Compositional closure for bayes risk in probabilistic noninterference', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 223 - 235, http://dx.doi.org/10.1007/978-3-642-14162-1_19
, 2010, 'Compositional closure for Bayes Risk in sequential noninterference', in Proceedings ICALP 2010, LNCS 6199, Springer, Bordeaux, pp. 223 - 235, presented at
, 2010, 'Linear-invariant generation for probabilistic programs', in AICI - Lecture Notes in Computer Science, Springer, Germany, pp. 390 - 406, presented at
, 2009, 'Preface', in Electronic Proceedings in Theoretical Computer Science, EPTCS, http://dx.doi.org/10.4204/EPTCS.13
, 2009, 'Security, probability and nearly fair coins in the cryptographers' cafe', in Logic Programming, 21st International Conference, Springer, Berlin, presented at
, 2009, 'Sums and Lovers: Case studies in security, compositionality and refinement', in Logic Programming, 21st International Conference, Springer, Berlin, presented at
, 2009, 'How to brew-up a refinement order', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Eindhoven, Netherlands, presented at
, 2009, 'Testing Finitary Probabilistic Processes', in Proceedings of the First International Conference on Advances in Natural Computation (ICNC 2005), Part III, Lecture Notes in Computer Science 3612/2005, Springer, Berlin, Germany, presented at
, 2008, 'Proofs and refutations for probabilistic systems', in Formal methods 2008, Springer, Turku, Finland, presented at
, 2008, 'Proofs and refutations for probabilistic refinement', in Cuellar J; Maibaum T; Sere K (eds.), FM 2008: FORMAL METHODS, PROCEEDINGS, SPRINGER-VERLAG BERLIN, FINLAND, Turku, pp. 100 - +, presented at
, 2007, 'Characterising testing preorders for finite probabilistic processes', in 22nd Annual IEEE symposium on logic in computer science, Institute of Electrical and Electronics Engineers Inc., 445 Hoes Lane / P.O. Box 1331, Piscataway, NJ 08855-1331, United States, Wroclaw, Poland, pp. 313 - 322, presented at
, 2007, 'Scalar outcomes suffice for finitary probabilistic testing', in 16th European symposium on programming, 2007, Braga, Portugal, presented at
, 2006, 'Using Probabilistic Kleene algebra for protocol verification', in Maths of Program Construction, Manchester, England, presented at
, 2006, 'The shadow knows: refinement of ignorance in sequential programs', in Mathematics of program construction, Kurressare, Estonia, presented at
, 2005, 'Probabilistic Guarded Commands Mechanized in HOL', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Barcelona, Spain, presented at
, 2005, 'Development via refinement in probabilistic B - Foundation and case study', in 13th International Conference on FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FoSSaCS 2010), Springer-Verlag, Germany, presented at
, 2005, 'A novel stochastic game via the quantitative modal mu-calculus', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Edinburgh, Scotland, presented at
, 2005, 'Programming-logic analysis of fault tolerance: Expected performance of self-stabilisation', in Butler M; Jones C; Romanovsky A; Troubitsyna E (eds.), RIGOROUS DEVELOPMENT OF COMPLEX FAULT-TOLERANT SYSTEMS, SPRINGER-VERLAG BERLIN, ENGLAND, Newcastle Univ, Newcastle upon Tyne, pp. 288 - +, presented at
, 2004, 'Deriving Probabilistic Semantics vis the Weakest Completion', in 6th International Conference on Formal Engineering Methods, ICFEM 2004, Springer, Seattle, Washington, USA, presented at
, 2004, 'Memoryless strategies for stochastic games via domain theory', in Electronic Notes in Theoretical Computer Science, Elsevier BV, Recife, presented at
, 2003, 'Probabilistic invariants for probabilistic machines', in ZB 2003: Formal Specification and develoment in B and Z, Springer, Turku, Finland, presented at
, 2003, 'Probabilistic Termination in B', in ZB 2003: Formal Specification and develoment in B and Z, Springer, Turku, Finland, presented at
, 2002, 'Games, probability and the quantitative mu-calculus qMu', in Logic for Programming, Artificial Intelligence and Reasoning LNAI 2514, Springer, Tbilisi Georgia, presented at
, 1998, 'The generalised substitution language extended to probabilistie programs', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 9 - 25, http://dx.doi.org/10.1007/bfb0053351
, 1990, 'Refinement of state-based concurrent systems', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 340 - 351, http://dx.doi.org/10.1007/3-540-52513-0_18
, 1989, 'Types and invariants in the refinement calculus', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 363 - 378, http://dx.doi.org/10.1007/3-540-51305-1_22
, 1985, 'Specification of a simplified network service in CSP (Problem 2)', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 345 - 353, http://dx.doi.org/10.1007/3-540-16047-7_56
, 1985, 'Specification of a simplified network service in Z (Problem 2)', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 318 - 344, http://dx.doi.org/10.1007/3-540-16047-7_55
https://orcid.org/0000-0002-8535-9068