Bruno Blanchet, Patrick Cousot, Radhia Cousot et al. · 2015
We show that abstract interpretation-based static program analysis can be made ecient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by renement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software. The main novelties are the design principle of static an-alyzers by renement and adaptation through parametriza-tion (Sect. 3 and 7), the symbolic manipulation of expres-sions to improve the precision of abstract transfer functions (Sect. 6.3), the octagon (Sect. 6.2.2), ellipsoid (Sect. 6.2.3), and decision tree (Sect. 6.2.4) abstract domains, all with sound handling of rounding errors in \noating point compu-tations, widening strategies (with thresholds: Sect. 7.1.2, delayed: Sect. 7.1.3) and the automatic determination of the parameters (parametrized packing: Sect. 7.2).
Cited by 0
Muroya, Koko · Centre International de Rencontres Mathématiques · 2022
Geometry of Interaction, combined with translation of lambda-calculus into MELL proof nets, has enabled an unconventional approach to program semantics. Danos and Regnier, and Mackie pioneered the approach, and introduced the so-called token-passing machines. It turned out that the unconventional token-passing machines can be turned into a graphical realisation of conventional reduction semantics, in a simple way. The resulting semantics can be more convenient than the standard (syntactical) reduction semantics, in analysing local behaviour of programs. I will explain how, in particular, the resulting graphical reduction semantics can be used to reason about observational equivalence between programs.
Cited by 0Open access
Bernd Grobauer · 2001
Programming is at least as much about manipulating existing code as it is about writing new code. Existing code is modified, for example to make inefficient code run faster, or to accommodate for new features when reusing code; existing code is analyzed, for example to verify certain program properties, or to use the analysis information for code modifications. Semantics-based program manipulation addresses methods for program modifications and program analyses that are formally defined and therefore can be verified with respect to the programming-language semantics. This dissertation comprises four articles in the field of semantics-based techniques for program manipulation: three articles are about partial evaluation, a method for program specialization; the fourth article treats an approach to automatic cost analysis.
Cited by 8
Yingzhou Zhang · InTech eBooks · 2012
Syntax: p :: = program ide is b b :: = d begin c end d :: = const ide = l.e | var ide : t | d1; d2 c :: = ide := l.e | c1; c2| skip | read ide | write l.e |while l.e do c endwhile | if l.e then c1 else c2 endif
Cited by 1Open access
Jeffery I. Zucker, Hing-Kai Hung · 2007
We apply intensional logic to the semantics of an Algol-like programming language. This associates with expressions their meanings relative to "possible worlds", here interpreted as machine states. These meanings lie in the semantic domains of a higher order typed intensional logic. The great advantage of this approach is that it preserves compositionality of the meaning function, even in "opaque contexts". This approach has been applied in three areas: (1) assignments (Janssen and Van Emde Boas 1977); (2) blocks and procedures with parameters passed by value and by reference (Hung 1990); and (3) assignments to pointers, and parameters passed by name (Hung and Zucker 1991). It is shown how this approach gives an elegant semantics which is simple, compositional and implementation independent. 1 Introduction 1.1 Denotational semantics; Compositionality. Assume (within some general framework) we have a number of syntactic domains \\Delta; : : : , and corresponding semantic domains D; : ...
Cited by 0
Aleksandar S. Dimovski · 2016
We introduce a new symbolic representation of algorithmic game semantics, and show how it can be applied for efficient verification of open (incomplete) programs. The focus is on an Algol-like programming language which contains the core ingredients of imperative and functional languages, especially on its second-order recursion-free fragment with infinite data types. We revisit the regular-language representation of game semantics of this language fragment. By using symbolic values instead of concrete ones, we generalize the standard notions of regular-language and automata representations of game semantics to that of corresponding symbolic representations. In this way programs with infinite data types, such as integers, can be expressed as finite-state symbolic-automata although the standard automata representation is infinite-state, i.e. the standard regular-language representation has infinite summations. More-over, in this way significant reductions of the state space of game semantics models are obtained. This enables efficient verification of programs by our pro-totype tool based on symbolic game models, which is illustrated with several examples.
Cited by 0
Graham Hutton · ACM SIGPLAN Notices · 1998
In this paper we explain how recursion operators can be used to structure and reason about program semantics within a functional language. In particular, we show how the recursion operator fold can be used to structure denotational semantics, how the dual recursion operator unfold can be used to structure operational semantics, and how algebraic properties of these operators can be used to reason about program semantics. The techniques are explained with the aid of two main examples, the first concerning arithmetic expressions, and the second concerning Milner's concurrent language CCS. The aim of the paper is to give functional programmers new insights into recursion operators, program semantics, and the relationships between them.
Cited by 1Open access
JoséLuiz Fiadeiro, Tom Maibaum · Science of Computer Programming · 1997
Cited by 93
Romain Péchoux · 2007
Il existe de nombreuses approches développées par la communauté Implicit Computational Complexity (ICC) permettant d'analyser les ressources nécessaires à la bonne exécution des algorithmes. Dans cette thèse, nous nous intéressons plus particulièrement au contrôle des ressources à l'aide d'interprétations sémantiques. Après avoir rappelé brièvement la notion de quasi-interprétation ainsi que les différentes propriétés et caractérisations qui en découlent, nous présentons les différentes avancées obtenues dans l'étude de cet outil : nous étudions le problème de la synthèse qui consiste à trouver une quasi-interprétation pour un programme donné, puis, nous abordons la question de la modularité des quasi-interprétations. La modularité permet de diminuer la complexité de la procédure de synthèse et de capturer un plus grand nombre d'algorithmes. Après avoir mentionné différentes extensions des quasi-interprétations à des langages de programmation réactifs, bytecode ou d'ordre supérieur, nous introduisons la sup-interprétation. Cette notion généralise la quasi-interprétation et est utilisée dans des critères de contrôle des ressources afin d'étudier la complexité d'un plus grand nombre d'algorithmes dont des algorithmes sur des données infinies ou des algorithmes de type diviser pour régner. Nous combinons cette notion à différents critères de terminaison comme les ordres RPO, les paires de dépendance ou le size-change principle et nous la comparons à la notion de quasi-interprétation. En outre, après avoir caractérisé des petites classes de complexité parallèles, nous donnons quelques heuristiques permettant de synthétiser des sup-interprétations sans la propriété sous-terme, c'est à dire des sup-interprétations qui ne sont pas des quasi-interprétations. Enfin, dans un dernier chapitre, nous adaptons les sup-interprétations à des langages orientés-objet, obtenant ainsi différents critères pour contrôler les ressources d'un programme objet et de ses méthodes
Cited by 0Open access
Nick Benton · 2005
These lectures are concerned with how we can formalize just what it is that a static analysis computes about programs and how we might begin to formalize the ways in which that information may be used in program transformation.
Cited by 2
Max Kanovich · Lecture notes in computer science · 1991
Cited by 11
Wiklicky, Herbert · arXiv (Cornell University) · 2014
For deterministic and probabilistic programs we investigate the problem of program synthesis and program optimisation (with respect to non-functional properties) in the general setting of global optimisation. This approach is based on the representation of the semantics of programs and program fragments in terms of linear operators, i.e. as matrices. We exploit in particular the fact that we can automatically generate the representation of the semantics of elementary blocks. These can then can be used in order to compositionally assemble the semantics of a whole program, i.e. the generator of the corresponding Discrete Time Markov Chain (DTMC). We also utilise a generalised version of Abstract Interpretation suitable for this linear algebraic or functional analytical framework in order to formulate semantical constraints (invariants) and optimisation objectives (for example performance requirements).
Cited by 0Open access
Gomes, Leandro Rafael Moreira · RepositóriUM (Universidade do Minho) · 2022
Cited by 0Open access
Gianluca Amato, Maria Chiara Meo, Francesca Scozzari · Theoretical Computer Science · 2020
Reasoning on a complex system in the abstract interpretation theory starts with a formal description of the system behavior specified by a collecting semantics. We take the common point of view that a collecting semantics is a very precise semantics from which other abstractions may be derived. We elaborate on both the concepts of precision and derivability, and introduce a notion of adequacy which tell us when a collecting semantics is a good choice for a given family of abstractions. We instantiate this approach to the case of first-order functional programs by considering three common collecting semantics and some abstract properties of functions. We study their relative precision and give a constructive characterization of the classes of abstractions which are adequate for the collecting semantics.
Cited by 4Open access
Sebastian Danicic, Mark Harman, John Howroyd et al. · Goldsmiths (University of London) · 2004
This paper demonstrates that if a slicing algorithm is expressed \ndenotationally, without intermediate structures, then the power of \ndenotational semantics can be used to prove correctness. \n \nThe semantics preserved by slicing algorithms, however, is non-standard. We introduce a new lazy semantics which we prove is preserved by slicing algorithms. \n \nIt is demonstrated how other concepts in program dependence, \ndifficult or impossible to express using standard semantics, \nfor example variable dependence, can be expressed naturally using our new lazy semantics.
Cited by 9
W. H. J. Feijen, A. J. M. van Gasteren · Texts and monographs in computer science · 1999
Cited by 0
Roberto Giacobazzi, Isabella Mastroeni · LISP and Symbolic Computation · 2003
Cited by 36
Aleksandar S. Dimovski · Theoretical Computer Science · 2014
Cited by 21Open access
Andrei Sabelfeld · 2000
Abstract The first part of the thesis investigates confidentiality, i.e. the problem of determining whether a given program (possibly received from an untrusted source) has secure information flow. We propose an extensional semanticsbased formal specification of secure information-flow properties in sequential and concurrent programs based on representing degrees of security by partial equivalence relations (pers). By making use of the machinery of powerdomain semantics, the approach is extended to handle nondeterminism and probabilistic covert channels for a small sequential language. The treatment of security for concurrent programs uses operational semantics and pers as probabilistic-bisimulation-like relations. We specify security for a small multi-threaded programming language with dynamic thread creation and generalise the security condition in order to define robust security with respect to a wide class of schedulers and program-controlled thread priorities. For both denotational and operational approaches, the usefulness of the compositional nature of the security specifications is illustrated by straightforward correctness proofs for simple type-based security analyses.
Cited by 0
Shangqing Liu · 2022
I was the corresponding author. I was responsible for co-designing the methodology, writing most of the code, drafting the manuscript and conducting the majority of the experiments. At the time of ending my Ph.D study, I would like to express my sincere gratitude and appreciation to anyone who
Cited by 0Open access