Global ETD Search

1	Logics of domains Zhang, Guo Qiang January 1989 (has links) No description available. 005 Semantics of programming languages
2	The semantic analysis of advanced programming languages Eades, Harley D., III 01 July 2014 (has links) We live in a time where computing devices power essential systems of our society: our automobiles, our airplanes and even our medical services. In these safety-critical systems, bugs do not just cost money to fix; they have a potential to cause harm, even death. Therefore, software correctness is of paramount importance. Existing mainstream programming languages do not support software verification as part of their design, but rely on testing, and thus cannot completely rule out the possibility of bugs during software development. To fix this problem we must reshape the very foundation on which programming languages are based. Programming languages must support the ability to verify the correctness of the software developed in them, and this software verification must be possible using the same language the software is developed in. In the first half of this dissertation we introduce three new programming languages: Freedom of Speech, Separation of Proof from Program, and Dualized Type Theory. The Freedom of Speech language separates a logical fragment from of a general recursive programming language, but still allowing for the types of the logical fragment to depend on general recursive programs while maintaining logical consistency. Thus, obtaining the ability to verify properties of general recursion programs. Separation of Proof from Program builds on the Freedom of Speech languageby relieving several restrictions, and adding a number of extensions. Finally, Dualized Type Theory is a terminating functional programming language rich in constructive duality, and shows promise of being a logical foundation of induction and coninduction. These languages have the ability to verify properties of software, but how can we trust this verification? To be able to put our trust in these languages requires that the language be rigorously and mathematically defined so that the programming language itself can be studied as a mathematical object. Then we must show one very important property, logical consistency of the fragment of the programming language used to verify mathematical properties of the software. In the second half of this dissertation we introduce a well-known proof technique for showing logical consistency called hereditary substitution. Hereditary substitution shows promise of being less complex than existing proof techniques like the Tait-Girard Reducibility method. However, we are unsure which programming languages can be proved terminating using hereditary substitution. Our contribution to this line of work is the application of the hereditary substitution technique to predicative polymorphic programming languages, and the first proof of termination using hereditary substitution for a classical type theory. Dependent Types Dualized Logic Hereditary Substitution Programming Languages Semantics of Programming Languages Type Theory Computer Sciences
3	A Quest for Exactness: Program Transformation for Reliable Real Numbers Neron, Pierre 04 October 2013 (has links) (PDF) Cette thèse présente un algorithme qui élimine les racines carrées et les divi- sions dans des programmes sans boucles, utilisés dans des systèmes embarqués, tout en préservant la sémantique. L'élimination de ces opérations permet d'éviter les erreurs d'arrondis à l'exécution, ces erreurs d'arrondis pouvant entraîner un comportement complètement inattendu de la part du programme. Cette trans- formation respecte les contraintes du code embarqué, en particulier la nécessité pour le programme produit de s'exécuter en mémoire fixe. Cette transformation utilise deux algorithmes fondamentaux développés dans cette thèse. Le premier permet d'éliminer les racines carrées et les divisions des expressions booléennes contenant des comparaisons d'expressions arithmétiques. Le second est un algo- rithme qui résout un problème d'anti-unification particulier, que nous appelons anti-unification contrainte. Cette transformation de programme est définie et prou- vée dans l'assistant de preuves PVS. Elle est aussi implantée comme une stratégie de ce système. L'anti-unification contrainte est aussi utilisée pour étendre la transformation à des programmes contenant des fonctions. Elle permet ainsi d'éliminer les racines carrées et les divisions de spécifications écrites en PVS. La robustesse de cette méthode est mise en valeur par un exemple conséquent: l'élimination des racines carrées et des divisions dans un programme de détection des conflits aériens. Program Transformation Real Number arithmetic Anti-unification Semantics of Programming Languages Proof Assistant Embedded Systems Quantifier Elimination
4	AspectKE: Security aspects with program analysis for distributed systems Fan, Yang, Masuhara, Hidehiko, Aotani, Tomoyuki, Nielson, Flemming, Nielson, Hanne Riis* January 2010 (has links) Enforcing security policies to distributed systems is difficult, in particular, when a system contains untrusted components. We designed AspectKE, a distributed AOP language based on a tuple space, to tackle this issue. In AspectKE, aspects can enforce access control policies that depend on future behavior of running processes. One of the key language features is the predicates and functions that extract results of static program analysis, which are useful for defining security aspects that have to know about future behavior of a program. AspectKE* also provides a novel variable binding mechanism for pointcuts, so that pointcuts can uniformly specify join points based on both static and dynamic information about the program. Our implementation strategy performs fundamental static analysis at load-time, so as to retain runtime overheads minimal. We implemented a compiler for AspectKE, and demonstrate usefulness of AspectKE through a security aspect for a distributed chat system. aspect oriented programming program analysis security policies distributed systems tuple spaces Data processing Computer science Language Constructs and Features (E.2) Abstract data types Classes and objects (NEW) Concurrent programming structures Constraints (NEW) Control structures Coroutines Data types and structures Dynamic storage management Frameworks (NEW) Inheritance (NEW) Input/output Modules, packages Patterns (NEW) Polymorphism (NEW) Procedures, functions, and subroutines Recursion Security and Protection (K.6.5) Access controls Authentication Cryptographic controls Information flow controls Security kernels Verification Algebraic approaches to semantics Denotational semantics Operational semantics Partial evaluation (NEW) Process models (NEW) Program analysis (NEW)

1

Page generated in 0.1173 seconds