Search Results

Documents authored by Veith, Helmut

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.CSL.2016.13
Monadic Second Order Finite Satisfiability and Unbounded Tree-Width

Authors: Tomer Kotek, Helmut Veith, and Florian Zuleger

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese. We prove that the following problem is decidable: Input: (i) A monadic second order logic sentence alpha, and (ii) a sentence beta in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of alpha and beta may intersect. Output: Is there a finite structure which satisfies alpha and beta such that the restriction of the structure to the vocabulary of alpha has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic MS^{exists card} extending monadic second order logic with linear cardinality constraints of the form |X_{1}|+...+|X_{r}| < |Y_{1}|+...+|Y_{s}| on the variables X_i, Y_j of the outer-most quantifier block. We prove the decidability of a similar extension of WS1S.
Cite as

Tomer Kotek, Helmut Veith, and Florian Zuleger. Monadic Second Order Finite Satisfiability and Unbounded Tree-Width. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kotek_et_al:LIPIcs.CSL.2016.13,
  author =	{Kotek, Tomer and Veith, Helmut and Zuleger, Florian},
  title =	{{Monadic Second Order Finite Satisfiability and Unbounded Tree-Width}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{13:1--13:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.13},
  URN =		{urn:nbn:de:0030-drops-65537},
  doi =		{10.4230/LIPIcs.CSL.2016.13},
  annote =	{Keywords: Monadic Second Order Logic MSO, Two variable Fragment with Counting C2, Finite decidability, Unbounded Tree-width, WS1S with Cardinality Constraints}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.6
Local Linearizability for Concurrent Container-Type Data Structures

Authors: Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations.
Cite as

Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. Local Linearizability for Concurrent Container-Type Data Structures. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{haas_et_al:LIPIcs.CONCUR.2016.6,
  author =	{Haas, Andreas and Henzinger, Thomas A. and Holzer, Andreas and Kirsch, Christoph M. and Lippautz, Michael and Payer, Hannes and Sezgin, Ali and Sokolova, Ana and Veith, Helmut},
  title =	{{Local Linearizability for Concurrent Container-Type Data Structures}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.6},
  URN =		{urn:nbn:de:0030-drops-61809},
  doi =		{10.4230/LIPIcs.CONCUR.2016.6},
  annote =	{Keywords: (concurrent) data structures, relaxed semantics, linearizability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.30
Parameterized Systems in BIP: Design and Model Checking

Authors: Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to systems parameterized in the number of components. We show that FOIL captures classical parameterized architectures such as token-passing rings, cliques of identical components communicating with rendezvous or broadcast, and client-server systems. Although the BIP framework includes efficient verification tools for statically-defined systems, none are available for parameterized systems with an unbounded number of components. The parameterized model checking literature contains a wealth of techniques for systems of classical architectures. However, application of these results requires a deep understanding of parameterized model checking techniques and their underlying mathematical models. To overcome these difficulties, we introduce a framework that automatically identifies parameterized model checking techniques applicable to a BIP design. To our knowledge, it is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.
Cite as

Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis. Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{konnov_et_al:LIPIcs.CONCUR.2016.30,
  author =	{Konnov, Igor and Kotek, Tomer and Wang, Qiang and Veith, Helmut and Bliudze, Simon and Joseph Sifakis},
  title =	{{Parameterized Systems in BIP: Design and Model Checking}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.30},
  URN =		{urn:nbn:de:0030-drops-61670},
  doi =		{10.4230/LIPIcs.CONCUR.2016.30},
  annote =	{Keywords: Rigorous system design, BIP, verification, parameterized model checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.377
On the Structure and Complexity of Rational Sets of Regular Languages

Authors: Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
In the recently designed and implemented test specification language FQL, relevant test goals are specified as regular expressions over program locations. To transition from single test goals to test suites, FQL describes suites as regular expressions over finite alphabets where each symbol corresponds to a regular expression over program locations. Hence, each word in a test suite expression yields a test goal specification. Such test suite specifications are in fact rational sets of regular languages (RSRLs). We show closure properties of general and finite RSRLs under common set theoretic operations. We also prove complexity results for checking equivalence and inclusion of star-free RSRLs and for checking whether a regular language is a member of a general or star-free RSRL. As the star-free (and thus finite) case underlies FQL specifications, the closure and complexity results provide a systematic foundation for FQL test specifications.
Cite as

Andreas Holzer, Christian Schallhart, Michael Tautschnig, and Helmut Veith. On the Structure and Complexity of Rational Sets of Regular Languages. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 377-388, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{holzer_et_al:LIPIcs.FSTTCS.2013.377,
  author =	{Holzer, Andreas and Schallhart, Christian and Tautschnig, Michael and Veith, Helmut},
  title =	{{On the Structure and Complexity of Rational Sets of Regular Languages}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{377--388},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.377},
  URN =		{urn:nbn:de:0030-drops-43871},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.377},
  annote =	{Keywords: Rational Sets, Regular Languages, Test Specification in FQL, Closure Properties, Decision Problems}
}
Document
DOI: 10.4230/DagRep.1.7.23
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272)

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Reports, Volume 1, Issue 7 (2011)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 11272 "Decision Procedures in Soft, Hard and Bio-ware (Follow Up)". It was held as a follow-on for a seminar 10161, of the same title, that took place in late April 2010 during the initial eruption of Eyjafjallajökull. In spite of the travel disruptions caused by the eruption of the volcano, the original seminar received a respectable turnout by European, mainly German and Italian participants. Unfortunately, the eruption hindered participation from overseas or even more distant parts of Europe. This caused the seminar to cover only part of the original objective. The follow-on seminar focused on the remaining objectives, in particular to bio-ware and constraint solving methods.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). In Dagstuhl Reports, Volume 1, Issue 7, pp. 23-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.1.7.23,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272)}},
  pages =	{23--35},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{7},
  editor =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.7.23},
  URN =		{urn:nbn:de:0030-drops-32775},
  doi =		{10.4230/DagRep.1.7.23},
  annote =	{Keywords: Hardware and Software Verification, Bio-analysis, Satisfiability Modulo Theories, Dynamic Symbolic Execution, Interpolants}
}
Document
DOI: 10.4230/DagSemProc.10161.1
10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)

Abstract
From April 19th, 2010 to April 23rd, 2010, the Dagstuhl Seminar 10161 "Decision Procedures in Soft, Hard and Bio-ware" was held in Schloss Dagstuhl Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as links to slides and links to papers behind the presentations and papers produced as a result of the seminar are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. 10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bjorner_et_al:DagSemProc.10161.1,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware}},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.1},
  URN =		{urn:nbn:de:0030-drops-27421},
  doi =		{10.4230/DagSemProc.10161.1},
  annote =	{Keywords: Decision Procedures, Satisfiability Modulo Theories, Software Verification, Dynamic Symbolic Execution, Interpolants, Hardware Verification, Bio-analysis}
}
Document
DOI: 10.4230/DagSemProc.10161.2
10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)

Abstract
The main goal of the seminar Decision Procedures in Soft, Hard and Bio-ware was to bring together renowned as well as young aspiring researchers from two groups. The first group formed by researchers who develop both theory and efficient implementations of decision procedures. The second group comprising of researchers from application areas such as program analysis and testing, crypto-analysis, hardware verification, industrial planning and scheduling, and bio-informatics, who have worked with, and contributed to, high quality decision procedures. The purpose of the seminar was to heighten awareness between tool and theory developers for decision procedures with the array of applications found in software, hardware and biological systems analysis.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. 10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bjorner_et_al:DagSemProc.10161.2,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware }},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.2},
  URN =		{urn:nbn:de:0030-drops-27369},
  doi =		{10.4230/DagSemProc.10161.2},
  annote =	{Keywords: Decision procedures, software, hardware, bioware}
}
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