ORCID as entered in ROS

Select Publications
2024, 'On Formal Methods Thinking in Computer Science Education', Formal Aspects of Computing, 37, http://dx.doi.org/10.1145/3670419
,2022, 'Flexible and scalable privacy assessment for very large datasets, with an application to official governmental microdata', Proceedings on Privacy Enhancing Technologies, 2022, pp. 378 - 399, http://dx.doi.org/10.56553/popets-2022-0114
,2021, 'The Laplace Mechanism has optimal utility for differential privacy over continuous queries', Proceedings Symposium on Logic in Computer Science, 2021-June, http://dx.doi.org/10.1109/LICS52264.2021.9470718
,2020, 'Preface', Acta Informatica, 57, pp. 305 - 311, http://dx.doi.org/10.1007/s00236-020-00382-7
,2019, 'Program algebra for quantitative information flow', Journal of Logical and Algebraic Methods in Programming, 106, pp. 55 - 77, http://dx.doi.org/10.1016/j.jlamp.2019.04.002
,2019, 'An axiomatization of information flow measures', Theoretical Computer Science, 777, pp. 32 - 54, http://dx.doi.org/10.1016/j.tcs.2018.10.016
,2019, 'Abstract hidden markov models: A monadic account of quantitative information flow', Logical Methods in Computer Science, 15, pp. 36 - 50, http://dx.doi.org/10.23638/LMCS-15(1:36)2019
,2018, 'A new proof rule for almost-sure termination', Proceedings of the ACM on Programming Languages, 2, http://dx.doi.org/10.1145/3158121
,2017, 'Privacy in elections: How small is “small”?', Journal of Information Security and Applications, 36, pp. 112 - 126, http://dx.doi.org/10.1016/j.jisa.2017.08.003
,2014, 'Selected papers from the Brazilian Symposium on Formal Methods (SBMF 2011)', Science of Computer Programming, 92, pp. 85, http://dx.doi.org/10.1016/j.scico.2014.02.004
,2014, 'Abstractions of non-interference security: Probabilistic versus possibilistic', Formal Aspects of Computing, 26, pp. 169 - 194, http://dx.doi.org/10.1007/s00165-012-0237-4
,2014, 'An old new notation for elementary probability theory', Science of Computer Programming, 85, pp. 115 - 136, http://dx.doi.org/10.1016/j.scico.2013.09.003
,2014, 'Hidden-Markov program algebra with iteration', Mathematical Structures in Computer Science, 29, http://dx.doi.org/10.1017/S0960129513000625
,2014, 'Real-reward testing for probabilistic processes', Theoretical Computer Science, 538, pp. 16 - 36, http://dx.doi.org/10.1016/j.tcs.2013.07.016
,2013, 'Lattices of information for security: Deterministic, demonic, probabilistic', Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 8144 LNCS, pp. 1 - 3, http://dx.doi.org/10.1007/978-3-642-41202-8_1
,2012, 'Abstractions of non-interference security: probabilistic versus possibilistic', Formal Aspects of Computing, pp. 1 - 26, http://dx.doi.org/10.1007/s00165-012-0237-4
,2012, 'Compositional noninterference from first principles', Formal Aspects of Computing, 24, pp. 3 - 26, http://dx.doi.org/10.1007/s00165-010-0167-y
,2012, 'Compositional noninterference from first principles', Formal Aspects of Computing, 24, pp. 3 - 26, http://dx.doi.org/10.1007/s00165-010-0167-y
,2010, 'Compositional refinement in agent-based security protocols', Formal Aspects of Computing, http://dx.doi.org/10.1007/s00165-010-0164-1
,2009, 'The Shadow Knows: Refinement and security in sequential programs', Science of Computer Programming, 74, pp. 629 - 653, http://dx.doi.org/10.1016/j.scico.2007.09.003
,2008, 'Characterising Testing Preorders for Finite Probabilistic Processes', Logical Methods in Computer Science, 4, http://dx.doi.org/10.2168/LMCS-4(4:4)2008
,2008, 'Using probabilistic Kleene algebra pKA for protocol verification', Journal of Logic and Algebraic Programming, 76, pp. 90 - 111, http://dx.doi.org/10.1016/j.jlap.2007.10.005
,2007, 'Remarks on Testing Probabilistic Processes', Electronic Notes in Theoretical Computer Science, 172, pp. 359 - 397, http://dx.doi.org/10.1016/j.entcs.2007.02.013
,2007, 'Results on the quantitative mu-calculus qM mu', ACM Transactions on Computational Logic, 8, pp. 3:1 - 3:43
,2006, 'The shadow knows: Refinement of ignorance in sequential programs', Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 4014 LNCS, pp. 359 - 378, http://dx.doi.org/10.1007/11783596_21
,2005, 'Abstraction and refinement in probabilistic systems', ACM SIGMETRICS performance evaluation review, 346, pp. 41 - 47, http://dx.doi.org/10.1145/1059816.1059824
,2005, 'An elementary proof that Herman`s Ring is Theta (N-2)', Information Processing Letters, 94, pp. 79 - 84, http://dx.doi.org/10.1016/j.ipl.2004.12.013
,2005, 'Probabilistic guarded commands mechanised in HOL', Theoretical Computer Science, 346, pp. 96 - 112, http://dx.doi.org/10.1016/j.tcs.2005.08.005
,2005, 'The challenge of probabilistic Event B - Extended abstract', 13th International Conference on FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FoSSaCS 2010), 3455, pp. 162 - 171, http://dx.doi.org/10.1007/11415787_10
,2003, 'Almost-certain eventualities and abstract probabilities in quantitative temporal logic', Theoretical Computer Science, 293, pp. 507 - 534
,2001, 'Cost analysis of games, using program logic', Proceedings of the Asia Pacific Software Engineering Conference and International Computer Science Conference APSEC and ICSC, pp. 351
,2001, 'Partial correctness for probabilistic demonic programs', Theoretical Computer Science, 266, pp. 513 - 541, http://dx.doi.org/10.1016/S0304-3975(00)00208-5
,2001, 'Almost-certain eventualities and abstract probabilities in quantitative temporal logic', Electronic Notes in Theoretical Computer Science, 42, pp. 12 - 40, http://dx.doi.org/10.1016/S1571-0661(04)80876-4
,2001, 'Demonic, angelic and unbounded probabilistic choices in sequential programs', Acta Informatica, 37, pp. 329 - 354, http://dx.doi.org/10.1007/s002360000046
,1998, 'The oxygen permeability of a new type of high Dk soft contact lens material', Optometry and Vision Science, pp. 30 - 36
,1997, 'Hierarchical Reasoning in Probabilistic CSP', Programming and Computer Software, 23, pp. 239 - 250
,1996, 'Unifying wp and wlp', Information Processing Letters, 59, pp. 159 - 163, http://dx.doi.org/10.1016/0020-0190(96)00093-2
,1996, 'Probabilistic Predicate Transformers', ACM Transactions on Programming Languages and Systems, 18, pp. 325 - 353, http://dx.doi.org/10.1145/229542.229547
,1996, 'Refinement-oriented probability for CSP', Formal Aspects of Computing, 8, pp. 617 - 647, http://dx.doi.org/10.1007/BF01213492
,1995, 'Action systems, unbounded nondeterminism, and infinite traces', Formal Aspects of Computing, 7, pp. 37 - 53, http://dx.doi.org/10.1007/BF01214622
,1995, 'Exits in the refinement calculus', Formal Aspects of Computing, 7, pp. 54 - 76, http://dx.doi.org/10.1007/BF01214623
,1994, 'Foreword', Science of Computer Programming, 22, pp. 1 - 2, http://dx.doi.org/10.1016/0167-6423(94)90004-3
,1993, 'A single complete rule for data refinement', Formal Aspects of Computing, 5, pp. 367 - 382, http://dx.doi.org/10.1007/BF01212407
,1991, 'Data refinement of predicate transformers', Theoretical Computer Science, 87, pp. 143 - 162, http://dx.doi.org/10.1016/0304-3975(91)90029-2
,1990, 'Data refinement by calculation', Acta Informatica, 27, pp. 481 - 503, http://dx.doi.org/10.1007/BF00277386
,1990, 'Types and invariants in the refinement calculus', Science of Computer Programming, 14, pp. 281 - 304, http://dx.doi.org/10.1016/0167-6423(90)90024-8
,1988, 'Auxiliary variables in data refinement', Information Processing Letters, 29, pp. 293 - 296, http://dx.doi.org/10.1016/0020-0190(88)90227-X
,1988, 'The Specification Statement', ACM Transactions on Programming Languages and Systems Toplas, 10, pp. 403 - 419, http://dx.doi.org/10.1145/44501.44503
,1988, 'Data refinement by miracles', Information Processing Letters, 26, pp. 243 - 246, http://dx.doi.org/10.1016/0020-0190(88)90147-0
,1988, 'Procedures, parameters, and abstraction: Separate concerns', Science of Computer Programming, 11, pp. 17 - 27, http://dx.doi.org/10.1016/0167-6423(88)90062-7
,