We give a new order-theoretic characterization of a complete Heyting and co-Heyting algebra $C$. This result provides an unexpected relationship with the field of Nash equilibria, being based on the ...so-called Veinott ordering relation on subcomplete sublattices of $C$, which is crucially used in Topkis' theorem for studying the order-theoretic stucture of Nash equilibria of supermodular games.
We introduce the notion of local completeness in abstract interpretation and define a logic for proving both the correctness and incorrectness of some program specification. Abstract interpretation ...is extensively used to design sound-by-construction program analyses that over-approximate program behaviours. Completeness of an abstract interpretation A for all possible programs and inputs would be an ideal situation for verifying correctness specifications, because the analysis can be done compositionally and no false alert will arise. Our first result shows that the class of programs whose abstract analysis on A is complete for all inputs has a severely limited expressiveness. A novel notion of local completeness weakens the above requirements by considering only some specific, rather than all, program inputs and thus finds wider applicability. In fact, our main contribution is the design of a proof system, parameterized by an abstraction A, that, for the first time, combines over- and under-approximations of program behaviours. Thanks to local completeness, in a provable triple ⊢A P c Q, the assertion Q is an under-approximation of the strongest post-condition postc(P) such that the abstractions in A of Q and postc(P) coincide. This means that Q is never too coarse, namely, under mild assumptions, the abstract interpretation of c does not yield false alerts for the input P iff Q has no alert. Thus, ⊢A P c Q not only ensures that all the alerts raised in Q are true ones, but also that if Q does not raise alerts then c is correct.
This volume of Formal Methods in System Design (FMSD) features extended and revised versions of a selection of papers presented at the Static Analysis Symposium (SAS) held on 2017 in New York, NY. ...The series of Static Analysis Symposia serves as a primary venue for the presentation of theoretical, practical, and applicational advances in the area of static analysis of programs and systems. After the conference, the Program Committee selected the best papers of SAS 2017 and invited their authors to submit an extended version. This special issue of FMSD contains the four high-quality articles that were accepted after a careful reviewing process.
Supermodular games are a well known class of noncooperative games which find significant applications in a variety of models, especially in operations research and economic applications. Supermodular ...games always have Nash equilibria which are characterized as fixed points of multivalued functions on complete lattices. Abstract interpretation is here applied to set up an approximation framework for Nash equilibria of supermodular games. This is achieved by extending the theory of abstract interpretation in order to cope with approximations of multivalued functions and by providing some methods for abstracting supermodular games, thus obtaining approximate Nash equilibria which are shown to be correct within the abstract interpretation framework.
History of Abstract Interpretation Giacobazzi, Roberto; Ranzato, Francesco
IEEE annals of the history of computing,
04/2022, Letnik:
44, Številka:
2
Journal Article
Recenzirano
Odprti dostop
We trace the roots of abstract interpretation and its role as a foundational principle to understand and design static program analysis and verification methods. Starting from the historical roots of ...formal methods and static program analysis, we show how abstract interpretation evolved and influenced the way we reason about program correctness in different programming languages and how this method shaped the literature and the practice in program analysis in the last 45 years.
Abstract interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are ...lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis. We introduce a weaker notion of completeness, called local completeness, which requires that no false alarms are produced only relatively to some fixed program inputs. Based on this idea, we introduce a program logic, called Local Completeness Logic for an abstract domain A, for proving both the correctness and incorrectness of program specifications. Our proof system, which is parameterized by an abstract domain A, combines over- and under-approximating reasoning. In a provable triple ⊦A p q, is a program, q is an under-approximation of the strongest post-condition of on input p such that their abstractions in A coincide. This means that q is never too coarse, namely, under some mild assumptions, the abstract interpretation of does not yield false alarms for the input p iff q has no alarm. Therefore, proving ⊦A p q not only ensures that all the alarms raised in q are true ones, but also that if q does not raise alarms, then is correct. We also prove that if A is the straightforward abstraction making all program properties equivalent, then our program logic coincides with O’Hearn’s incorrectness logic, while for any other abstraction, contrary to the case of incorrectness logic, our logic can also establish program correctness.
Classical results in computability theory, notably Rice's theorem, focus on the extensional content of programs, namely, on the partial recursive functions that programs compute. Later work ...investigated intensional generalisations of such results that take into account the way in which functions are computed, thus affected by the specific programs computing them. In this paper, we single out a novel class of program semantics based on abstract domains of program properties that are able to capture nonextensional aspects of program computations, such as their asymptotic complexity or logical invariants, and allow us to generalise some foundational computability results such as Rice's Theorem and Kleene's Second Recursion Theorem to these semantics. In particular, it turns out that for this class of abstract program semantics, any nontrivial abstract property is undecidable and every decidable over-approximation necessarily includes an infinite set of false positives which covers all the values of the semantic abstract domain.
Abstract We study the certification of stability properties, such as robustness and individual fairness, of the k -nearest neighbor algorithm ( k NN). Our approach leverages abstract interpretation, ...a well-established program analysis technique that has been proven successful in verifying several machine learning algorithms, notably, neural networks, decision trees, and support vector machines. In this work, we put forward an abstract interpretation-based framework for designing a sound approximate version of the k NN algorithm, which is instantiated to the interval and zonotope abstractions for approximating the range of numerical features. We show how this abstraction-based method can be used for stability, robustness, and individual fairness certification of k NN. Our certification technique has been implemented and experimentally evaluated on several benchmark datasets. These experimental results show that our tool can formally prove the stability of k NN classifiers in a precise and efficient way, thus expanding the range of machine learning models amenable to robustness certification.
We study the language inclusion problem
L
1
⊆
L
2
, where
L
1
is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of
L
1
, ...obtained by approximating the Kleene iterates of its least fixpoint characterization, is included in
L
2
. We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e., its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e., it guarantees termination of least fixpoint computations). This overapproximating abstraction of languages can be defined using quasiorder relations on words, where the abstraction gives the language of all the words “greater than or equal to” a given input word for that quasiorder. We put forward a range of such quasiorders that allow us to systematically design decision procedures for different language inclusion problems, such as regular languages into regular languages or into trace sets of one-counter nets, and context-free languages into regular languages. In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms, like the so-called antichain algorithms. Finally, we provide an equivalent language inclusion checking algorithm based on a greatest fixpoint computation that relies on quotients of languages and, to the best of our knowledge, was not previously known.
A number of algorithms for computing the simulation preorder (and equivalence) on Kripke structures are available. Let
Σ
denote the state space,
→
the transition relation and
P
sim
the partition of
Σ
...induced by simulation equivalence. While some algorithms are designed to reach the best space bounds, whose dominating additive term is
|
P
sim
|
2
, other algorithms are devised to attain the best time complexity
O
(
|
P
sim
|
|
→
|
)
. We present a novel simulation algorithm which is both space and time efficient: it runs in
O
(
|
P
sim
|
2
log
|
P
sim
|
+
|
Σ
|
log
|
Σ
|
)
space and
O
(
|
P
sim
|
|
→
|
log
|
Σ
|
)
time. Our simulation algorithm thus reaches the best space bounds while closely approaching the best time complexity.
PDF
