160 Search Results for "Sangiorgi, Davide"


Volume

LIPIcs, Volume 55

43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

ICALP 2016, July 11-15, 2016, Rome, Italy

Editors: Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi

Document
Invited Talk
Enhanced Induction in Behavioural Relations (Invited Talk)

Authors: Davide Sangiorgi

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)


Abstract
We outline an attempt at transporting the well-known theory of enhancements for the coinduction proof method, widely used on behavioural relations such as bisimilarity, onto the realms of inductive behaviour relations, i.e., relations defined from inductive observables, and discuss relevant literature.

Cite as

Davide Sangiorgi. Enhanced Induction in Behavioural Relations (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{sangiorgi:LIPIcs.CSL.2023.4,
  author =	{Sangiorgi, Davide},
  title =	{{Enhanced Induction in Behavioural Relations}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{4:1--4:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.4},
  URN =		{urn:nbn:de:0030-drops-174658},
  doi =		{10.4230/LIPIcs.CSL.2023.4},
  annote =	{Keywords: coinduction, induction, semantics, behavioural relations}
}
Document
Invited Paper
CONCUR Test-Of-Time Award 2022 (Invited Paper)

Authors: Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four papers that received the Award in 2022.

Cite as

Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi. CONCUR Test-Of-Time Award 2022 (Invited Paper). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1:1-1:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{castellani_et_al:LIPIcs.CONCUR.2022.1,
  author =	{Castellani, Ilaria and Gastin, Paul and Kupferman, Orna and Randour, Mickael and Sangiorgi, Davide},
  title =	{{CONCUR Test-Of-Time Award 2022}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{1:1--1:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.1},
  URN =		{urn:nbn:de:0030-drops-170644},
  doi =		{10.4230/LIPIcs.CONCUR.2022.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques

Authors: Enguerrand Prebet

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
We present a fully abstract encoding of λ^{ref}, the call-by-value λ-calculus with references, in the π-calculus. By contrast with previous full abstraction results for sequential languages in the π-calculus, the characterisation of contextual equivalence in the source language uses a labelled bisimilarity. To define the latter equivalence, we refine existing notions of typed bisimulation in the π-calculus, and introduce in particular a specific component to handle divergences. We obtain a proof technique that allows us to prove equivalences between λ^{ref} programs via the encoding. The resulting proofs correspond closely to normal form bisimulations in the λ-calculus, making proofs in the π-calculus expressible as if reasoning in λ^{ref}. We study how standard and new up-to techniques can be used to reason about diverging terms and simplify proofs of equivalence using the bisimulation we introduce. This shows how the π-calculus theory can be used to prove interesting equivalences between λ^{ref} programs, using algebraic reasoning and up-to techniques.

Cite as

Enguerrand Prebet. Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 130:1-130:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{prebet:LIPIcs.ICALP.2022.130,
  author =	{Prebet, Enguerrand},
  title =	{{Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{130:1--130:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.130},
  URN =		{urn:nbn:de:0030-drops-164715},
  doi =		{10.4230/LIPIcs.ICALP.2022.130},
  annote =	{Keywords: Call-by-value \lambda-calculus, imperative Programming, \pi-calculus, Bisimulation, Type System}
}
Document
Games, Mobile Processes, and Functions

Authors: Guilhem Jaber and Davide Sangiorgi

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)


Abstract
We establish a tight connection between two models of the λ-calculus, namely Milner’s encoding into the π-calculus (precisely, the Internal π-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by π and OGS. We do so for various LTSs: the standard LTS for π and a new "concurrent" LTS for OGS; an "output-prioritised" LTS for π and the standard alternating LTS for OGS. We then show that the equivalences induced on λ-terms by all these LTSs (for π and OGS) coincide. These connections allow us to transfer results and techniques between π and OGS. In particular we import up-to techniques from π onto OGS and we derive congruence and compositionality results for OGS from those of π. The study is illustrated for call-by-value; similar results hold for call-by-name.

Cite as

Guilhem Jaber and Davide Sangiorgi. Games, Mobile Processes, and Functions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{jaber_et_al:LIPIcs.CSL.2022.25,
  author =	{Jaber, Guilhem and Sangiorgi, Davide},
  title =	{{Games, Mobile Processes, and Functions}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.25},
  URN =		{urn:nbn:de:0030-drops-157450},
  doi =		{10.4230/LIPIcs.CSL.2022.25},
  annote =	{Keywords: \lambda-calculus, \pi-calculus, game semantics}
}
Document
The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service

Authors: Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)


Abstract
Serverless computing is a paradigm for programming cloud applications in terms of stateless functions, executed and scaled in proportion to inbound requests. Here, we revisit SKC, a calculus capturing the essential features of serverless programming. By exploring the design space of the language, we refined the integration between the fundamental features of the two calculi that inspire SKC: the λ- and the π-calculus. That investigation led us to a revised syntax and semantics, which support an increase in the expressiveness of the language. In particular, now function names are first-class citizens and can be passed around. To illustrate the new features, we present step-by-step examples and two non-trivial use cases from artificial intelligence, which model, respectively, a perceptron and an image tagging system into compositions of serverless functions. We also illustrate how SKC supports reasoning on serverless implementations, i.e., the underlying network of communicating, concurrent, and mobile processes which execute serverless functions in the cloud. To that aim, we show an encoding from SKC to the asynchronous π-calculus and prove it correct in terms of an operational correspondence. Dedicated to Maurizio Gabbrielli, on his 60th birthday (... rob da mët ! )

Cite as

Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro. The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:OASIcs.Gabbrielli.5,
  author =	{Giallorenzo, Saverio and Lanese, Ivan and Montesi, Fabrizio and Sangiorgi, Davide and Zingaro, Stefano Pio},
  title =	{{The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{5:1--5:21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.5},
  URN =		{urn:nbn:de:0030-drops-132271},
  doi =		{10.4230/OASIcs.Gabbrielli.5},
  annote =	{Keywords: Serverless computing, Process calculi, Pi-calculus}
}
Document
On the Representation of References in the Pi-Calculus

Authors: Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been fully investigated. In this paper we address this issue. We focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We first define π^ref, an extension of Aπ with references and operators to manipulate them, and illustrate examples of the subtleties of behavioural equivalence in π^ref. We then consider a translation of π^ref into Aπ. References of π^ref are mapped onto names of Aπ belonging to a dedicated "reference" type. We show how the presence of reference names affects the definition of barbed congruence. We establish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the two calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another, more efficient and involving an inductive "game" on reference names, we derive soundness, leaving completeness open. Finally, we discuss examples of uses of the bisimilarities.

Cite as

Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On the Representation of References in the Pi-Calculus. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2020.34,
  author =	{Hirschkoff, Daniel and Prebet, Enguerrand and Sangiorgi, Davide},
  title =	{{On the Representation of References in the Pi-Calculus}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{34:1--34:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.34},
  URN =		{urn:nbn:de:0030-drops-128466},
  doi =		{10.4230/LIPIcs.CONCUR.2020.34},
  annote =	{Keywords: Process calculus, Bisimulation, Asynchrony, Imperative programming}
}
Document
Divergence and Unique Solution of Equations

Authors: Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)


Abstract
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the ‘up-to techniques’). Finally, we study the theorems in name-passing calculi such as the asynchronous pi-calculus, and revisit the completeness proof of Milner’s encoding of the lambda-calculus into the pi-calculus for Lévy-Longo Trees.

Cite as

Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and Unique Solution of Equations. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{durier_et_al:LIPIcs.CONCUR.2017.11,
  author =	{Durier, Adrien and Hirschkoff, Daniel and Sangiorgi, Davide},
  title =	{{Divergence and Unique Solution of Equations}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.11},
  URN =		{urn:nbn:de:0030-drops-77849},
  doi =		{10.4230/LIPIcs.CONCUR.2017.11},
  annote =	{Keywords: Bisimilarity, unique solution of equations, termination, process calculi}
}
Document
Complete Volume
LIPIcs, Volume 55, ICALP'16, Complete Volume

Authors: Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
LIPIcs, Volume 55, ICALP'16, Complete Volume

Cite as

43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@Proceedings{chatzigiannakis_et_al:LIPIcs.ICALP.2016,
  title =	{{LIPIcs, Volume 55, ICALP'16, Complete Volume}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016},
  URN =		{urn:nbn:de:0030-drops-65844},
  doi =		{10.4230/LIPIcs.ICALP.2016},
  annote =	{Keywords: Theory of Computation}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Organization, List of Authors

Authors: Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
Front Matter, Table of Contents, Preface, Organization, List of Authors

Cite as

43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 0:i-0:xliv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{chatzigiannakis_et_al:LIPIcs.ICALP.2016.0,
  author =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  title =	{{Front Matter, Table of Contents, Preface, Organization, List of Authors}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{0:i--0:xliv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.0},
  URN =		{urn:nbn:de:0030-drops-61917},
  doi =		{10.4230/LIPIcs.ICALP.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Organization, List of Authors}
}
Document
Invited Talk
Compute Choice (Invited Talk)

Authors: Devavrat Shah

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
In this talk, we shall discuss the question of learning distribution over permutations of n choices based on partial observations. This is central to capturing the so called "choice" in a variety of contexts: understanding preferences of consumers over a collection of products based on purchasing and browsing data in the setting of retail and e-commerce, learning public opinion amongst a collection of socio-economic issues based on sparse polling data, and deciding a ranking of teams or players based on outcomes of games. The talk will primarily discuss the relationship between the ability to learn, nature of partial information and number of available observations. Connections to the classical theory of social choice and behavioral psychology, as well as modern literature in Statistics, learning theory and operations research will be discussed.

Cite as

Devavrat Shah. Compute Choice (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{shah:LIPIcs.ICALP.2016.1,
  author =	{Shah, Devavrat},
  title =	{{Compute Choice}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.1},
  URN =		{urn:nbn:de:0030-drops-63374},
  doi =		{10.4230/LIPIcs.ICALP.2016.1},
  annote =	{Keywords: Decision Systems, Learning Distributions, Partial observations}
}
Document
Invited Talk
Formally Verifying a Compiler: What Does It Mean, Exactly? (Invited Talk)

Authors: Xavier Leroy

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
Compilers, and especially optimizing compilers, are complicated programs. Bugs in compilers happen, and can lead to miscompilation: the production of wrong executable code from a correct source program. Miscompilation is documented in the literature and a concern for high-assurance software, as it endangers the guarantees obtained by source-level formal verification of programs. Compiler verification is a radical solution to the miscompilation problem: by applying program proof to the compiler itself, we can obtain mathematically strong guarantees that the generated executable code is faithful to the semantics of the source program. The state of the art in this line of research is arguably the CompCert verified compiler. This talk will give an overview of this optimizing C compiler and of its formal verification, conducted with the Coq proof assistant. A formal verification is as good as the specifications it uses. In other words, verification reduces the problem of trusting a large implementation to that of ensuring that its formal specification enforce the intended correctness properties. In the case of CompCert, the correctness statement that is proved is rather complex, as it involves large operational semantics (for the C language and for the assembly languages of the target architectures) and simulations between these semantics that support both choice refinement and behavior refinement. The talk will review and discuss these elements of the specification, along with some of the accompanying proof principles.

Cite as

Xavier Leroy. Formally Verifying a Compiler: What Does It Mean, Exactly? (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{leroy:LIPIcs.ICALP.2016.2,
  author =	{Leroy, Xavier},
  title =	{{Formally Verifying a Compiler: What Does It Mean, Exactly?}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.2},
  URN =		{urn:nbn:de:0030-drops-63384},
  doi =		{10.4230/LIPIcs.ICALP.2016.2},
  annote =	{Keywords: Compilers, Compiler Optimization, Compiler Verification}
}
Document
Invited Talk
Hardness of Approximation (Invited Talk)

Authors: Subhash Khot

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
The talk will present connections between approximability of NP-complete problems, analysis, and geometry, and the role played by the Unique Games Conjecture in facilitating these connections.

Cite as

Subhash Khot. Hardness of Approximation (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{khot:LIPIcs.ICALP.2016.3,
  author =	{Khot, Subhash},
  title =	{{Hardness of Approximation}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.3},
  URN =		{urn:nbn:de:0030-drops-63395},
  doi =		{10.4230/LIPIcs.ICALP.2016.3},
  annote =	{Keywords: NP-completeness, Approximation algorithms, Inapproximability, Probabilistically Checkable Proofs, Discrete Fourier analysis}
}
Document
Invited Talk
Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk)

Authors: Marta Z. Kwiatkowska

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying quantitative probabilistic specifications such as the probability of a critical failure occurring or expected time to termination. Much progress has been made in recent years in algorithms, tools and applications of probabilistic model checking, as exemplified by the probabilistic model checker PRISM (http://www.prismmodelchecker.org). However, the unstoppable rise of autonomous systems, from robotic assistants to self-driving cars, is placing greater and greater demands on quantitative modelling and verification technologies. To address the challenges of autonomy we need to consider collaborative, competitive and adversarial behaviour, which is naturally modelled using game-theoretic abstractions, enhanced with stochasticity arising from randomisation and uncertainty. This paper gives an overview of quantitative verification and strategy synthesis techniques developed for turn-based stochastic multi-player games, summarising recent advances concerning multi-objective properties and compositional strategy synthesis. The techniques have been implemented in the PRISM-games model checker built as an extension of PRISM.

Cite as

Marta Z. Kwiatkowska. Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kwiatkowska:LIPIcs.ICALP.2016.4,
  author =	{Kwiatkowska, Marta Z.},
  title =	{{Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.4},
  URN =		{urn:nbn:de:0030-drops-62285},
  doi =		{10.4230/LIPIcs.ICALP.2016.4},
  annote =	{Keywords: Quantitative verification, Stochastic games, Temporal logic, Model checking, Strategy synthesis}
}
Document
Fine-Grained Complexity Analysis of Two Classic TSP Variants

Authors: Mark de Berg, Kevin Buchin, Bart M. P. Jansen, and Gerhard Woeginger

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)


Abstract
We analyze two classic variants of the Traveling Salesman Problem using the toolkit of fine-grained complexity. Our first set of results is motivated by the Bitonic tsp problem: given a set of n points in the plane, compute a shortest tour consisting of two monotone chains. It is a classic dynamicprogramming exercise to solve this problem in O(n^2) time. While the near-quadratic dependency of similar dynamic programs for Longest Common Subsequence and Discrete Fréchet Distance has recently been proven to be essentially optimal under the Strong Exponential Time Hypothesis, we show that bitonic tours can be found in subquadratic time. More precisely, we present an algorithm that solves bitonic tsp in O(n*log^2(n)) time and its bottleneck version in O(n*log^3(n)) time. In the more general pyramidal tsp problem, the points to be visited are labeled 1, ..., n and the sequence of labels in the solution is required to have at most one local maximum. Our algorithms for the bitonic (bottleneck) tsp problem also work for the pyramidal tsp problem in the plane. Our second set of results concerns the popular k-opt heuristic for tsp in the graph setting. More precisely, we study the k-opt decision problem, which asks whether a given tour can be improved by a k-opt move that replaces k edges in the tour by k new edges. A simple algorithm solves k-opt in O(n^k) time for fixed k. For 2-opt, this is easily seen to be optimal. For k = 3 we prove that an algorithm with a runtime of the form ~O(n^{3-epsilon}) exists if and only if All-Pairs Shortest Paths in weighted digraphs has such an algorithm. For general k-opt, it is known that a runtime of f(k)*n^{o(k/log(k))} would contradict the Exponential Time Hypothesis. The results for k = 2, 3 may suggest that the actual time complexity of k-opt is Theta(n^k). We show that this is not the case, by presenting an algorithm that finds the best k-move in O(n^{lfoor 2k/3 rfloor +1}) time for fixed k >= 3. This implies that 4-opt can be solved in O(n^3) time, matching the best-known algorithm for 3-opt. Finally, we show how to beat the quadratic barrier for k = 2 in two important settings, namely for points in the plane and when we want to solve 2-opt repeatedly

Cite as

Mark de Berg, Kevin Buchin, Bart M. P. Jansen, and Gerhard Woeginger. Fine-Grained Complexity Analysis of Two Classic TSP Variants. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{deberg_et_al:LIPIcs.ICALP.2016.5,
  author =	{de Berg, Mark and Buchin, Kevin and Jansen, Bart M. P. and Woeginger, Gerhard},
  title =	{{Fine-Grained Complexity Analysis of Two Classic TSP Variants}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{5:1--5:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.5},
  URN =		{urn:nbn:de:0030-drops-62770},
  doi =		{10.4230/LIPIcs.ICALP.2016.5},
  annote =	{Keywords: Traveling salesman problem, fine-grained complexity, bitonic tours, k-opt}
}
  • Refine by Author
  • 8 Sangiorgi, Davide
  • 3 Galanis, Andreas
  • 3 Goldberg, Leslie Ann
  • 3 Hajiaghayi, Mohammad Taghi
  • 3 Mitzenmacher, Michael
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Concurrency
  • 2 Theory of computation → Program semantics
  • 2 Theory of computation → Semantics and reasoning
  • 1 Computer systems organization → Cloud computing

  • Refine by Keyword
  • 5 Approximation Algorithms
  • 5 communication complexity
  • 3 Approximation algorithms
  • 3 Bisimulation
  • 3 complexity
  • Show More...

  • Refine by Type
  • 159 document
  • 1 volume

  • Refine by Publication Year
  • 153 2016
  • 3 2022
  • 2 2020
  • 1 2017
  • 1 2023

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