Mads Dam

CoRR, 2023

Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined Processor.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022

Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

HOL4P4: semantics for a verified data plane.

[BibT_eX]

[DOI]

Proceedings of the 5th International Workshop on P4 in Europe, 2022

A Case Study in Information Flow Refinement for Low Level Systems.

[BibT_eX]

[DOI]

Proceedings of the Logic of Software. A Tasting Menu of Formal Methods, 2022

2021

Refinement-Based Verification of Device-to-Device Information Flow.

[BibT_eX]

[DOI]

Ning Dong

Proceedings of the Formal Methods in Computer Aided Design, 2021

On Compositional Information Flow Aware Refinement.

[BibT_eX]

[DOI]

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

Hoare-Style Logic for Unstructured Programs.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 18th International Conference, 2020

InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis.

[BibT_eX]

[DOI]

Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

2019

On the verification of system-level information flow properties for virtualized execution platforms.

[BibT_eX]

[DOI]

Christoph Baumann

J. Cryptogr. Eng., 2019

2018

Formal Verification of Integrity-Preserving Countermeasures Against Cache Storage Side-Channels.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - 7th International Conference, 2018

2017

Compositional Verification of Security Properties for Embedded Execution Platforms.

[BibT_eX]

[DOI]

Christoph Baumann

Proceedings of the PROOFS 2017, 2017

2016

Provably secure memory isolation for Linux on ARM.

[BibT_eX]

[DOI]

J. Comput. Secur., 2016

Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures.

[BibT_eX]

[DOI]

Proceedings of the IEEE Symposium on Security and Privacy, 2016

Automatic Derivation of Platform Noninterference Properties.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

2015

Location-independent routing in process network overlays.

[BibT_eX]

[DOI]

Karl Palmskog

Serv. Oriented Comput. Appl., 2015

Security monitor inlining and certification for multithreaded Java.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2015

Trustworthy Memory Isolation of Linux on Embedded Devices.

[BibT_eX]

[DOI]

Proceedings of the Trust and Trustworthy Computing - 8th International Conference, 2015

Trustworthy Virtualization of the ARMv7 Memory Subsystem.

[BibT_eX]

[DOI]

Hamed Nemati

Proceedings of the SOFSEM 2015: Theory and Practice of Computer Science, 2015

Trustworthy Prevention of Code Injection in Linux on Embedded Devices.

[BibT_eX]

[DOI]

Proceedings of the Computer Security - ESORICS 2015, 2015

2014

Formal Verification of Secure User Mode Device Execution with DMA.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2014

Automating Information Flow Analysis of Low Level Code.

[BibT_eX]

[DOI]

Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

2013

ABS-NET: Fully Decentralized Runtime Adaptation for Distributed Objects.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 6th Interaction and Concurrency Experience, 2013

Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties.

[BibT_eX]

[DOI]

Narges Khakpour

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

Machine code verification of a tiny ARM hypervisor.

[BibT_eX]

[DOI]

Hamed Nemati

Proceedings of the TrustED'13, 2013

Formal verification of information flow security for a simple arm-based separation kernel.

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

Efficient and fully abstract routing of futures in object network overlays.

[BibT_eX]

[DOI]

Karl Palmskog

Proceedings of the 2013 Workshop on Programming based on Actors, 2013

2012

ENCoVer: Symbolic Exploration for Information Flow Security.

[BibT_eX]

[DOI]

Gurvan Le Guernic

Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

TreeDroid: a tree automaton based approach to enforcing data processing policies.

[BibT_eX]

[DOI]

Gurvan Le Guernic

Andreas Lundblad

Proceedings of the ACM Conference on Computer and Communications Security, 2012

2011

An Epistemic Predicate CTL<sup>*</sup> for Finite Control π-Processes.

[BibT_eX]

[DOI]

Dimitar P. Guelev

Proceedings of the 7th Workshop on Methods for Modalities, 2011

Epistemic temporal logic for information flow security.

[BibT_eX]

[DOI]

Gurvan Le Guernic

Proceedings of the 2011 Workshop on Programming Languages and Analysis for Security, 2011

2010

In-Network Monitoring.

[BibT_eX]

[DOI]

Proceedings of the Algorithms for Next Generation Networks, 2010

A gossiping protocol for detecting global threshold crossings.

[BibT_eX]

[DOI]

IEEE Trans. Netw. Serv. Manag., 2010

Provably correct inline monitoring for multithreaded Java-like programs.

[BibT_eX]

[DOI]

J. Comput. Secur., 2010

A Proof Carrying Code Framework for Inlined Reference Monitors in Java Bytecode

[BibT_eX]

[DOI]

Andreas Lundblad

CoRR, 2010

The Accuracy of Tree-based Counting in Dynamic Networks

[BibT_eX]

[DOI]

Supriya Krishnamurthy

CoRR, 2010

Brief announcement: the accuracy of tree-based counting in dynamic networks.

[BibT_eX]

[DOI]

Supriya Krishnamurthy

Fetahi Zebenigus Wuhib

Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, 2010

Practical Private Information Aggregation in Large Networks.

[BibT_eX]

[DOI]

Gunnar Kreitz

Douglas Wikström

Proceedings of the Information Security Technology for Applications, 2010

Towards Flexible and Secure Distributed Aggregation.

[BibT_eX]

[DOI]

Kristján Valur Jónsson

Mads F. Dam

Proceedings of the Mechanisms for Autonomous Management of Networks and Services, 2010

2009

Robust monitoring of network-wide aggregates through gossiping.

[BibT_eX]

[DOI]

IEEE Trans. Netw. Serv. Manag., 2009

Provably correct runtime monitoring.

[BibT_eX]

[DOI]

Irem Aktug

J. Log. Algebraic Methods Program., 2009

Gossiping for threshold detection.

[BibT_eX]

[DOI]

Proceedings of the Integrated Network Management, 2009

A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2009, 2009

Security Monitor Inlining for Multithreaded Java.

[BibT_eX]

[DOI]

Proceedings of the ECOOP 2009, 2009

A Data Symmetry Reduction Technique for Temporal-epistemic Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2009

Abstraction in model checking multi-agent systems.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2009), 2009

2008

Decentralized detection of global threshold crossings using aggregation trees.

[BibT_eX]

[DOI]

Comput. Networks, 2008

Decentralized real-time monitoring of network-wide aggregates.

[BibT_eX]

[DOI]

Alberto Gonzalez Prieto

Proceedings of the 2nd Workshop on Large-Scale Distributed Systems and Middleware, 2008

2007

A Complete Axiomatization of Knowledge and Cryptography.

[BibT_eX]

[DOI]

Mika Cohen

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2006

Decidability and proof systems for language-based noninterference relations.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

2005

Decentralized Computation of Threshold Crossing Alerts.

[BibT_eX]

[DOI]

Proceedings of the Ambient Networks, 2005

2004

On the secure implementation of security protocols.

[BibT_eX]

[DOI]

Pablo Giambiagi

Sci. Comput. Program., 2004

2003

A verification tool for ERLANG.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2003

On global induction mechanisms in a µ-calculus with explicit approximations.

[BibT_eX]

[DOI]

Christoph Sprenger

RAIRO Theor. Informatics Appl., 2003

Formal Methods Research at SICS and KTH: An Overview.

[BibT_eX]

[DOI]

Lars-Åke Fredlund

Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems, 2003

Regular SPKI (Discussion).

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 2003

Regular SPKI.

[BibT_eX]

[DOI]

Proceedings of the Security Protocols, 2003

On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the µ-Calculus.

[BibT_eX]

[DOI]

Christoph Sprenger

Proceedings of the Foundations of Software Science and Computational Structures, 2003

Proof Systems for π-Calculus Logics.

[BibT_eX]

[DOI]

Proceedings of the Logic for Concurrency and Synchronisation, 2003

2002

µ-Calculus with Explicit Points and Approximations.

[BibT_eX]

[DOI]

J. Log. Comput., 2002

Constrained Delegation.

[BibT_eX]

[DOI]

Olav L. Bandmann

Babak Sadighi Firozabadi

Proceedings of the 2002 IEEE Symposium on Security and Privacy, 2002

A note on global induction in a mu-calculus with explicit approximations.

[BibT_eX]

Christoph Sprenger

Proceedings of the Fixed Points in Computer Science, 2002

2000

Confidentiality for Mobile Code: The Case of a Simple Payment Protocol.

[BibT_eX]

[DOI]

Pablo Giambiagi

Proceedings of the 13th IEEE Computer Security Foundations Workshop, 2000

1999

Verifying a Distributed Database Lookup Manager Written in Erlang.

[BibT_eX]

[DOI]

Thomas Arts

Proceedings of the FM'99 - Formal Methods, 1999

Compositional Verification of CCS Processes.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of System Informatics, 1999

1998

Proving Properties of Dynamic Process Networks.

[BibT_eX]

[DOI]

Inf. Comput., 1998

On the verification of open distributed systems.

[BibT_eX]

[DOI]

Lars-Åke Fredlund

Proceedings of the 1998 ACM symposium on Applied Computing, 1998

Proving Trust in Systems of 2nd-Order Processes: Preliminary Results.

[BibT_eX]

[DOI]

Proceedings of the Thirty-First Annual Hawaii International Conference on System Sciences, 1998

From Higher-Order pi-Calculus to pi-Calculus in the Presence of Static Operators.

[BibT_eX]

[DOI]

José-Luis Vivas

Proceedings of the CONCUR '98: Concurrency Theory, 1998

System Description: Verification of Distributed Erlang Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

1997

On the Decidability of Process Equivalences for the pi-Calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1997

Toward Parametric Verification of Open Distributed Systems.

[BibT_eX]

[DOI]

Lars-Åke Fredlund

Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

1996

Model Checking Mobile Processes.

[BibT_eX]

[DOI]

Inf. Comput., 1996

Modalities in Analysis and Verification.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

Logical and Operational Methods in the Analysis of Programs and Systems.

[BibT_eX]

[DOI]

Proceedings of the Analysis and Verification of Multiple-Agent Languages, 1996

Toward a Modal Theory of Types for the pi-Calculus.

[BibT_eX]

[DOI]

Roberto M. Amadio

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1996

1995

Reasoning about Higher-Order Processes.

[BibT_eX]

[DOI]

Roberto M. Amadio

Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Compositional Proof Systems for Model Checking Infinite State Processes.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '95: Concurrency Theory, 1995

1994

CTL* and ECTL* as Fragments of the Modal mu-Calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1994

Process-Algebraic Interpretations of Positive Linear and Relevant Logics.

[BibT_eX]

[DOI]

J. Log. Comput., 1994

1992

R-Generability, and Definability in Branching Time Logics.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1992

Fixed Points of Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1992

CTL* and ECTL* as Fragments of the Modal µ-Calculus.

[BibT_eX]

[DOI]

Proceedings of the CAAP '92, 1992

1988

Relevance Logic and Concurrent Composition

[BibT_eX]

[DOI]

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

1986

Compiler Generation from Relational Semantics.

[BibT_eX]

[DOI]