10 Search Results for "Bartocci, Ezio"

Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2026.2
Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
With substantial progress in automated reasoning, algebraic approaches emerged to automatically analyse program loops in an exact manner. In this invited talk, we discuss recent results in characterizing the functional behaviour of loops with polynomial arithmetic and probabilistic updates. This problem remains unsolved even when we restrict consideration to loops that are non-nested, without conditionals, and/or without exit conditions [Ehud Hrushovski et al., 2023; Julian Müllner and others, 2024]. We are motivated by applications of computer-aided verification, in particular to assess the safety, security, and sensitivity of computer systems [M. Z. Kwiatkowska et al., 2011; Gilles Barthe et al., 2012; Gilles Barthe and others, 2018; Marcel Moosbrugger et al., 2023; Alessandro Abate et al., 2023; Andrey Kofnov and others, 2024]. We are interested in modeling, deciding, and solving loop analysis. The key to our work are moment-computable loops [L. Kovács, 2008; Marcel Moosbrugger et al., 2022] which allow us to set limits on what is decidable and solvable in loop analysis. Our approach combines algebra, statistics, and automated reasoning to mechanize loop analysis. Various techniques, such as martingale theory and quantifier elimination, can be seen as examples of moment-computable loop analysis. This talk is structured within three inter-connected parts. We first bring moment-based loop analysis into the landscape of {loop invariant synthesis} and extend moment-computable loops with {termination guarantees}. We next automate the reasoning about (probabilistic) loops by summarizing loop semantics as (probabilistic) algebraic recurrences, whose closed-form solutions capture (higher-order) moments, and hence invariants, among loop variables. These recurrences together with loop tests yield moment-based (super)martingales necessary to prove loop termination and compute probability bounds on termination. We finally describe moment-computable loops whose invariant synthesis {decidable} or as {hard} as open problems, such as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008].
Cite as

Laura Kovács. Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk). In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.STACS.2026.2,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Moments in Time: Algebraic Analysis for Solvable Loops}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.2},
  URN =		{urn:nbn:de:0030-drops-254910},
  doi =		{10.4230/LIPIcs.STACS.2026.2},
  annote =	{Keywords: program analysis, algebraic reasoning, symbolic computation, loop invariants}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.20
Flavors of Quantifiers in Hyperlogics

Authors: Marek Chalupa, Thomas A. Henzinger, and Ana Oliveira da Costa

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

Abstract
Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple traces. In this work, we extend hypertrace logic by introducing trace quantifiers that range over the set of all possible traces. In this extended logic, formulas can quantify over two kinds of trace variables: constrained trace variables, which range over a fixed set of traces defined by the model, and unconstrained trace variables, which can be assigned to any trace. In comparison, hyperlogics such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic to study how different quantifier patterns affect the decidability of the satisfiability problem. We prove that hypertrace logic without constrained trace quantifiers is equivalent to monadic second-order logic of one successor (S1S), and therefore satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace formulas where the only alternation between constrained trace quantifiers is from an existential to a universal quantifier are equisatisfiable to formulas without constraints on their trace variables and, therefore, decidable as well. Our framework allows us to study also time-prefixed hyperlogics, for which we provide new decidability and undecidability results.
Cite as

Marek Chalupa, Thomas A. Henzinger, and Ana Oliveira da Costa. Flavors of Quantifiers in Hyperlogics. 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. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chalupa_et_al:LIPIcs.FSTTCS.2025.20,
  author =	{Chalupa, Marek and Henzinger, Thomas A. and Oliveira da Costa, Ana},
  title =	{{Flavors of Quantifiers in Hyperlogics}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{20:1--20: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.20},
  URN =		{urn:nbn:de:0030-drops-251016},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.20},
  annote =	{Keywords: Hyperproperties, Satisfiability, First-order Logic, S1S}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.76
Deciding Termination of Simple Randomized Loops

Authors: Éléanore Meyer and Jürgen Giesl

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a program is finite for all inputs. Our class contains all programs that consist of a single loop, with a linear loop guard and a loop body composed of two linear commuting and diagonalizable updates. In each iteration of the loop, the update to be carried out is picked at random, according to a fixed probability. We show the decidability of UPAST for this class of programs, where the program’s variables and inputs may range over various sub-semirings of the real numbers. In this way, we extend a line of research initiated by Tiwari in 2004 into the realm of randomized programs.
Cite as

Éléanore Meyer and Jürgen Giesl. Deciding Termination of Simple Randomized Loops. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 76:1-76:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{meyer_et_al:LIPIcs.MFCS.2025.76,
  author =	{Meyer, \'{E}l\'{e}anore and Giesl, J\"{u}rgen},
  title =	{{Deciding Termination of Simple Randomized Loops}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{76:1--76:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.76},
  URN =		{urn:nbn:de:0030-drops-241833},
  doi =		{10.4230/LIPIcs.MFCS.2025.76},
  annote =	{Keywords: decision procedures, randomized programs, linear loops, positive almost sure termination}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

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

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4: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.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.10
The Complexity of Second-Order HyperLTL

Authors: Hadar Frenkel and Martin Zimmermann

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

Abstract
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is Σ₁¹-complete, i.e., only as hard as for (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in Σ₂² and are Σ₁¹-hard, and thus also less complex than for full second-order HyperLTL.
Cite as

Hadar Frenkel and Martin Zimmermann. The Complexity of Second-Order HyperLTL. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{frenkel_et_al:LIPIcs.CSL.2025.10,
  author =	{Frenkel, Hadar and Zimmermann, Martin},
  title =	{{The Complexity of Second-Order HyperLTL}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{10:1--10:23},
  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.10},
  URN =		{urn:nbn:de:0030-drops-227679},
  doi =		{10.4230/LIPIcs.CSL.2025.10},
  annote =	{Keywords: HyperLTL, Satisfiability, Model-checking}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2023.1
Learning Temporal Logic Formulas from Time-Series Data (Invited Talk)

Authors: Laura Nenzi

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
In this talk, we provide an overview of recent advancements in the field of mining formal specifications from time-series data, with a specific focus on learning Signal Temporal Logic (STL) formulae.
Cite as

Laura Nenzi. Learning Temporal Logic Formulas from Time-Series Data (Invited Talk). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nenzi:LIPIcs.TIME.2023.1,
  author =	{Nenzi, Laura},
  title =	{{Learning Temporal Logic Formulas from Time-Series Data}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.1},
  URN =		{urn:nbn:de:0030-drops-190917},
  doi =		{10.4230/LIPIcs.TIME.2023.1},
  annote =	{Keywords: Temporal Logic, Mining Specifications}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.21
Hypernode Automata

Authors: Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automata. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs.
Cite as

Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. Hypernode Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bartocci_et_al:LIPIcs.CONCUR.2023.21,
  author =	{Bartocci, Ezio and Henzinger, Thomas A. and Nickovic, Dejan and Oliveira da Costa, Ana},
  title =	{{Hypernode Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.21},
  URN =		{urn:nbn:de:0030-drops-190153},
  doi =		{10.4230/LIPIcs.CONCUR.2023.21},
  annote =	{Keywords: Hyperproperties, Asynchronous, Automata, Logic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2023.4
Algebraic Reasoning for (Un)Solvable Loops (Invited Talk)

Authors: Laura Kovács

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
Loop invariants describe valid program properties that hold before and after every loop iteration. As such, loop invariants are the workhorses in formalizing loop semantics and automating the formal analysis and verification of programs with loops. While automatically synthesizing loop invariants is, in general, an uncomputable problem, when considering only single-path loops with linear updates (linear loops), the strongest polynomial invariant is in fact computable [Michael Karr, 1976; Markus Müller-Olm and Helmut Seidl, 2004; Laura Kovács, 2008; Ehud Hrushovski et al., 2018]. Yet, already for loops with "only" polynomial updates, computing the strongest invariant has been an open challenge since 2004 [Markus Müller-Olm and Helmut Seidl, 2004]. In this invited talk, we first present computability results on polynomial invariant synthesis for restricted polynomial loops, called solvable loops [Rodríguez-Carbonell and Kapur, 2004]. Key to solvable loops is that one can automatically compute invariants from closed-form solutions of algebraic recurrence equations that model the loop behaviour [Laura Kovács, 2008; Andreas Humenberger et al., 2017]. We also establish a technique for invariant synthesis for classes of loops that are not solvable, termed unsolvable loops [Daneshvar Amrollahi et al., 2022]. We next study the limits of computability in deriving the (strongest) polynomial invariants for arbitrary polynomial loops. We prove that computing the strongest polynomial invariant of arbitrary, single-path polynomial loops is very hard [Julian Müllner, 2023] - namely, it is at least as hard as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008], a prominent algebraic problem in the theory of linear recurrences. Going beyond single-path loops, we show that the strongest polynomial invariant is uncomputable already for multi-path polynomial loops with arbitrary quadratic polynomial updates [Laura Kovács and Anton Varonka, 2023].
Cite as

Laura Kovács. Algebraic Reasoning for (Un)Solvable Loops (Invited Talk). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kovacs:LIPIcs.MFCS.2023.4,
  author =	{Kov\'{a}cs, Laura},
  title =	{{Algebraic Reasoning for (Un)Solvable Loops}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{4:1--4:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.4},
  URN =		{urn:nbn:de:0030-drops-185385},
  doi =		{10.4230/LIPIcs.MFCS.2023.4},
  annote =	{Keywords: Symbolic Computation, Formal Methods, Loop Analysis, Polynomial Invariants}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.1
Locally Static, Globally Dynamic Session Types for Active Objects

Authors: Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan

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

Abstract
Active object languages offer an attractive trade-off between low-level, preemptive concurrency and fully distributed actors: syntactically identifiable atomic code segments and asynchronous calls are the basis of cooperative concurrency, still permitting interleaving, but nevertheless being mechanically analyzable. The challenge is to reconcile local static analysis of atomic segments with the global scheduling constraints it depends on. Here, we propose an approximate, hybrid approach; At compile-time we perform a local static analysis: later, any run not complying to a global specification is excluded via runtime checks. That specification is expressed in a type-theoretic language inspired by session types. The approach reverses the usual (first global, then local) order of analysis and, thereby, supports analysis of open distributed systems.
Cite as

Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan. Locally Static, Globally Dynamic Session Types for Active Objects. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hahnle_et_al:OASIcs.Gabbrielli.1,
  author =	{H\"{a}hnle, Reiner and Haubner, Anton W. and Kamburjan, Eduard},
  title =	{{Locally Static, Globally Dynamic Session Types for Active Objects}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{1:1--1:24},
  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.1},
  URN =		{urn:nbn:de:0030-drops-132237},
  doi =		{10.4230/OASIcs.Gabbrielli.1},
  annote =	{Keywords: Session Types, Active Objects, Runtime Verification, Static Verification}
}
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}
}
  • Refine by Type
  • 10 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 4 2025
  • 3 2023
  • 2 2020

  • Refine by Author
  • 2 Henzinger, Thomas A.
  • 2 Kovács, Laura
  • 2 Oliveira da Costa, Ana
  • 1 Aceto, Luca
  • 1 Achilleos, Antonis
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs
  • 2 OASIcs

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 2 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Probabilistic computation
  • 1 Mathematics of computing → Discrete mathematics
  • 1 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Hyperproperties
  • 2 Satisfiability
  • 1 Active Objects
  • 1 Asynchronous
  • 1 Automata
  • 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