Spelling suggestions: "subject:"equational theory"" "subject:"equationals theory""
1 |
Reasoning About Multi-stage ProgramsInoue, Jun 24 July 2013 (has links)
Multi-stage programming (MSP) is a style of writing program
generators---programs which generate programs---supported by special
annotations that direct construction, combination, and execution of
object programs. Various researchers have shown MSP to be effective
in writing efficient programs without sacrificing genericity.
However, correctness proofs of such programs have so far received
limited attention, and approaches and challenges for that task have
been largely unexplored. In this thesis, I establish formal
equational properties of the multi-stage lambda calculus and related
proof techniques, as well as results that delineate the intricacies
of multi-stage languages that one must be aware of.
In particular, I settle three basic questions that naturally arise
when verifying multi-stage functional programs. Firstly, can adding
staging MSP to a language compromise the interchangeability of terms
that held in the original language? Unfortunately it can, and more
care is needed to reason about terms with free variables. Secondly,
staging annotations, as the term ``annotations'' suggests, are often
thought to be orthogonal to the behavior of a program, but when is
this formally guaranteed to be the case? I give termination
conditions that characterize when this guarantee holds. Finally, do
multi-stage languages satisfy extensional facts, for example that
functions agreeing on all arguments are equivalent? I develop a
sound and complete notion of applicative bisimulation, which can
establish not only extensionality but, in principle, any other valid
program equivalence as well. These results improve our general
understanding of staging and enable us to prove the correctness of
complicated multi-stage programs.
|
2 |
Reasoning About Staged ProgramsJanuary 2010 (has links)
This thesis establishes formal equational properties of multi-stage
calculi and related proof techniques that support analyses of staged
programs. A key promise of staging is to make programs efficient
without destroying clarity, thereby reducing the likelihood of bugs.
However, few publications rigorously verify that their staged
programs indeed behave as intended. In fact, little is known about
how staged programs can be verified, or what correctness issues
staging introduces. To solve this problem, I show a reduction of
the correctness of a staged program to that of an unstaged program.
This reduction not only clarifies the effects of staging on program
behavior but also eases verification, as unstaged programs are more
susceptible to existing reasoning techniques. I also demonstrate
that important single-stage reasoning techniques apply to staged
programs. These techniques are useful for establishing side
conditions for the reduction and for discovering or validating
further reasoning principles. / NSF grant CCF-0747431
|
3 |
Contraintes d'anti-filtrage et programmation par réécriture / Anti-matching constraints and programming with rewrite rulesKöpetz, Radu 15 October 2008 (has links)
L’objectif principal de cette thèse est l’étude et la formalisation de nouvelles constructions permettant d’augmenter l’expressivité du filtrage et des langages à base de règles en général. Ceci est motivé par le développement de Tom, un système qui enrichit les langages impératifs comme Java et C avec des constructions de haut niveau comme le filtrage et les stratégies. Une première extension que l’on propose est la notion d’anti-patterns, i.e. des motifs qui peuvent contenir des symboles de complément. Nous définissons de manière formelle la sémantique des anti-patterns dans le cas syntaxique et modulo une théorie équationnelle arbitraire. Puis nous étendons la notion classique de filtrage entre les motifs et les termes clos au filtrage entre les anti-patterns et les termes clos (anti-filtrage). Ensuite, nous proposons plusieurs extensions aux constructions de filtrage fournies par Tom. La condition pour l’application d’une règle devient une conjonction ou disjonction de contraintes de filtrage et d’anti-filtrage ainsi que d’autres types de conditions. Les techniques classiques de compilation du filtrage ne sont pas bien adaptées à ces conditions complexes. On propose donc une nouvelle méthode de compilation basée sur des systèmes de réécriture contrôlés par des stratégies. Nous avons complètement réécrit le compilateur de Tom en utilisant cette technique. Tous ces éléments rassemblés constituent un environnement pour décrire et implémenter des transformations de manière élégante et concise. Pour promouvoir son utilisation dans des projets à grand échelle, on développe une technique pour extraire automatiquement des informations structurelles à partir d’une hiérarchie de classes Java. Cela permet l’intégration du filtrage offert par Tom dans n’importe quelle application Java / The main objective of this thesis is the study of new constructs and formalisms that increase the expressivity of pattern matching and rule based languages in general. This is motivated by the development of Tom, a system that adds high level constructs such as pattern matching and strategies to languages like Java and C. A first extension that we propose is the notion of anti-patterns, i.e. patterns that may contain complement symbols. We define formally the semantics of anti-patterns both in the syntactic case and modulo an arbitrary equational theory. We then extend the classical notion of matching between patterns and ground terms to matching between anti-patterns and ground terms. We further propose several extensions to the matching constructs provided by Tom. Consequently, the condition for the application of a rule becomes a combination of matching and anti-matching constraints together with other types of conditions. Classical compilation techniques for pattern matching are not very well suited for these complex conditions. Therefore we propose a new compilation method based on rewrite systems controlled by strategies, which provides a high level of modularity. Tom’s compiler has been rewritten from scratch using this technique. All this constitutes a software environment for expressing transformations in a clear and concise way. To promote its use in large scale applications, we propose an approach for extracting automatically structural information from arbitrary Java hierarchies. This allows a seamless integration of Tom’s pattern matching facilities in any application
|
4 |
Advanced Features in Protocol Verification: Theory, Properties, and Efficiency in Maude-NPASantiago Pinazo, Sonia 31 March 2015 (has links)
The area of formal analysis of cryptographic protocols has been an active
one since the mid 80’s. The idea is to verify communication protocols
that use encryption to guarantee secrecy and that use authentication of
data to ensure security. Formal methods are used in protocol analysis to
provide formal proofs of security, and to uncover bugs and security flaws
that in some cases had remained unknown long after the original protocol
publication, such as the case of the well known Needham-Schroeder
Public Key (NSPK) protocol. In this thesis we tackle problems regarding
the three main pillars of protocol verification: modelling capabilities,
verifiable properties, and efficiency.
This thesis is devoted to investigate advanced features in the analysis
of cryptographic protocols tailored to the Maude-NPA tool. This tool
is a model-checker for cryptographic protocol analysis that allows for
the incorporation of different equational theories and operates in the
unbounded session model without the use of data or control abstraction.
An important contribution of this thesis is relative to theoretical aspects
of protocol verification in Maude-NPA. First, we define a forwards
operational semantics, using rewriting logic as the theoretical framework
and the Maude programming language as tool support. This is the first
time that a forwards rewriting-based semantics is given for Maude-NPA.
Second, we also study the problem that arises in cryptographic protocol
analysis when it is necessary to guarantee that certain terms generated
during a state exploration are in normal form with respect to the protocol
equational theory.
We also study techniques to extend Maude-NPA capabilities to support
the verification of a wider class of protocols and security properties.
First, we present a framework to specify and verify sequential protocol
compositions in which one or more child protocols make use of information obtained from running a parent protocol. Second, we present a
theoretical framework to specify and verify protocol indistinguishability
in Maude-NPA. This kind of properties aim to verify that an attacker
cannot distinguish between two versions of a protocol: for example, one
using one secret and one using another, as it happens in electronic voting
protocols.
Finally, this thesis contributes to improve the efficiency of protocol
verification in Maude-NPA. We define several techniques which drastically
reduce the state space, and can often yield a finite state space,
so that whether the desired security property holds or not can in fact
be decided automatically, in spite of the general undecidability of such
problems. / Santiago Pinazo, S. (2015). Advanced Features in Protocol Verification: Theory, Properties, and Efficiency in Maude-NPA [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/48527 / TESIS
|
Page generated in 0.0832 seconds