9 Search Results for "Hankin, Chris"


Document
Circuit Transformations for Quantum Architectures

Authors: Andrew M. Childs, Eddie Schoute, and Cem M. Unsal

Published in: LIPIcs, Volume 135, 14th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2019)


Abstract
Quantum computer architectures impose restrictions on qubit interactions. We propose efficient circuit transformations that modify a given quantum circuit to fit an architecture, allowing for any initial and final mapping of circuit qubits to architecture qubits. To achieve this, we first consider the qubit movement subproblem and use the ROUTING VIA MATCHINGS framework to prove tighter bounds on parallel routing. In practice, we only need to perform partial permutations, so we generalize ROUTING VIA MATCHINGS to that setting. We give new routing procedures for common architecture graphs and for the generalized hierarchical product of graphs, which produces subgraphs of the Cartesian product. Secondly, for serial routing, we consider the TOKEN SWAPPING framework and extend a 4-approximation algorithm for general graphs to support partial permutations. We apply these routing procedures to give several circuit transformations, using various heuristic qubit placement subroutines. We implement these transformations in software and compare their performance for large quantum circuits on grid and modular architectures, identifying strategies that work well in practice.

Cite as

Andrew M. Childs, Eddie Schoute, and Cem M. Unsal. Circuit Transformations for Quantum Architectures. In 14th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 135, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{childs_et_al:LIPIcs.TQC.2019.3,
  author =	{Childs, Andrew M. and Schoute, Eddie and Unsal, Cem M.},
  title =	{{Circuit Transformations for Quantum Architectures}},
  booktitle =	{14th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2019)},
  pages =	{3:1--3:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-112-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{135},
  editor =	{van Dam, Wim and Man\v{c}inska, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2019.3},
  URN =		{urn:nbn:de:0030-drops-103958},
  doi =		{10.4230/LIPIcs.TQC.2019.3},
  annote =	{Keywords: quantum circuit, quantum architectures, circuit mapping}
}
Document
Higher-Order Demand-Driven Program Analysis

Authors: Zachary Palmer and Scott F. Smith

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)


Abstract
We explore a novel approach to higher-order program analysis that brings ideas of on-demand lookup from first-order CFL-reachability program analyses to higher-order programs. The analysis needs to produce only a control-flow graph; it can derive all other information including values of variables directly from the graph. Several challenges had to be overcome, including how to build the control-flow graph on-the-fly and how to deal with non-local variables in functions. The resulting analysis is flow- and context-sensitive with a provable polynomial-time bound. The analysis is formalized and proved correct and terminating, and an initial implementation is described.

Cite as

Zachary Palmer and Scott F. Smith. Higher-Order Demand-Driven Program Analysis. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 19:1-19:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{palmer_et_al:LIPIcs.ECOOP.2016.19,
  author =	{Palmer, Zachary and Smith, Scott F.},
  title =	{{Higher-Order Demand-Driven Program Analysis}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{19:1--19:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.19},
  URN =		{urn:nbn:de:0030-drops-61132},
  doi =		{10.4230/LIPIcs.ECOOP.2016.19},
  annote =	{Keywords: functional programming, program analysis, polynomial-time, demand-driven, flow-sensitive, context-sensitive}
}
Document
Variability Abstractions: Trading Precision for Speed in Family-Based Analyses

Authors: Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski

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


Abstract
Family-based (lifted) data-flow analysis for Software Product Lines (SPLs) is capable of analyzing all valid products (variants) without generating any of them explicitly. It takes as input only the common code base, which encodes all variants of a SPL, and produces analysis results corresponding to all variants. However, the computational cost of the lifted analysis still depends inherently on the number of variants (which is exponential in the number of features, in the worst case). For a large number of features, the lifted analysis may be too costly or even infeasible. In this paper, we introduce variability abstractions defined as Galois connections and use abstract interpretation as a formal method for the calculational-based derivation of approximate (abstracted) lifted analyses of SPL programs, which are sound by construction. Moreover, given an abstraction we define a syntactic transformation that translates any SPL program into an abstracted version of it, such that the analysis of the abstracted SPL coincides with the corresponding abstracted analysis of the original SPL. We implement the transformation in a tool, that works on Object-Oriented Java program families, and evaluate the practicality of this approach on three Java SPL benchmarks.

Cite as

Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability Abstractions: Trading Precision for Speed in Family-Based Analyses. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 247-270, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{dimovski_et_al:LIPIcs.ECOOP.2015.247,
  author =	{Dimovski, Aleksandar S. and Brabrand, Claus and Wasowski, Andrzej},
  title =	{{Variability Abstractions: Trading Precision for Speed in Family-Based Analyses}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{247--270},
  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.247},
  URN =		{urn:nbn:de:0030-drops-52253},
  doi =		{10.4230/LIPIcs.ECOOP.2015.247},
  annote =	{Keywords: Software Product Lines, Family-Based Program Analysis, Abstract Interpretation}
}
Document
Framework for Static Analysis of PHP Applications

Authors: David Hauzar and Jan Kofron

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


Abstract
Dynamic languages, such as PHP and JavaScript, are widespread and heavily used. They provide dynamic features such as dynamic type system, virtual and dynamic method calls, dynamic includes, and built-in dynamic data structures. This makes it hard to create static analyses, e.g., for automatic error discovery. Yet exploiting errors in such programs, especially in web applications, can have significant impacts. In this paper, we present static analysis framework for PHP, automatically resolving features common to dynamic languages and thus reducing the complexity of defining new static analyses. In particular, the framework enables defining value and heap analyses for dynamic languages independently and composing them automatically and soundly. We used the framework to implement static taint analysis for finding security vulnerabilities. The analysis has revealed previously unknown security problems in real application. Comparing to existing state-of-the-art analysis tools for PHP, it has found more real problems with a lower false-positive rate.

Cite as

David Hauzar and Jan Kofron. Framework for Static Analysis of PHP Applications. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 689-711, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{hauzar_et_al:LIPIcs.ECOOP.2015.689,
  author =	{Hauzar, David and Kofron, Jan},
  title =	{{Framework for Static Analysis of PHP Applications}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{689--711},
  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.689},
  URN =		{urn:nbn:de:0030-drops-52435},
  doi =		{10.4230/LIPIcs.ECOOP.2015.689},
  annote =	{Keywords: Static analysis, abstract interpretation, dynamic languages, PHP, security}
}
Document
Formally Verified Implementation of an Idealized Model of Virtualization

Authors: Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)


Abstract
VirtualCert is a machine-checked model of virtualization that can be used to reason about isolation between operating systems in presence of cache-based side-channels. In contrast to most prominent projects on operating systems verification, where such guarantees are proved directly on concrete implementations of hypervisors, VirtualCert abstracts away most implementations issues and specifies the effects of hypervisor actions axiomatically, in terms of preconditions and postconditions. Unfortunately, seemingly innocuous implementation issues are often relevant for security. Incorporating the treatment of errors into VirtualCert is therefore an important step towards strengthening the isolation theorems proved in earlier work. In this paper, we extend our earlier model with errors, and prove that isolation theorems still apply. In addition, we provide an executable specification of the hypervisor, and prove that it correctly implements the axiomatic model. The executable specification constitutes a first step towards a more realistic implementation of a hypervisor, and provides a useful tool for validating the axiomatic semantics developed in previous work.

Cite as

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna. Formally Verified Implementation of an Idealized Model of Virtualization. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 45-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


Copy BibTex To Clipboard

@InProceedings{barthe_et_al:LIPIcs.TYPES.2013.45,
  author =	{Barthe, Gilles and Betarte, Gustavo and Campo, Juan Diego and Chimento, Jes\'{u}s Mauricio and Luna, Carlos},
  title =	{{Formally Verified Implementation of an Idealized Model of Virtualization}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{45--63},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.45},
  URN =		{urn:nbn:de:0030-drops-46254},
  doi =		{10.4230/LIPIcs.TYPES.2013.45},
  annote =	{Keywords: virtualization, Cache and TLB, Executable specification, Error management, Isolation}
}
Document
Security through Analysis and Verification (Dagstuhl Seminar 00501)

Authors: Pierpaolo Degano, Roberto Gorrieri, Chris Hankin, Flemming Nielson, and Hanne Riis Nielson

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Pierpaolo Degano, Roberto Gorrieri, Chris Hankin, Flemming Nielson, and Hanne Riis Nielson. Security through Analysis and Verification (Dagstuhl Seminar 00501). Dagstuhl Seminar Report 294, pp. 1-15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2001)


Copy BibTex To Clipboard

@TechReport{degano_et_al:DagSemRep.294,
  author =	{Degano, Pierpaolo and Gorrieri, Roberto and Hankin, Chris and Nielson, Flemming and Riis Nielson, Hanne},
  title =	{{Security through Analysis and Verification (Dagstuhl Seminar 00501)}},
  pages =	{1--15},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{294},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.294},
  URN =		{urn:nbn:de:0030-drops-151781},
  doi =		{10.4230/DagSemRep.294},
}
Document
New Trends In the Integration of Paradigms (Dagstuhl Seminar 9538)

Authors: Chris Hankin and Hanne Riis Nielson

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Chris Hankin and Hanne Riis Nielson. New Trends In the Integration of Paradigms (Dagstuhl Seminar 9538). Dagstuhl Seminar Report 126, pp. 1-27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (1996)


Copy BibTex To Clipboard

@TechReport{hankin_et_al:DagSemRep.126,
  author =	{Hankin, Chris and Riis Nielson, Hanne},
  title =	{{New Trends In the Integration of Paradigms (Dagstuhl Seminar 9538)}},
  pages =	{1--27},
  ISSN =	{1619-0203},
  year =	{1996},
  type = 	{Dagstuhl Seminar Report},
  number =	{126},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.126},
  URN =		{urn:nbn:de:0030-drops-150143},
  doi =		{10.4230/DagSemRep.126},
}
Document
Functional Languages: Compiler Technology and Parallelism (Dagstuhl Seminar 9213)

Authors: Werner Damm, Chris Hankin, and John Hughes

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Werner Damm, Chris Hankin, and John Hughes. Functional Languages: Compiler Technology and Parallelism (Dagstuhl Seminar 9213). Dagstuhl Seminar Report 36, pp. 1-32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (1992)


Copy BibTex To Clipboard

@TechReport{damm_et_al:DagSemRep.36,
  author =	{Damm, Werner and Hankin, Chris and Hughes, John},
  title =	{{Functional Languages: Compiler Technology and Parallelism (Dagstuhl Seminar 9213)}},
  pages =	{1--32},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{36},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.36},
  URN =		{urn:nbn:de:0030-drops-149240},
  doi =		{10.4230/DagSemRep.36},
}
Document
Functional Languages: Optimization for Parallelism (Dagstuhl Seminar 9036)

Authors: Hankin Chris and Wilhelm Reinhard

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Hankin Chris and Wilhelm Reinhard. Functional Languages: Optimization for Parallelism (Dagstuhl Seminar 9036). Dagstuhl Seminar Report 3, pp. 1-28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (1991)


Copy BibTex To Clipboard

@TechReport{chris_et_al:DagSemRep.3,
  author =	{Chris, Hankin and Reinhard, Wilhelm},
  title =	{{Functional Languages: Optimization for Parallelism (Dagstuhl Seminar 9036)}},
  pages =	{1--28},
  ISSN =	{1619-0203},
  year =	{1991},
  type = 	{Dagstuhl Seminar Report},
  number =	{3},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.3},
  URN =		{urn:nbn:de:0030-drops-148914},
  doi =		{10.4230/DagSemRep.3},
}
  • Refine by Author
  • 3 Hankin, Chris
  • 2 Riis Nielson, Hanne
  • 1 Barthe, Gilles
  • 1 Betarte, Gustavo
  • 1 Brabrand, Claus
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Physics
  • 1 Computer systems organization → Quantum computing
  • 1 General and reference → General conference proceedings
  • 1 Hardware → Quantum computation
  • 1 Mathematics of computing → Graph theory
  • Show More...

  • Refine by Keyword
  • 1 Abstract Interpretation
  • 1 Cache and TLB
  • 1 Error management
  • 1 Executable specification
  • 1 Family-Based Program Analysis
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 2 2015
  • 1 1991
  • 1 1992
  • 1 1996
  • 1 2001
  • 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