11 Search Results for "Smaragdakis, Yannis"

Document
DOI: 10.4230/LIPIcs.AFT.2024.7
DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance

Authors: Rundong Gan, Liyi Zhou, Le Wang, Kaihua Qin, and Xiaodong Lin

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
Decentralized Finance (DeFi) has witnessed a monumental surge, reaching 53.039 billion USD in total value locked. As this sector continues to expand, ensuring the reliability of DeFi smart contracts becomes increasingly crucial. While some users are adept at reading code or the compiled bytecode to understand smart contracts, many rely on documentation. Therefore, discrepancies between the documentation and the deployed code can pose significant risks, whether these discrepancies are due to errors or intentional fraud. To tackle these challenges, we developed DeFiAligner, an end-to-end system to identify inconsistencies between documentation and smart contracts. DeFiAligner incorporates a symbolic execution tool, SEVM, which explores execution paths of on-chain binary code, recording memory and stack states. It automatically generates symbolic expressions for token balance changes and branch conditions, which, along with related project documents, are processed by LLMs. Using structured prompts, the LLMs evaluate the alignment between the symbolic expressions and the documentation. Our tests across three distinct scenarios demonstrate DeFiAligner’s capability to automate inconsistency detection in DeFi, achieving recall rates of 92% and 90% on two public datasets respectively.
Cite as

Rundong Gan, Liyi Zhou, Le Wang, Kaihua Qin, and Xiaodong Lin. DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gan_et_al:LIPIcs.AFT.2024.7,
  author =	{Gan, Rundong and Zhou, Liyi and Wang, Le and Qin, Kaihua and Lin, Xiaodong},
  title =	{{DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{7:1--7:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.7},
  URN =		{urn:nbn:de:0030-drops-209431},
  doi =		{10.4230/LIPIcs.AFT.2024.7},
  annote =	{Keywords: Decentralized Finance Security, Large Language Models, Project Review, Symbolic Analysis, Smart Contracts}
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.2
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda

Authors: Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.
Cite as

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2,
  author =	{Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
  title =	{{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{2:1--2:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.2},
  URN =		{urn:nbn:de:0030-drops-198673},
  doi =		{10.4230/OASIcs.FMBC.2024.2},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.15
Static Analysis of Shape in TensorFlow Programs

Authors: Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Machine learning has been widely adopted in diverse science and engineering domains, aided by reusable libraries and quick development patterns. The TensorFlow library is probably the best-known representative of this trend and most users employ the Python API to its powerful back-end. TensorFlow programs are susceptible to several systematic errors, especially in the dynamic typing setting of Python. We present Pythia, a static analysis that tracks the shapes of tensors across Python library calls and warns of several possible mismatches. The key technical aspects are a close modeling of library semantics with respect to tensor shape, and an identification of violations and error-prone patterns. Pythia is powerful enough to statically detect (with 84.62% precision) 11 of the 14 shape-related TensorFlow bugs in the recent Zhang et al. empirical study - an independent slice of real-world bugs.
Cite as

Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis. Static Analysis of Shape in TensorFlow Programs. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 15:1-15:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lagouvardos_et_al:LIPIcs.ECOOP.2020.15,
  author =	{Lagouvardos, Sifis and Dolby, Julian and Grech, Neville and Antoniadis, Anastasios and Smaragdakis, Yannis},
  title =	{{Static Analysis of Shape in TensorFlow Programs}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{15:1--15:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.15},
  URN =		{urn:nbn:de:0030-drops-131726},
  doi =		{10.4230/LIPIcs.ECOOP.2020.15},
  annote =	{Keywords: Python, TensorFlow, static analysis, Doop, Wala}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.6
Static Analysis of Shape in TensorFlow Programs (Artifact)

Authors: Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
These instructions are intended for using the artifact for our ECOOP'20 paper entitled "Static Analysis of Shape in TensorFlow Programs". They can be used to run Pythia - the tool implementing the paper’s analysis - on the paper’s evaluation set demonstrating bug detection in the most precise configuration of our analysis as well as the precision of the analysis under different configurations.
Cite as

Sifis Lagouvardos, Julian Dolby, Neville Grech, Anastasios Antoniadis, and Yannis Smaragdakis. Static Analysis of Shape in TensorFlow Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 6:1-6:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{lagouvardos_et_al:DARTS.6.2.6,
  author =	{Lagouvardos, Sifis and Dolby, Julian and Grech, Neville and Antoniadis, Anastasios and Smaragdakis, Yannis},
  title =	{{Static Analysis of Shape in TensorFlow Programs (Artifact)}},
  pages =	{6:1--6:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Lagouvardos, Sifis and Dolby, Julian and Grech, Neville and Antoniadis, Anastasios and Smaragdakis, Yannis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.6},
  URN =		{urn:nbn:de:0030-drops-132035},
  doi =		{10.4230/DARTS.6.2.6},
  annote =	{Keywords: Python, TensorFlow, static analysis, Doop, Wala}
}
Document
Artifact
DOI: 10.4230/DARTS.5.2.6
Deep Static Modeling of invokedynamic (Artifact)

Authors: George Fourtounis and Yannis Smaragdakis

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, introduced in Java 8, are a very popular feature, which is, however, resistant to static analysis, since it mixes invokedynamic with dynamic code generation. These techniques invalidate static analysis assumptions: programmable linking breaks reasoning about method resolution while dynamically generated code is, by definition, not available statically. In this paper, we show that a static analysis can predictively model uses of invokedynamic while also cooperating with extra rules to handle the runtime code generation of lambdas. Our approach plugs into an existing static analysis and helps eliminate all unsoundness in the handling of lambdas (including associated features such as method references) and generic invokedynamic uses. We evaluate our technique on a benchmark suite of our own and on third-party benchmarks, uncovering all code previously unreachable due to unsoundness, highly efficiently.
Cite as

George Fourtounis and Yannis Smaragdakis. Deep Static Modeling of invokedynamic (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 6:1-6:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{fourtounis_et_al:DARTS.5.2.6,
  author =	{Fourtounis, George and Smaragdakis, Yannis},
  title =	{{Deep Static Modeling of invokedynamic}},
  pages =	{6:1--6:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Fourtounis, George and Smaragdakis, Yannis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.6},
  URN =		{urn:nbn:de:0030-drops-107835},
  doi =		{10.4230/DARTS.5.2.6},
  annote =	{Keywords: invokedynamic, lambdas, static analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2019.15
Deep Static Modeling of invokedynamic

Authors: George Fourtounis and Yannis Smaragdakis

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, introduced in Java 8, are a very popular feature, which is, however, resistant to static analysis, since it mixes invokedynamic with dynamic code generation. These techniques invalidate static analysis assumptions: programmable linking breaks reasoning about method resolution while dynamically generated code is, by definition, not available statically. In this paper, we show that a static analysis can predictively model uses of invokedynamic while also cooperating with extra rules to handle the runtime code generation of lambdas. Our approach plugs into an existing static analysis and helps eliminate all unsoundness in the handling of lambdas (including associated features such as method references) and generic invokedynamic uses. We evaluate our technique on a benchmark suite of our own and on third-party benchmarks, uncovering all code previously unreachable due to unsoundness, highly efficiently.
Cite as

George Fourtounis and Yannis Smaragdakis. Deep Static Modeling of invokedynamic. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{fourtounis_et_al:LIPIcs.ECOOP.2019.15,
  author =	{Fourtounis, George and Smaragdakis, Yannis},
  title =	{{Deep Static Modeling of invokedynamic}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.15},
  URN =		{urn:nbn:de:0030-drops-108076},
  doi =		{10.4230/LIPIcs.ECOOP.2019.15},
  annote =	{Keywords: static analysis, invokedynamic}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.23
Defensive Points-To Analysis: Effective Soundness via Laziness

Authors: Yannis Smaragdakis and George Kastrinis

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
We present a defensive may-point-to analysis approach, which offers soundness even in the presence of arbitrary opaque code: all non-empty points-to sets computed are guaranteed to be over-approximations of the sets of values arising at run time. A key design tenet of the analysis is laziness: the analysis computes points-to relationships only for variables or objects that are guaranteed to never escape into opaque code. This means that the analysis misses some valid inferences, yet it also never wastes work to compute sets of values that are not "complete", i.e., that may be missing elements due to opaque code. Laziness enables great efficiency, allowing a highly precise points-to analysis (such as a 5-call-site-sensitive, flow-sensitive analysis). Despite its conservative nature, our analysis yields sound, actionable results for a large subset of the program code, achieving (under worst-case assumptions) 34-74% of the program coverage of an unsound state-of-the-art analysis for real-world programs.
Cite as

Yannis Smaragdakis and George Kastrinis. Defensive Points-To Analysis: Effective Soundness via Laziness. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 23:1-23:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{smaragdakis_et_al:LIPIcs.ECOOP.2018.23,
  author =	{Smaragdakis, Yannis and Kastrinis, George},
  title =	{{Defensive Points-To Analysis: Effective Soundness via Laziness}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{23:1--23:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.23},
  URN =		{urn:nbn:de:0030-drops-92287},
  doi =		{10.4230/LIPIcs.ECOOP.2018.23},
  annote =	{Keywords: static analysis, soundness, defensive analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.26
Efficient Reflection String Analysis via Graph Coloring

Authors: Neville Grech, George Kastrinis, and Yannis Smaragdakis

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Static analyses for reflection and other dynamic language features have recently increased in number and advanced in sophistication. Most such analyses rely on a whole-program model of the flow of strings, through the stack and heap. We show that this global modeling of strings remains a major bottleneck of static analyses and propose a compact encoding, in order to battle unnecessary complexity. In our encoding, strings are maximally merged if they can never serve to differentiate class members in reflection operations. We formulate the problem as an instance of graph coloring and propose a fast polynomial-time algorithm that exploits the unique features of the setting (esp. large cliques, leading to hundreds of colors for realistic programs). The encoding is applied to two different frameworks for string-guided Java reflection analysis from past literature and leads to significant optimization (e.g., a ~2x reduction in the number of string-flow inferences), for a whole-program points-to analysis that uses strings.
Cite as

Neville Grech, George Kastrinis, and Yannis Smaragdakis. Efficient Reflection String Analysis via Graph Coloring. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 26:1-26:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{grech_et_al:LIPIcs.ECOOP.2018.26,
  author =	{Grech, Neville and Kastrinis, George and Smaragdakis, Yannis},
  title =	{{Efficient Reflection String Analysis via Graph Coloring}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{26:1--26:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.26},
  URN =		{urn:nbn:de:0030-drops-92319},
  doi =		{10.4230/LIPIcs.ECOOP.2018.26},
  annote =	{Keywords: reflection, static analysis, graph coloring}
}
Document
DOI: 10.4230/DARTS.1.1.9
Streams à la carte: Extensible Pipelines with Object Algebras (Artifact)

Authors: Aggelos Biboudis, Nick Palladinos, George Fourtounis, and Yannis Smaragdakis

Published in: DARTS, Volume 1, Issue 1, Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
In Streams à la carte we address extensibility shortcomings in libraries for lazy-streaming queries with a new design. The architecture underlying this design borrows heavily from Oliveira and Cook's object algebra solution to the expression problem, extended with a design that exposes the push/pull character of the iteration, and an encoding of higher-kinded polymorphism. In this library we apply our design to Java and show that the addition of full extensibility is accompanied by high performance, matching or exceeding that of the original, highly-optimized Java streams library. In this artifact we present a fundamental set of sequential operators map, filter, reduce, count, take/limit and iterate. Additionally we present the behaviors that are discussed in the paper: push, pull, fused pull, logging, id (for blocking terminal operators), future (for non-blocking terminal operators).
Cite as

Aggelos Biboudis, Nick Palladinos, George Fourtounis, and Yannis Smaragdakis. Streams à la carte: Extensible Pipelines with Object Algebras (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{biboudis_et_al:DARTS.1.1.9,
  author =	{Biboudis, Aggelos and Palladinos, Nick and Fourtounis, George and Smaragdakis, Yannis},
  title =	{{Streams \`{a} la carte: Extensible Pipelines with Object Algebras (Artifact)}},
  pages =	{9:1--9:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2015},
  volume =	{1},
  number =	{1},
  editor =	{Biboudis, Aggelos and Palladinos, Nick and Fourtounis, George and Smaragdakis, Yannis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.1.1.9},
  URN =		{urn:nbn:de:0030-drops-55189},
  doi =		{10.4230/DARTS.1.1.9},
  annote =	{Keywords: object algebras, streams, extensibility, domain-specific languages, expression problem, library design}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.591
Streams a la carte: Extensible Pipelines with Object Algebras

Authors: Aggelos Biboudis, Nick Palladinos, George Fourtounis, and Yannis Smaragdakis

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
Streaming libraries have become ubiquitous in object-oriented languages, with recent offerings in Java, C#, and Scala. All such libraries, however, suffer in terms of extensibility: there is no way to change the semantics of a streaming pipeline (e.g., to fuse filter operators, to perform computations lazily, to log operations) without changes to the library code. Furthermore, in some languages it is not even possible to add new operators (e.g., a zip operator, in addition to the standard map, filter, etc.) without changing the library. We address such extensibility shortcomings with a new design for streaming libraries. The architecture underlying this design borrows heavily from Oliveira and Cook's object algebra solution to the expression problem, extended with a design that exposes the push/pull character of the iteration, and an encoding of higher-kinded polymorphism. We apply our design to Java and show that the addition of full extensibility is accompanied by high performance, matching or exceeding that of the original, highly-optimized Java streams library.
Cite as

Aggelos Biboudis, Nick Palladinos, George Fourtounis, and Yannis Smaragdakis. Streams a la carte: Extensible Pipelines with Object Algebras. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 591-613, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{biboudis_et_al:LIPIcs.ECOOP.2015.591,
  author =	{Biboudis, Aggelos and Palladinos, Nick and Fourtounis, George and Smaragdakis, Yannis},
  title =	{{Streams a la carte: Extensible Pipelines with Object Algebras}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{591--613},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.591},
  URN =		{urn:nbn:de:0030-drops-52392},
  doi =		{10.4230/LIPIcs.ECOOP.2015.591},
  annote =	{Keywords: object algebras, streams, extensibility, domain-specific languages, expression problem, library design}
}
Document
DOI: 10.4230/DagRep.3.4.91
Pointer Analysis (Dagstuhl Seminar 13162)

Authors: Ondrej Lhotak, Yannis Smaragdakis, and Manu Sridharan

Published in: Dagstuhl Reports, Volume 3, Issue 4 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13162 ``Pointer Analysis''. The seminar had 27 attendees, including both pointer analysis experts and researchers developing clients in need of better pointer analysis. The seminar came at a key point in time, with pointer analysis techniques acquiring sophistication but still being just beyond the edge of wide practical deployment. The seminar participants presented recent research results, and identified key open problems and future directions for the field. This report presents abstracts of the participants' talks and summaries of the breakout sessions from the seminar.
Cite as

Ondrej Lhotak, Yannis Smaragdakis, and Manu Sridharan. Pointer Analysis (Dagstuhl Seminar 13162). In Dagstuhl Reports, Volume 3, Issue 4, pp. 91-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{lhotak_et_al:DagRep.3.4.91,
  author =	{Lhotak, Ondrej and Smaragdakis, Yannis and Sridharan, Manu},
  title =	{{Pointer Analysis (Dagstuhl Seminar 13162)}},
  pages =	{91--113},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{4},
  editor =	{Lhotak, Ondrej and Smaragdakis, Yannis and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.4.91},
  URN =		{urn:nbn:de:0030-drops-41698},
  doi =		{10.4230/DagRep.3.4.91},
  annote =	{Keywords: pointer analysis, points-to analysis, alias analysis, static analysis, programming languages}
}
  • Refine by Author
  • 9 Smaragdakis, Yannis
  • 4 Fourtounis, George
  • 3 Grech, Neville
  • 2 Antoniadis, Anastasios
  • 2 Biboudis, Aggelos
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 7 static analysis
  • 2 Doop
  • 2 Python
  • 2 TensorFlow
  • 2 Wala
  • Show More...

  • Refine by Type
  • 11 document

  • Refine by Publication Year
  • 2 2015
  • 2 2018
  • 2 2019
  • 2 2020
  • 2 2024
  • 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 About DROPS Imprint Privacy Contact