8 Search Results for "Zanella-B�guelin, Santiago"

Document
DOI: 10.4230/LIPIcs.ICDT.2023.12
How Do Centrality Measures Choose the Root of Trees?

Authors: Cristian Riveros, Jorge Salas, and Oskar Skibski

Published in: LIPIcs, Volume 255, 26th International Conference on Database Theory (ICDT 2023)

Abstract
Centrality measures are widely used to assign importance to graph-structured data. Recently, understanding the principles of such measures has attracted a lot of attention. Given that measures are diverse, this research has usually focused on classes of centrality measures. In this work, we provide a different approach by focusing on classes of graphs instead of classes of measures to understand the underlying principles among various measures. More precisely, we study the class of trees. We observe that even in the case of trees, there is no consensus on which node should be selected as the most central. To analyze the behavior of centrality measures on trees, we introduce a property of tree rooting that states a measure selects one or two adjacent nodes as the most important, and the importance decreases from them in all directions. This property is satisfied by closeness centrality but violated by PageRank. We show that, for several centrality measures that root trees, the comparison of adjacent nodes can be inferred by potential functions that assess the quality of trees. We use these functions to give fundamental insights on rooting and derive a characterization explaining why some measure root trees. Moreover, we provide an almost linear time algorithm to compute the root of a graph by using potential functions. Finally, using a family of potential functions, we show that many ways of tree rooting exist with desirable properties.
Cite as

Cristian Riveros, Jorge Salas, and Oskar Skibski. How Do Centrality Measures Choose the Root of Trees?. In 26th International Conference on Database Theory (ICDT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 255, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{riveros_et_al:LIPIcs.ICDT.2023.12,
  author =	{Riveros, Cristian and Salas, Jorge and Skibski, Oskar},
  title =	{{How Do Centrality Measures Choose the Root of Trees?}},
  booktitle =	{26th International Conference on Database Theory (ICDT 2023)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-270-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{255},
  editor =	{Geerts, Floris and Vandevoort, Brecht},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2023.12},
  URN =		{urn:nbn:de:0030-drops-177545},
  doi =		{10.4230/LIPIcs.ICDT.2023.12},
  annote =	{Keywords: Databases, centrality measures, data centrality, graph theory, tree structures}
}
Document
Extended Abstract
DOI: 10.4230/LIPIcs.ECOOP.2022.34
Slicing of Probabilistic Programs Based on Specifications (Extended Abstract)

Authors: Marcelo Navarro and Federico Olmedo

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We present the first slicing approach for probabilistic programs based on specifications. Concretely, we show that when probabilistic programs are accompanied by their functional specifications in the form of pre- and post-condition, one can exploit this semantic information to produce specification-preserving slices strictly more precise than slices yielded by conventional techniques based on data/control dependency. To illustrate this, assume that Alice and Bob repeatedly flip a fair coin until observing a matching outcome, either both heads or both tails. However, Alice decides to "trick" Bob and switches the outcome of her coin, before comparing it to Bob’s. The game can be encoded by the program below, which is instrumented with a variable n that tracks the required number of rounds until observing the first match. The program terminates after K loop iterations with probability 1/(2^K) provided K > 0, and with probability 0 otherwise, satisfying the annotated specification. \\ pre: 1/(2^K) [K > 0] n := 0; a, b := 0, 1; while (a ̸= b) do n := n + 1; {a := 0} [1/2] {a := 1}; a := 1 − a; {b := 0} [1/2] {b := 1} \\ post: [n = K] Traditional slicing techniques based on data/control dependencies conclude that the only valid slice of the program (w.r.t. output variable n) is the very same program. However, our slicing approach allows removing the assignment a := 1-a from the loop body, while preserving the program specification. At the technical level, our slicing technique works by propagating post-conditions backward using the greatest pre-expectation transformer - the probabilistic counterpart of Dijkstra’s weakest pre-condition transformer. This endows programs with an axiomatic semantics, expressed in terms of a verification condition generator (VCGen) that yields quantitative proof obligations. In particular, we design (and prove sound) VCGens for both the partial (allowing divergence) and the total (requiring termination) correctness of probabilistic programs, making our slicing technique termination-sensitive. To handle iteration, we assume that program loops are annotated with invariants. To reason about (probabilistic) termination, we assume that loop annotations also include (probabilistic) variants. Another appealing property of our slicing technique is its modularity: It yields valid slices of a program from valid slices of its subprograms. Most importantly, this involves only local reasoning. Besides developing the theoretical foundations of our slicing approach, we also exhibit an algorithm for computing program slices. Interestingly, the algorithm computes the least slice that can be derived from the slicing approach, according to a proper notion of slice size, using, as main ingredient, a shortest-path algorithm. Finally, we demonstrate the applicability of our approach by means of a few illustrative examples and a case study from the probabilistic modeling field.
Cite as

Marcelo Navarro and Federico Olmedo. Slicing of Probabilistic Programs Based on Specifications (Extended Abstract). In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 34:1-34:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{navarro_et_al:LIPIcs.ECOOP.2022.34,
  author =	{Navarro, Marcelo and Olmedo, Federico},
  title =	{{Slicing of Probabilistic Programs Based on Specifications}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{34:1--34:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.34},
  URN =		{urn:nbn:de:0030-drops-162628},
  doi =		{10.4230/LIPIcs.ECOOP.2022.34},
  annote =	{Keywords: probabilistic programming, program slicing, expectation transformer semantics, verification condition generator}
}
Document
DOI: 10.4230/OASIcs.SLATE.2021.10
LeMe-PT: A Medical Package Leaflet Corpus for Portuguese

Authors: Alberto Simões and Pablo Gamallo

Published in: OASIcs, Volume 94, 10th Symposium on Languages, Applications and Technologies (SLATE 2021)

Abstract
The current trend on natural language processing is the use of machine learning. This is being done on every field, from summarization to machine translation. For these techniques to be applied, resources are needed, namely quality corpora. While there are large quantities of corpora for the Portuguese language, there is the lack of technical and focused corpora. Therefore, in this article we present a new corpus, built from drug package leaflets. We describe its structure and contents, and discuss possible exploration directions.
Cite as

Alberto Simões and Pablo Gamallo. LeMe-PT: A Medical Package Leaflet Corpus for Portuguese. In 10th Symposium on Languages, Applications and Technologies (SLATE 2021). Open Access Series in Informatics (OASIcs), Volume 94, pp. 10:1-10:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{simoes_et_al:OASIcs.SLATE.2021.10,
  author =	{Sim\~{o}es, Alberto and Gamallo, Pablo},
  title =	{{LeMe-PT: A Medical Package Leaflet Corpus for Portuguese}},
  booktitle =	{10th Symposium on Languages, Applications and Technologies (SLATE 2021)},
  pages =	{10:1--10:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-202-0},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{94},
  editor =	{Queir\'{o}s, Ricardo and Pinto, M\'{a}rio and Sim\~{o}es, Alberto and Portela, Filipe and Pereira, Maria Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2021.10},
  URN =		{urn:nbn:de:0030-drops-144277},
  doi =		{10.4230/OASIcs.SLATE.2021.10},
  annote =	{Keywords: drug corpora, information extractiom, word embeddings}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2020.21
Optimal Joins Using Compact Data Structures

Authors: Gonzalo Navarro, Juan L. Reutter, and Javiel Rojas-Ledesma

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)

Abstract
Worst-case optimal join algorithms have gained a lot of attention in the database literature. We now count with several algorithms that are optimal in the worst case, and many of them have been implemented and validated in practice. However, the implementation of these algorithms often requires an enhanced indexing structure: to achieve optimality we either need to build completely new indexes, or we must populate the database with several instantiations of indexes such as B+-trees. Either way, this means spending an extra amount of storage space that may be non-negligible. We show that optimal algorithms can be obtained directly from a representation that regards the relations as point sets in variable-dimensional grids, without the need of extra storage. Our representation is a compact quadtree for the static indexes, and a dynamic quadtree sharing subtrees (which we dub a qdag) for intermediate results. We develop a compositional algorithm to process full join queries under this representation, and show that the running time of this algorithm is worst-case optimal in data complexity. Remarkably, we can extend our framework to evaluate more expressive queries from relational algebra by introducing a lazy version of qdags (lqdags). Once again, we can show that the running time of our algorithms is worst-case optimal.
Cite as

Gonzalo Navarro, Juan L. Reutter, and Javiel Rojas-Ledesma. Optimal Joins Using Compact Data Structures. In 23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{navarro_et_al:LIPIcs.ICDT.2020.21,
  author =	{Navarro, Gonzalo and Reutter, Juan L. and Rojas-Ledesma, Javiel},
  title =	{{Optimal Joins Using Compact Data Structures}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020.21},
  URN =		{urn:nbn:de:0030-drops-119453},
  doi =		{10.4230/LIPIcs.ICDT.2020.21},
  annote =	{Keywords: Join algorithms, Compact data structures, Quadtrees, AGM bound}
}
Document
DOI: 10.4230/OASIcs.SLATE.2019.20
Identifying Causal Relations in Legal Documents with Dependency Syntactic Analysis

Authors: Pablo Gamallo, Patricia Martín-Rodilla, and Beatriz Calderón

Published in: OASIcs, Volume 74, 8th Symposium on Languages, Applications and Technologies (SLATE 2019)

Abstract
This article describes a method for enriching a dependency-based parser with causal connectors. Our specific objective is to identify causal relationships between elementary discourse units in Spanish legal texts. For this purpose, the approach we follow is to search for specific discourse connectives which are taken as causal dependencies relating an effect event (head) with a verbal or nominal cause (dependent). As a result, we turn a specific syntactic parser into a discourse parser aimed at recognizing causal structures.
Cite as

Pablo Gamallo, Patricia Martín-Rodilla, and Beatriz Calderón. Identifying Causal Relations in Legal Documents with Dependency Syntactic Analysis. In 8th Symposium on Languages, Applications and Technologies (SLATE 2019). Open Access Series in Informatics (OASIcs), Volume 74, pp. 20:1-20:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gamallo_et_al:OASIcs.SLATE.2019.20,
  author =	{Gamallo, Pablo and Mart{\'\i}n-Rodilla, Patricia and Calder\'{o}n, Beatriz},
  title =	{{Identifying Causal Relations in Legal Documents with Dependency Syntactic Analysis}},
  booktitle =	{8th Symposium on Languages, Applications and Technologies (SLATE 2019)},
  pages =	{20:1--20:6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-114-6},
  ISSN =	{2190-6807},
  year =	{2019},
  volume =	{74},
  editor =	{Rodrigues, Ricardo and Janou\v{s}ek, Jan and Ferreira, Lu{\'\i}s and Coheur, Lu{\'\i}sa and Batista, Fernando and Gon\c{c}alo Oliveira, Hugo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2019.20},
  URN =		{urn:nbn:de:0030-drops-108870},
  doi =		{10.4230/OASIcs.SLATE.2019.20},
  annote =	{Keywords: Dependency Analysis, Discourse Analysis, Causal Markers, Legal Documents}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.103
Monadic Decomposability of Regular Relations (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
Monadic decomposibility - the ability to determine whether a formula in a given logical theory can be decomposed into a boolean combination of monadic formulas - is a powerful tool for devising a decision procedure for a given logical theory. In this paper, we revisit a classical decision problem in automata theory: given a regular (a.k.a. synchronized rational) relation, determine whether it is recognizable, i.e., it has a monadic decomposition (that is, a representation as a boolean combination of cartesian products of regular languages). Regular relations are expressive formalisms which, using an appropriate string encoding, can capture relations definable in Presburger Arithmetic. In fact, their expressive power coincide with relations definable in a universal automatic structure; equivalently, those definable by finite set interpretations in WS1S (Weak Second Order Theory of One Successor). Determining whether a regular relation admits a recognizable relation was known to be decidable (and in exponential time for binary relations), but its precise complexity still hitherto remains open. Our main contribution is to fully settle the complexity of this decision problem by developing new techniques employing infinite Ramsey theory. The complexity for DFA (resp. NFA) representations of regular relations is shown to be NLOGSPACE-complete (resp. PSPACE-complete).
Cite as

Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen. Monadic Decomposability of Regular Relations (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 103:1-103:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{barcelo_et_al:LIPIcs.ICALP.2019.103,
  author =	{Barcel\'{o}, Pablo and Hong, Chih-Duo and Le, Xuan-Bach and Lin, Anthony W. and Niskanen, Reino},
  title =	{{Monadic Decomposability of Regular Relations}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{103:1--103:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.103},
  URN =		{urn:nbn:de:0030-drops-106790},
  doi =		{10.4230/LIPIcs.ICALP.2019.103},
  annote =	{Keywords: Transducers, Automata, Synchronized Rational Relations, Ramsey Theory, Variable Independence, Automatic Structures}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.104
Boundedness of Conjunctive Regular Path Queries (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Pablo Barceló, Diego Figueira, and Miguel Romero

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We study the boundedness problem for unions of conjunctive regular path queries with inverses (UC2RPQs). This is the problem of, given a UC2RPQ, checking whether it is equivalent to a union of conjunctive queries (UCQ). We show the problem to be ExpSpace-complete, thus coinciding with the complexity of containment for UC2RPQs. As a corollary, when a UC2RPQ is bounded, it is equivalent to a UCQ of at most triple-exponential size, and in fact we show that this bound is optimal. We also study better behaved classes of UC2RPQs, namely acyclic UC2RPQs of bounded thickness, and strongly connected UCRPQs, whose boundedness problem is, respectively, PSpace-complete and Pi_2^P-complete. Most upper bounds exploit results on limitedness for distance automata, in particular extending the model with alternation and two-wayness, which may be of independent interest.
Cite as

Pablo Barceló, Diego Figueira, and Miguel Romero. Boundedness of Conjunctive Regular Path Queries (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 104:1-104:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{barcelo_et_al:LIPIcs.ICALP.2019.104,
  author =	{Barcel\'{o}, Pablo and Figueira, Diego and Romero, Miguel},
  title =	{{Boundedness of Conjunctive Regular Path Queries}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{104:1--104:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.104},
  URN =		{urn:nbn:de:0030-drops-106803},
  doi =		{10.4230/LIPIcs.ICALP.2019.104},
  annote =	{Keywords: regular path queries, boundedness, limitedness, distance automata}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.1
Everest: Towards a Verified, Drop-in Replacement of HTTPS

Authors: Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract
The HTTPS ecosystem is the foundation on which Internet security is built. At the heart of this ecosystem is the Transport Layer Security (TLS) protocol, which in turn uses the X.509 public-key infrastructure and numerous cryptographic constructions and algorithms. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks and emergency patches many times a year. We describe our ongoing efforts in Everest (The Everest VERified End-to-end Secure Transport) a project that aims to build and deploy a verified version of TLS and other components of HTTPS, replacing the current infrastructure with proven, secure software. Aiming both at full verification and usability, we conduct high-level code-based, game-playing proofs of security on cryptographic implementations that yield efficient, deployable code, at the level of C and assembly. Concretely, we use F*, a dependently typed language for programming, meta-programming, and proving at a high level, while relying on low-level DSLs embedded within F* for programming low-level components when necessary for performance and, sometimes, side-channel resistance. To compose the pieces, we compile all our code to source-like C and assembly, suitable for deployment and integration with existing code bases, as well as audit by independent security experts. Our main results so far include (1) the design of Low*, a subset of F* designed for C-like imperative programming but with high-level verification support, and KreMLin, a compiler that extracts Low* programs to C; (2) an implementation of the TLS-1.3 record layer in Low*, together with a proof of its concrete cryptographic security; (3) Vale, a new DSL for verified assembly language, and several optimized cryptographic primitives proven functionally correct and side-channel resistant. In an early deployment, all our verified software is integrated and deployed within libcurl, a widely used library of networking protocols.
Cite as

Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a Verified, Drop-in Replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 1:1-1:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bhargavan_et_al:LIPIcs.SNAPL.2017.1,
  author =	{Bhargavan, Karthikeyan and Bond, Barry and Delignat-Lavaud, Antoine and Fournet, C\'{e}dric and Hawblitzel, Chris and Hritcu, Catalin and Ishtiaq, Samin and Kohlweiss, Markulf and Leino, Rustan and Lorch, Jay and Maillard, Kenji and Pan, Jianyang and Parno, Bryan and Protzenko, Jonathan and Ramananandro, Tahina and Rane, Ashay and Rastogi, Aseem and Swamy, Nikhil and Thompson, Laure and Wang, Peng and Zanella-B\'{e}guelin, Santiago and Zinzindohou\'{e}, Jean-Karim},
  title =	{{Everest: Towards a Verified, Drop-in Replacement of HTTPS}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{1:1--1:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.1},
  URN =		{urn:nbn:de:0030-drops-71196},
  doi =		{10.4230/LIPIcs.SNAPL.2017.1},
  annote =	{Keywords: Security, Cryptography, Verification, TLS}
}
  • Refine by Author
  • 2 Barceló, Pablo
  • 2 Gamallo, Pablo
  • 1 Bhargavan, Karthikeyan
  • 1 Bond, Barry
  • 1 Calderón, Beatriz
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Data structures and algorithms for data management
  • 1 Computing methodologies → Information extraction
  • 1 Computing methodologies → Language resources
  • 1 Computing methodologies → Natural language processing
  • 1 Computing methodologies → Network science
  • Show More...

  • Refine by Keyword
  • 1 AGM bound
  • 1 Automata
  • 1 Automatic Structures
  • 1 Causal Markers
  • 1 Compact data structures
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 3 2019
  • 1 2017
  • 1 2020
  • 1 2021
  • 1 2022
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact