Global ETD Search

1	SoC Security Verification Using Assertion-Based and Information Flow Tracking Techniques Achyutha, Shanmukha Murali January 2021 (has links) No description available. Electrical Engineering SoC Assertion based verification information flow tracking system verilog assertions static verification security verification
2	Reasoning Tradeoffs in Implicit Invocation and Aspect Oriented Languages Sanchez Salazar, Jose 01 January 2015 (has links) To reason about a program means to state or conclude, by logical means, some properties the program exhibits; like its correctness according to certain expected behavior. The continuous need for more ambitious, more complex, and more dependable software systems demands for better mechanisms to modularize them and reason about their correctness. The reasoning process is affected by the design decisions made by the developer of the program and by the features supported by the programming language used. Beyond Object Orientation, Implicit Invocation and Aspect Oriented languages pose very hard reasoning challenges. Important tradeoffs must be considered while reasoning about a program: modular vs. non-modular reasoning, case-by-case analysis vs. abstraction, explicitness vs. implicitness; are some of them. By deciding a series of tradeoffs one can configure a reasoning scenario. For example if one decides for modular reasoning and explicit invocation a well-known object oriented reasoning scenario can be used. This dissertation identifies various important tradeoffs faced when reasoning about implicit invocation and aspect oriented programs, characterize scenarios derived from making choices regarding these tradeoffs, and provides sound proof rules for verification of programs covered by all these scenarios. Guidance for program developers and language designers is also given, so that reasoning about these types of programs becomes more tractable. Program reasoning static verification implicit invocation aspect orientation ptolemy language jml events Computer Sciences Engineering
3	Algorithmic Analysis of Name-Bounded Programs : From Java programs to Petri Nets via π-calculus Settenvini, Matteo January 2014 (has links) Context. Name-bounded analysis is a type of static analysis that allows us to take a concurrent program, abstract away from it, and check for some interesting properties, such as deadlock-freedom, or watching the propagation of variables across different components or layers of the system. Objectives. In this study we investigate the difficulties of giving a representation of computer programs in a name-bounded variation of π-calculus. Methods. A preliminary literature review is conducted to assess the presence (or lack thereof) of other successful translations from real-world programming languages to π-calculus, as well for the presence of relevant prior art in the modelling of concurrent systems. Results. This thesis gives a novel translation going from a relevant subset of the Java programming language, to its corresponding name-bounded π-calculus equivalent. In particular, the strengths of our translation are being able to dispose of names representing inactive objects when there are no circular references, and a transparent handling of polymorphism and dynamic method resolution. The resulting processes can then be further transformed into their Petri-Net representation, enabling us to check for important properties, such as reachability and coverability of program states. Conclusions. We conclude that some important properties that are not, in general, easy to check for concurrent programs, can be in fact be feasibly determined by giving a more constrained model in π-calculus first, and as Petri Nets afterwards. / +49 151 52966429 pi-calculus static verification static analysis concurrency petri nets name boundedness Information Systems Software Engineering Programvaruteknik
4	Zimní stadion v Olomouci / Winter Stadium in Olomouc Tomčíková, Lucie January 2020 (has links) The content of the bachelor thesis is static verification and the desing of two options of a roofing of the winter stadium in Olomouc. The object has a rectangular plan of dimension 68 x 100 m, the minimum clearance is given by requirements of the operation of winter sports. Steel construction is made of steel strength class S355. The calculations are made according to valid norms ČSN EN.
5	Zastřešení atletické haly / Roofing of Athletic Hall Potůčková, Simona Unknown Date (has links) The aim of this diploma thesis is a design of two versions of bearing roof construction of the athletic stadium in Brno and a smaller side roofing of changing rooms. The building has rectangular plan of dimension 67 x 102 m and the side construction has also rectangular plan of dimension 61x 8 m. The minimum height is given by requirements of various athletic sports. Material used for the main construction is steel strength class S355 and for the side construction it is steel strength class S235. All the calculations are according to valid norms ČSN EN.
6	Programování s přístupem Design by Contract na platformě .NET / Programming with Design by Contract Approach on .NET Platform Bohačiak, Ondrej January 2009 (has links) This paper aims to introduce programming using Design by Contract (DbC) approach, its principles and implementations in different environments. The motivation for the creation of this approach is discussed in the beginning and the DbC metaphor is explained, as well as its application to programming. The description of major elements of the contract in the context of routine interface follows afterwards. The subject matter of this paper is the analysis and comparison of individual programming systems for DbC development with the help of code samples. The benefits of using this approach and its role in the modern development process are evaluated in conclusion.
7	Provably Sound and Secure Automatic Proving and Generation of Verification Conditions / Tillförlitligt sund och säker automatisk generering och bevisning av verifieringsvillkor Lundberg, Didrik January 2018 (has links) Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. This thesis presents a proof procedure to efficiently generate a theorem stating the weakest precondition for a program to terminate successfully in a state upon which a certain postcondition is placed. Specifically, the Poly/ML implementation of the SML metalanguage is used to generate a theorem in the HOL4 interactive theorem prover regarding the properties of a program written in BIR, an abstract intermediate representation of machine code used in the PROSPER project. / Bevis av säkerhetsegenskaper hos program genom formell verifiering kan göras med hjälp av interaktiva teorembevisare. Det program som skall verifieras representeras i en mellanliggande språkrepresentation inuti den interaktiva teorembevisaren, varefter påståenden kan konstrueras, som sedan bevisas. Detta är en process som kan automatiseras i hög grad. Här presenterar vi en metod för att effektivt skapa och bevisa ett teorem som visar sundheten hos den svagaste förutsättningen för att ett program avslutas framgångsrikt under ett givet postvillkor. Specifikt använder vi Poly/ML-implementationen av SML för att generera ett teorem i den interaktiva teorembevisaren HOL4 som beskriver egenskaper hos ett program i BIR, en abstrakt mellanrepresentation av maskinkod som används i PROSPER-projektet. HOL4 HOL Higher-order logic SML Poly/ML Formal methods Axiomatic semantics Formal verification Static verification Program verification Hoare logic Floyd-Hoare logic ITP Interactive theorem prover Theorem prover Proof assistant BIR Automated theorem proving ATP Automated deduction Computer-assisted proof Automated reasoning Computer Sciences Datavetenskap (datalogi) Software Engineering Programvaruteknik

1

Page generated in 0.1549 seconds