Arrow Research search

Author name cluster

Martín Abadi

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

15 papers
2 author rows

Possible papers

15

ICLR Conference 2017 Conference Paper

Semi-supervised Knowledge Transfer for Deep Learning from Private Training Data

  • Nicolas Papernot
  • Martín Abadi
  • Úlfar Erlingsson
  • Ian J. Goodfellow
  • Kunal Talwar

Some machine learning applications involve training data that is sensitive, such as the medical histories of patients in a clinical trial. A model may inadvertently and implicitly store some of its training data; careful analysis of the model may therefore reveal sensitive information. To address this problem, we demonstrate a generally applicable approach to providing strong privacy guarantees for training data: Private Aggregation of Teacher Ensembles (PATE). The approach combines, in a black-box fashion, multiple models trained with disjoint datasets, such as records from different subsets of users. Because they rely directly on sensitive data, these models are not published, but instead used as ''teachers'' for a ''student'' model. The student learns to predict an output chosen by noisy voting among all of the teachers, and cannot directly access an individual teacher or the underlying data or parameters. The student's privacy properties can be understood both intuitively (since no single teacher and thus no single dataset dictates the student's training) and formally, in terms of differential privacy. These properties hold even if an adversary can not only query the student but also inspect its internal workings. Compared with previous work, the approach imposes only weak assumptions on how teachers are trained: it applies to any model, including non-convex models like DNNs. We achieve state-of-the-art privacy/utility trade-offs on MNIST and SVHN thanks to an improved privacy analysis and semi-supervised learning.

CSL Conference 2015 Conference Paper

The Prophecy of Timely Rollback (Invited Talk)

  • Martín Abadi

Techniques for rollback recovery play a central role in ensuring fault-tolerance in many distributed systems. This talk addresses the formal specification and analysis of those techniques. In particular, we will discuss the relevance of prophecy variables (auxiliary program variables whose values are defined in terms of current program state and future behavior) to reasoning about systems with undo operations. We will then focus on a model for data-parallel computation with a notion of virtual time. In this model, rollbacks allow the selective undo of work at particular virtual times. A refinement theorem ensures the consistency of rollbacks. This talk is largely based on joint work with Michael Isard.

I&C Journal 2010 Journal Article

A model of dynamic separation for transactional memory

  • Martín Abadi
  • Tim Harris
  • Katherine F. Moore

Dynamic separation is a new programming discipline for systems with transactional memory. We study it formally in the setting of a small calculus with transactions. We provide a precise formulation of dynamic separation and compare it with other programming disciplines. Furthermore, exploiting dynamic separation, we investigate some possible implementations of the calculus and we establish their correctness.

TCS Journal 2006 Journal Article

Deciding knowledge in security protocols under equational theories

  • Martín Abadi
  • Véronique Cortier

The analysis of security protocols requires precise formulations of the knowledge of protocol participants and attackers. In formal approaches, this knowledge is often treated in terms of message deducibility and indistinguishability relations. In this paper we study the decidability of these two relations. The messages in question may employ functions (encryption, decryption, etc.) axiomatized in an equational theory. One of our main positive results says that deducibility and indistinguishability are both decidable in polynomial time for a large class of equational theories. This class of equational theories is defined syntactically and includes, for example, theories for encryption, decryption, and digital signatures. We also establish general decidability theorems for an even larger class of theories. These theorems require only loose, abstract conditions, and apply to many other useful theories, for example with blind digital signatures, homomorphic encryption, XOR, and other associative–commutative functions.

LPAR Conference 2004 Conference Paper

BCiC: A System for Code Authentication and Verification

  • Nathan Whitehead
  • Martín Abadi

Abstract We present BCiC, a system for verifying and authenticating code that combines language-based proof methods with public-key digital signatures. BCiC aims to augment the rigor of formal proofs about intrinsic properties of code by relying on authentication and trust relations. BCiC integrates the Binder security language with the Calculus of (Co)Inductive Constructions (CiC). In this respect, it is a descendant of our previous logic BLF, which was based on LF rather than CiC. This paper focuses on the architecture and implementation of BCiC. In addition to a logical inference engine, the design most notably includes a network communication module for the efficient exchange of logical facts between hosts, and a cryptography module for generating and checking signatures. The implementation cooperates with the Open Verifier, a state-of-the-art system for proof-carrying code with modular checkers.

TCS Journal 2003 Journal Article

Secrecy types for asymmetric communication

  • Martín Abadi
  • Bruno Blanchet

We develop a typed process calculus for security protocols in which types convey secrecy properties. We focus on asymmetric communication primitives, especially on public-key encryption. These present special difficulties, partly because they rely on related capabilities (e. g. , “public” and “private” keys) with different levels of secrecy and scopes.

MFCS Conference 1995 Conference Paper

An Abstract Account of Composition

  • Martín Abadi
  • Stephan Merz

Abstract We present a logic of specifications of reactive systems. The logic is independent of particular computational models, but it captures common patterns of reasoning with assumption-commitment specifications. We use the logic for deriving proof rules for TLA and CTL * specifications.

TCS Journal 1993 Journal Article

A logical view of composition

  • Martín Abadi
  • Gordon D. Plotkin

We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification approaches; one of the logics is intuitionistic, while the other one is linear.

TCS Journal 1991 Journal Article

The existence of refinement mappings

  • Martín Abadi
  • Leslie Lamport

Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. We consider specifications consisting of a state machine (which may be infinite- state) that specifies safety requirements, and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S1 to a higher-level one S2 is a mapping from S1 's state space to S2 's state space. It maps steps of S1 's state machine to steps of S2 's state machine and maps behaviors allowed by S1 to behaviors allowed by S2. We show that, under reasonable assumptions about the specification, if S1 implements S2, then by adding auxiliary variables to S1 we can guarantee the existence of a refinement mapping. This provides a completeness result for a practical, hierarchical specification method.

FOCS Conference 1989 Conference Paper

Decidability and Expressiveness for First-Order Logics of Probability (Extended Abstract)

  • Martín Abadi
  • Joseph Y. Halpern

Decidability and expressiveness issues for two first-order logics of probability are considered. In one the probability is on possible worlds, whereas in the other it is on the domain. It turns out that in both cases it takes very little to make reasoning about probability highly undecidable. It is shown that, when the probability is on the domain, if the language contains only unary predicates, then the validity problem is decidable. However, if the language contains even one binary predicate, the validity problem is Pi /sub 1//sup 2/ as hard as elementary analysis with free predicate and function symbols. With equality in the language, even with no other symbol, the validity problem is at least as hard as that for elementary analysis, Pi /sub infinity //sup 1/. Thus, the logic cannot be axiomatized in either case. When the probability is on the set of possible worlds, the validity problem is Pi /sub 1//sup 2/ complete with as little as one unary predicate in the language, even without equality. With equality, Pi /sub infinity //sup 1/ hardness with only a constant symbol is obtained. In many applications it suffices to restrict attention to domains of a bounded size; it is shown that the logics are decidable in this case. >

TCS Journal 1989 Journal Article

The power of temporal proofs

  • Martín Abadi

Some methods for reasoning about concurrent programs and hardware devices have been based on proof systems for temporal logic. Unfortunately, all effective proof systems for temporal logic are incomplete for the standard semantics, in the sense that some formulas hold in every intended model but cannot be proved. We evaluate and compare the power of several proof systems for temporal logic. Specifically, we relate temporal systems to classical systems with explicit time parameters. A typical temporal system turns out to be incomplete in a strong sense; we exhibit a short, valid formula it fails to prove. We suggest the addition of new rules to define auxiliary predicates. With these rules, we obtain nonstandard soundness and completeness results. In particular, one of the simple temporal systems we describe is as powerful as Peano Arithmetic.

v2026.09.13