Search Results

Documents authored by Tamir, Orr

Document
DOI: 10.4230/LIPIcs.ICDT.2017.16
On the Automated Verification of Web Applications with Embedded SQL

Authors: Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, and Florian Zuleger

Published in: LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

Abstract
A large number of web applications is based on a relational database together with a program, typically a script, that enables the user to interact with the database through embedded SQL queries and commands. In this paper, we introduce a method for formal automated verification of such systems which connects database theory to mainstream program analysis. We identify a fragment of SQL which captures the behavior of the queries in our case studies, is algorithmically decidable, and facilitates the construction of weakest preconditions. Thus, we can integrate the analysis of SQL queries into a program analysis tool chain. To this end, we implement a new decision procedure for the SQL fragment that we introduce. We demonstrate practical applicability of our results with three case studies, a web administrator, a simple firewall, and a conference management system.
Cite as

Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, and Florian Zuleger. On the Automated Verification of Web Applications with Embedded SQL. In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{itzhaky_et_al:LIPIcs.ICDT.2017.16,
  author =	{Itzhaky, Shachar and Kotek, Tomer and Rinetzky, Noam and Sagiv, Mooly and Tamir, Orr and Veith, Helmut and Zuleger, Florian},
  title =	{{On the Automated Verification of Web Applications with Embedded SQL}},
  booktitle =	{20th International Conference on Database Theory (ICDT 2017)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-024-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{68},
  editor =	{Benedikt, Michael and Orsi, Giorgio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017.16},
  URN =		{urn:nbn:de:0030-drops-70509},
  doi =		{10.4230/LIPIcs.ICDT.2017.16},
  annote =	{Keywords: SQL; scripting language; web services; program verification; two-variable fragment of first order logic; decidability; reasoning}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2015.15
A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms

Authors: Orr Tamir, Adam Morrison, and Noam Rinetzky

Published in: LIPIcs, Volume 46, 19th International Conference on Principles of Distributed Systems (OPODIS 2015)

Abstract
Existing concurrent priority queues do not allow to update the priority of an element after its insertion. As a result, algorithms that need this functionality, such as Dijkstra's single source shortest path algorithm, resort to cumbersome and inefficient workarounds. We report on a heap-based concurrent priority queue which allows to change the priority of an element after its insertion. We show that the enriched interface allows to express Dijkstra's algorithm in a more natural way, and that its implementation, using our concurrent priority queue, outperform existing algorithms.
Cite as

Orr Tamir, Adam Morrison, and Noam Rinetzky. A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 46, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{tamir_et_al:LIPIcs.OPODIS.2015.15,
  author =	{Tamir, Orr and Morrison, Adam and Rinetzky, Noam},
  title =	{{A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms}},
  booktitle =	{19th International Conference on Principles of Distributed Systems (OPODIS 2015)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-98-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{46},
  editor =	{Anceaume, Emmanuelle and Cachin, Christian and Potop-Butucaru, Maria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2015.15},
  URN =		{urn:nbn:de:0030-drops-66068},
  doi =		{10.4230/LIPIcs.OPODIS.2015.15},
  annote =	{Keywords: priority queues, concurrent data structures, Dijkstra's single-source shortest path algorithm}
}
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