Mads Dam: Selected publications

Refereed journal publications and book chapters:

M. Dam, B. Jacobs, A. Lundblad, F. Piessens "Security Monitor Inlining and Certification for Multithreaded Java," to appear in Mathematical Structures in Computer Science (MSCS), Cambridge University Press

F. Wuhib, R. Stadler, M. Dam "A Gossiping Protocol for Detecting Global Threshold Crossings," IEEE Transactions on Network and Service Management (TNSM), vol. 7, no. 1, March 2010

F. Wuhib, M. Dam, R. Stadler, A. Clemm “Robust Monitoring of Network-wide Aggregates through Gossiping,” IEEE Transactions on Network and Service Management (TNSM), Vol. 6, No. 2, June 2009

D. Raz, R. Stadler, C. Elster, and M. Dam, “In-Network Monitoring,” in: G. Cormode, M. Thottan (Eds.), Algorithms for Next Generation Networks, Springer, to appear Feb 2010

M. Dam, B. Jacobs, A. Lundblad, F. Piessens: “Provably Correct Inline Monitoring for Multi-threaded Java-like Programs”, Journal of Computer Security vol 18, number 1, pp. 37-59, 2010. [pdf]

I. Aktug, M. Dam, D. Gurov: “Provably Correct Runtime Monitoring”, Journal of Logic and Algebraic Programming. Volume 78, Issue 5, Pages 304-339 (May-June 2009). [pdf, ps ]

M. Cohen, M. Dam: “A Completeness result for BAN logic”, To appear in Journal of Logic, Language, and Information. [pdf]

F. Wuhib, M. Dam, R. Stadler, A. Clemm. “Decentralized Detection of Global Threshold Crossings Using Aggregation Trees.” Computer Networks 52 (2008) 1745–1761 [pdf]

C. Sprenger and M. Dam: “A Note on Global Induction Mechanisms in a µ-Calculus With Explicit Approximations", Theoretical Informatics and Applications vol. 37, 2003, pp. 365-399, special issue on FICS’02. [pdf,ps]

P. Giambiagi, M. Dam: “On the Secure Implementation of Security Protocols”, Science of Computer Programming vol. 50, issue 1-3, 2004, pp. 73-99, special issue on ESOP’03. [pdf]

L.-å. Fredlund, D. Gurov, T. Noll, M. Dam, T. Arts, G. Chugunov. “A Verification Tool for Erlang.” Int. Journal on Software Tools for Technology Transfer vol. 4, issue 4, pp. 405-420, Springer Verlag 2003. [pdf, ps]

M. Dam: “Proof Systems for Pi-Calculus Logics”. In R. de Queiroz (ed.), "Logic for Concurrency and Synchronisation", Trends in Logic, Logica Library, Kluwer, 2003, pp. 145-212. [pdf, ps]

M. Dam and D. Gurov: “Mu-Calculus with Explicit Points and Approximations”, Journal of Logic and Computation, vol. 12, issue 2, April 2002, pp. 255-269. [pdf]

M. Dam: ``Proving Properties of Dynamic Process Networks''. Information and Computation vol. 140, 1998, pp. 95-114. [pdf, ps]

M. Dam, L.-å. Fredlund and D. Gurov. "Toward Parametric Verification of Open Distributed Systems." In: Compositionality: The Significant Difference (H. Langmaack, A. Pnueli, W.-P. De Roever (eds.)), LNCS vol. 1536, Springer Verlag 1998, pp. 150-185. [pdf, ps]

M. Dam. "On the Decidability of Process Equivalences for the pi-Calculus". Theoretical Computer Science vol. 183, 1997, pp. 215-228. [pdf, ps]

M. Dam. ``Modalities in Analysis and Verification''. ACM Computing Surveys Symposium on Models of Programming Languages and Computation, vol. 28, issue 2, (June 1996), pp. 346-348. [pdf, ps]

M. Dam. "Model Checking Mobile Processes". Information and Computation vol. 129, issue 1, 1996, pp. 35-51. [pdf, ps]

M. Dam. ``CTL* and ECTL* as Fragments of the Modal mu-Calculus''. Theoretical Computer Science vol. 126, 1994, pp. 77-96. [pdf, ps]

M. Dam. ``Process-Algebraic Interpretations of Positive Linear and Relevant Logics''. Journal of Logic and Computation vol. 4, 1994, pp. 939-973. [pdf, ps]

M. Dam. ``R-Generability, and Definability in Branching Time Logics''. Information Processing Letters vol. 41, 1992, pp. 281-287. [pdf, ps (abstract only)]

Refereed conference and workshop publications:

D. Guelev, M. Dam: "An epistemic predicate CTL* for finite control pi-processes" Proc. LAMAS 2011

G. Kreitz, D. Wikström, M. Dam: "Practical Private Information Aggregation in Large Networks" Proc. NordSec 2010.

K. Palmskog, A.G. Prieto, C. Meirosu, R. Stadler, M. Dam: "Scalable metadata-directed search in a network of information" Proc Future Network and Mobile Summit, Florence, Italy, June 2010.

K. Jónsson, M. Dam: "Towards Flexible and secure distributed aggregation", Proc. AIMS'10, 4th International Conference on Autonomous Infrastructure, Management and Security, Zurich, Switzerland, 2010, Springer Lecture Notes in Computer Science, vol. 6155, pp. 159-162

S. Krishnamurthy, J. Ardelius, E. Aurell, M. Dam, R. Stadler, F. Z. Wuhib: "Brief announcement: The accuracy of tree-based counting in dynamic networks", Proc. PODC'10, Proc. 29th Annual ACM Symposium on Principles of Distributed Computing, Zurich, Switzerland, 2010, pp. 291-292

M. Cohen, M. Dam, A. Lomuscio, H. Qu: "A Data Symmetry Reduction Technique for Temporal-Epistemic Logic", in Proc. ATVA'09

M. Cohen, A. Lomuscio, M. Dam, H. Qu: “A symmetry reduction technique for model checking temporal epistemic logic”, in Proc. IJCAI'09 [pdf]

M. Dam, B. Jacobs, A. Lundblad, F. Piessens: “Security monitor inlining for multithreaded Java”, in Proc. ECOOP'09 [pdf]

R. Stadler, M. Dam, A. Gonzalez, F. Wuhib: “Decentralized Real-Time Monitoring of Network-Wide Aggregates”, Proc. 2nd Workshop on Large-Scale Distributed Systems and Middleware 2008. ISBN:978-1-60558-296-2. Appeared 2009 [pdf]

M. Cohen, M. Dam, A. Lomuscio, F. Russo: “Abstraction in  Model Checking Multi-agent Systems”, in Proc. AAMAS’09 [pdf]

F. Wuhib, R. Stadler, M. Dam: “Gossiping for Threshold Detection”, in Proc. Integrated Management (IM), 2009 [pdf]

I. Aktug, M. Dam, D. Gurov. “Provably Correct Runtime Monitoring”. In Proc. FM’08. [pdf]

M. Cohen, M. Dam. “A Complete Axiomatization of Knowledge and Cryptography.” In Proc. LICS’07, pp. 77-88. [pdf]

Wuhib, R. Stadler, M. Dam, A. Clemm. "Robust Monitoring of Network-wide Aggregates through Gossiping." In Proc. Integrated Management (IM) 2007, pp. 226-235. [pdf, ps]

M. Dam: “Decidability and Proof Systems for Language-Based Noninterference Relations”. Proc. POPL’06, Charleston, SC, 2006, pp. 67-78. [pdf]

M. Cohen, M. Dam: “A Completeness Result for BAN Logics”, in Proc. Methods for Modalities (M4M), Berlin, Dec. 2005, pp. 202-219. [pdf]

M. Dam, R. Stadler. "A Generic Protocol for Network State Aggregation". Proc. Radiovetenskap och Kommunikation (RVK), Linköping 2005. [pdf]

F. Wuhib, M. Dam, R. Stadler, A. Clemm. "Decentralized Computation of Threshold Crossing Alerts." in Proc. DSOM'05. [pdf]

M. Cohen and M. Dam: "Logical Omniscience in the Semantics of BAN Logics", in Proc. FCS'05, Chicago, 2005, pp. 121-132. [pdf]

M. Dam: “Regular SPKI”, Proc. 2003 Cambridge Security Protocols Workshop, Cambridge, U.K., LNCS vol 3364, pp. 134-150. [pdf]

P. Giambiagi, M. Dam: “On the Secure Implementation of Security Protocols”, Proc. ESOP’03, Springer LNCS vol. 2618, pp. 144-158 [pdf]

C. Sprenger and M. Dam: “On the Structure of Inductive Reasoning: Circular and Tree-shaped Proofs in the mu-Calculus”, Proc. FOSSACS’03, Springer LNCS vol. 2620, pp. 425-440. [pdf]

O. Bandmann and M. Dam: "A Note on SPKI's Authorisation Syntax". Proc. 1st International PKI Research Workshop, NIST, Gaithersburg, MD, 2002, pp. 127-138. [pdf]

O. Bandmann, M. Dam and B. Sadighi: "Constrained Delegation". In Proc. IEEE Symposium on Security and Privacy, Berkeley, California, 2002, pp. 131-142. [pdf]

C. Sprenger and M. Dam: “A Note on Global Induction Mechanisms in a µ-Calculus With Explicit Approximations", In Proc. FICS’02, Copenhagen, Denmark, 2002. [pdf]

M. Dam and D. Gurov: “Mu-Calculus with Explicit Points and Approximations”, in Proc. FICS’00, Paris, France, 2002. [pdf]

M. Dam, G. Karlsson, B. S. Firozabadi, R. Stadler: “A Research Agenda for Distributed Policy-Based Management”, in Proc. Radiovetenskap och Kommunikation (RVK), Stockholm 2002. [pdf]

M. Dam and P. Giambiagi: "Confidentiality for Mobile Code: The Case of a Simple Payment Protocol". Proc. 13th Computer Science Foundations Workshop, 2000, pp. 233-244. [pdf]

M. Dam and D. Gurov: "Compositional Verification of CCS Processes". Proc. PSI'99, Springer Lecture notes in Computer Science, vol. 1755, 1999, pp. 247-256. [pdf]

T. Arts and M. Dam: "Verifying a Distributed Database Lookup Manager Written in Erlang". Proc. FM'99, Springer Lecture Notes in Computer Science, vol. 1708, 1999, pp. 682-700. [pdf]

T. Arts, M. Dam, L.-å. Fredlund and D. Gurov. "System Description: Verification of Distributed Erlang Programs." In Proc. of CADE'98, Springer LNAI, vol. 1421, pp. 38-41, 1998. [pdf]

M. Dam and L.-å. Fredlund. "On the Verification of Open Distributed Systems." Proc. SAC'98, ACM Press, 1998, pp. 532-540. [pdf]

J.-L. Vivas and M. Dam: "From Higher-Order pi-Calculus to pi-Calculus in the Presence of Static Operators". Proc. CONCUR'98, Springer Lecture Notes in Computer Science, vol. 1466, 1998, pp. 115-130. [pdf]

M. Dam.  "Proving Trust in Systems of Second-Order Processes (Extended Abstract)" in Proc. HICSS'98, Vol. VII, IEEE Computer Science Press, pp. 255-264, 1998. [pdf, full version]

M. Dam, L.-å. Fredlund, D. Gurov. ”Compositional Verification of Erlang Programs'.' In Proc.Third International Workshop on Formal Methods for Industrial Critical Systems (FMICS), CWI, 1998. [pdf]

R. Amadio and M. Dam. ``Toward a Modal Theory of Types for the pi-Calculus''. In Proc. FTRTFT'96, Springer Lecture Notes in Computer Science, vol. 1135, 1996, pp. 347-365. [pdf]

M. Dam: ``Compositional proof systems for model checking infinite state processes'', Proc. CONCUR'95, Springer Lecture notes in Computer Science, vol. 962, 1995, pp. 12-26. [pdf]

R. Amadio, M. Dam. ``Reasoning about Higher-Order Processes''. Proc. CAAP'95, Springer Lecture Notes in Computer Science, vol. 915, pp. 202-217. [pdf]

M. Dam. "On the Decidability of Process Equivalences for the pi-Calculus". Proc. AMAST'95, Springer Lecture notes in Computer Science, vol. 936, 1995, pp. 169-183.

M. Dam. "Model Checking Mobile Processes". In Proc. CONCUR’93, Springer Lecture Notes in Computer Science, vol. 715, 1993, pp. 22-36. [pdf]

M. Dam. ``Fixed Points of Buchi Automata''. In Proceedings of 12th Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 652, 1992, pp. 39-50. [pdf]

M. Dam. ``CTL* and ECTL* as Fragments of the Modal mu-Calculus''. In Proc. CAAP’92, Springer Lecture Notes in Computer Science, vol. 581, 1992, pp. 145-164.

M. Dam. ``Relevance Logic and Concurrent Composition''. Proc. LICS'88, pp. 178-185. [pdf]

M. Dam, F. Jensen. ``Compiler Generation from Relational Semantics''. Proceedings of the European Symposium on Programming, Lecture Notes in Computer Science 213 (1986) pp. 1-29.  

Books and theses:

M. Dam (ed). ``Analysis and Verification of Multiple Agent Languages´´, Proc. 5th LOMAPS Workshop, Springer Lecture Notes in Computer Science, vol. 1192, 1997.

M. Dam. ``Relevance Logic and Concurrent Composition''. PhD thesis, Dept. of Computer Science, University of Edinburgh, 1990, CST-66-90. Also published as ECS-LFCS-90-119.

Other, unrefereed:

M. Dam, L.-å. Fredlund and D. Gurov: “Formal Methods Research at SICS and KTH: An Overview”, Proc. Formal Methods for Industrial Critical Systems (FMICS), Trondheim . Electr. Notes Theor. Comput. Sci. 80, Springer-Verlag 2003.

F. Nielson, P. Cousot, M. Dam, P. Degano, P. Jouvelot, A. Mycroft, B. Thomsen: “Logical and Operational Methods in the Analysis of Programs and Systems”. Proc. 5th LOMAPS Workshop, Springer Lecture Notes in Computer Science, vol. 1192, 1997, pp. 1-21.