13 Search Results for "Hankin, Chris"

Document
DOI: 10.4230/LIPIcs.CSL.2026.45
Reasoning About Quality in Hyperproperties

Authors: Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman [Almagor et al., 2016] where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.
Cite as

Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning About Quality in Hyperproperties. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{graepler_et_al:LIPIcs.CSL.2026.45,
  author =	{Graepler, Samuel and Monmege, Benjamin and Talbot, Jean-Marc},
  title =	{{Reasoning About Quality in Hyperproperties}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{45:1--45:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.45},
  URN =		{urn:nbn:de:0030-drops-254704},
  doi =		{10.4230/LIPIcs.CSL.2026.45},
  annote =	{Keywords: Hyperlogics, Automata-based model checking, Quantitative verification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.18
Iterating Non-Aggregative Structure Compositions

Authors: Marius Bozga, Radu Iosif, and Florian Zuleger

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface. In this paper, we study a non-aggregative composition operation, called fusion, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite hyperedge-replacement (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called context-free. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possiblity of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.
Cite as

Marius Bozga, Radu Iosif, and Florian Zuleger. Iterating Non-Aggregative Structure Compositions. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bozga_et_al:LIPIcs.FSTTCS.2025.18,
  author =	{Bozga, Marius and Iosif, Radu and Zuleger, Florian},
  title =	{{Iterating Non-Aggregative Structure Compositions}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.18},
  URN =		{urn:nbn:de:0030-drops-250997},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.18},
  annote =	{Keywords: Hyperedge replacement, Tree-width}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.23
First-Order Store and Visibility in Name-Passing Calculi

Authors: Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed.
Cite as

Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-Order Store and Visibility in Name-Passing Calculi. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2025.23,
  author =	{Hirschkoff, Daniel and Qu\'{e}merais, Iwan and Sangiorgi, Davide},
  title =	{{First-Order Store and Visibility in Name-Passing Calculi}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.23},
  URN =		{urn:nbn:de:0030-drops-239737},
  doi =		{10.4230/LIPIcs.CONCUR.2025.23},
  annote =	{Keywords: process calculi, behavioural equivalence, type system}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.18
Knowledge Problems vs Unification and Matching: Dichotomy Results

Authors: Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The research area of cryptographic protocol analysis contains a number of innovative algorithms and procedures for checking various security properties of protocols. Most of these procedures focus on solving one of several "knowledge problems" that model intruder knowledge. Solving these problems can demonstrate the ability of the intruder to obtain some forbidden information of the protocol, such as secret keys. Two important examples of these problems are the deduction problem and the static equivalence problem. Deduction is concerned with the ability to derive a term from a set of terms (or knowledge) obtained from the observation of a protocol instance. Static equivalence, on the other hand, is concerned with distinguishing between two runs of a protocol based on two sets of knowledge. These two knowledge problems at first inspection appear to be very close to the older automated reasoning problems of matching and unification. However, this first impression is wrong, and there have been a few results that have shown theories where one problem, such as unification, is undecidable but another problem, such as deduction, is decidable. These existing dichotomy results were, however, incomplete, and not all cases had been examined, thus leaving the possibility of some connection between the problems for those unexamined cases. In this paper, we consider the missing dichotomy cases. For each of the remaining cases, we demonstrate a theory that separates the two problems. In addition, once the dichotomy results are completed, it leaves open the question of the existence of non-trivial classes of theories for which all four of the problems are decidable. One example for which this is true is the well-known class of subterm convergent term rewrite systems. In this paper, we develop another example, a class of restrictive permutative theories for which all problems are likewise decidable.
Cite as

Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Knowledge Problems vs Unification and Matching: Dichotomy Results. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{erbatur_et_al:LIPIcs.FSCD.2025.18,
  author =	{Erbatur, Serdar and Marshall, Andrew M. and Narendran, Paliath and Ringeissen, Christophe},
  title =	{{Knowledge Problems vs Unification and Matching: Dichotomy Results}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.18},
  URN =		{urn:nbn:de:0030-drops-236331},
  doi =		{10.4230/LIPIcs.FSCD.2025.18},
  annote =	{Keywords: Knowledge Problems, Unification, Matching, Decidability}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.34
Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

Authors: Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is not scalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection. To address the above limitations, we present RecTopo, a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs. We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Cite as

Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.ECOOP.2025.34,
  author =	{Yang, Jiawei and Cheng, Xiao and Chang, Bor-Yuh Evan and Luo, Xiapu and Sui, Yulei},
  title =	{{Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{34:1--34:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.34},
  URN =		{urn:nbn:de:0030-drops-233265},
  doi =		{10.4230/LIPIcs.ECOOP.2025.34},
  annote =	{Keywords: Abstract interpretation, recursion, weak topological ordering}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.24
Fair Termination of Asynchronous Binary Sessions

Authors: Luca Padovani and Gianluigi Zavattaro

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Cite as

Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{padovani_et_al:LIPIcs.ECOOP.2025.24,
  author =	{Padovani, Luca and Zavattaro, Gianluigi},
  title =	{{Fair Termination of Asynchronous Binary Sessions}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{24:1--24:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.24},
  URN =		{urn:nbn:de:0030-drops-233169},
  doi =		{10.4230/LIPIcs.ECOOP.2025.24},
  annote =	{Keywords: Binary sessions, fair asynchronous subtyping, fair termination, linear logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.47
A Rewriting Theory for Quantum λ-Calculus

Authors: Claudia Faggian, Gaetan Lopez, and Benoît Valiron

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Quantum lambda calculus has been studied mainly as an idealized programming language - the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus are standardization and normalization results.
Cite as

Claudia Faggian, Gaetan Lopez, and Benoît Valiron. A Rewriting Theory for Quantum λ-Calculus. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{faggian_et_al:LIPIcs.CSL.2025.47,
  author =	{Faggian, Claudia and Lopez, Gaetan and Valiron, Beno\^{i}t},
  title =	{{A Rewriting Theory for Quantum \lambda-Calculus}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{47:1--47:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.47},
  URN =		{urn:nbn:de:0030-drops-228046},
  doi =		{10.4230/LIPIcs.CSL.2025.47},
  annote =	{Keywords: quantum lambda-calculus, probabilistic rewriting, operational semantics, asymptotic normalization, principles of quantum programming languages}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.4
Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation

Authors: Mila Dalla Preda

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

Abstract
Static and dynamic program analyses attempt to extract useful information on program’s behaviours. Static analysis uses an abstract model of programs to reason on their runtime behaviour without actually running them, while dynamic analysis reasons on a test set of real program executions. For this reason, the precision of static analysis is limited by the presence of false positives (executions allowed by the abstract model that cannot happen at runtime), while the precision of dynamic analysis is limited by the presence of false negatives (real executions that are not in the test set). Researchers have developed many analysis techniques and tools in the attempt to increase the precision of program verification. Software protection is an interesting scenario where programs need to be protected from adversaries that use program analysis to understand their inner working and then exploit this knowledge to perform some illicit actions. Program analysis plays a dual role in program verification and software protection: in program verification we want the analysis to be as precise as possible, while in software protection we want to degrade the results of the analysis as much as possible. Indeed, in software protection researchers usually recur to a special class of program transformations, called code obfuscation, to modify a program in order to make it more difficult to analyse while preserving its intended functionality. In this setting, it is interesting to study how program transformations that preserve the intended behaviour of programs can affect the precision of both static and dynamic analysis. While some works have been done in order to formalise the efficiency of code obfuscation in degrading static analysis and in the possibility of transforming programs in order to avoid or increase false positives, less attention has been posed to formalise the relation between program transformations and false negatives in dynamic analysis. In this work we are setting the scene for a formal investigation of the syntactic and semantic program features that affect the presence of false negatives in dynamic analysis. We believe that this understanding would be useful for improving the precision of the existing dynamic analysis tools and in the design of program transformations that complicate the dynamic analysis. To Maurizio on his 60th birthday!
Cite as

Mila Dalla Preda. Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dallapreda:OASIcs.Gabbrielli.4,
  author =	{Dalla Preda, Mila},
  title =	{{Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{4:1--4:22},
  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.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.4},
  URN =		{urn:nbn:de:0030-drops-132263},
  doi =		{10.4230/OASIcs.Gabbrielli.4},
  annote =	{Keywords: Program analysis, analysis precision, program transformation, software protection, code obfuscation}
}
Document
DOI: 10.4230/LITES-v005-i001-a003
The Semantic Foundations and a Landscape of Cache-Persistence Analyses

Authors: Jan Reineke

Published in: LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1

Abstract
We clarify the notion of cache persistence and contribute to the understanding of persistence analysis for caches with least-recently-used replacement.To this end, we provide the first formal definition of persistence as a property of a trace semantics. Based on this trace semantics we introduce a semantics-based, i.e., abstract-interpretation-based persistence analysis framework.We identify four basic persistence analyses and prove their correctness as instances of this analysis framework.Combining these basic persistence analyses via two generic cooperation mechanisms yields a lattice of ten persistence analyses.Notably, this lattice contains all persistence analyses previously described in the literature. As a consequence, we obtain uniform correctness proofs for all prior analyses and a precise understanding of how and why these analyses work, as well as how they relate to each other in terms of precision.
Cite as

Jan Reineke. The Semantic Foundations and a Landscape of Cache-Persistence Analyses. In LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1, pp. 03:1-03:52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{reineke:LITES-v005-i001-a003,
  author =	{Reineke, Jan},
  title =	{{The Semantic Foundations and a Landscape of Cache-Persistence Analyses}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:52},
  ISSN =	{2199-2002},
  year =	{2018},
  volume =	{5},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v005-i001-a003},
  URN =		{urn:nbn:de:0030-drops-192748},
  doi =		{10.4230/LITES-v005-i001-a003},
  annote =	{Keywords: caches, persistence analysis, WCET analysis}
}
Document
DOI: 10.4230/DagSemRep.294
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
DOI: 10.4230/DagSemRep.126
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
DOI: 10.4230/DagSemRep.36
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
DOI: 10.4230/DagSemRep.3
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 Type
  • 13 Document/PDF
  • 7 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 6 2025
  • 1 2020
  • 1 2018
  • 1 2001
  • Show More...

  • Refine by Author
  • 3 Hankin, Chris
  • 2 Riis Nielson, Hanne
  • 1 Bozga, Marius
  • 1 Chang, Bor-Yuh Evan
  • 1 Cheng, Xiao
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 1 OASIcs
  • 1 LITES
  • 4 DagSemRep

  • Refine by Classification
  • 2 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Linear logic
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Program analysis
  • 1 Computer systems organization → Real-time system architecture
  • Show More...

  • Refine by Keyword
  • 1 Abstract interpretation
  • 1 Automata-based model checking
  • 1 Binary sessions
  • 1 Decidability
  • 1 Hyperedge replacement
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact