Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS. 2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovaný program je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab- straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonáva komponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýto solver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbu nových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a teda zmenšuje program analyzátora.

No description available.

Mit der aktuellen Überarbeitung der Sprache SDL (Specification and Description Language) der ITU-T wurde die semantische Fundierung der formalen Definition dieser Sprache vollständig überarbeitet; die formale Definition basiert nun auf dem Kalkül der Abstract State Machines (ASMs). Ebenfalls neu definiert wurde das um objekt-orientierte Konzepte erweiterte Datentypsystem. Damit musste eine formale semantische Fundierung für diese neuen Konzepte gefunden werden. Der bisher verwendete Kalkül ACT.ONE sollte nicht mehr verwendet werden, da er schwer verwendbar, nicht implementierbar und nicht auf Objektsysteme erweiterbar ist. In der vorliegenden Arbeit werden die Prinzipien einer formalen Sprachdefinition dargelegt und die Umsetzung dieser Prinzipien für die Sprache SDL-2000 vorgestellt. Dabei wird erläutert, dass eine konsistente Sprachdefinition nur dadurch erreicht werden konnte, dass die Definition der formalen Semantik der Sprache parallel mit der Entwicklung der informalen Definition erfolgte. Dabei deckt die formale Sprachdefinition alle Aspekte der Sprache ab: Syn-tax, statische Semantik und dynamische Semantik. Am Beispiel der Datentypsemantik wird erläutert, wie jeder dieser Aspekte informal beschrieben und dann formalisiert wurde. Von zentraler Rolle für die Anwendbarkeit der formalen Semantikdefinition in der Praxis ist der Einsatz von Werkzeugen. Die Arbeit erläutert, wie aus der formalen Sprachdefinition voll-automatisch ein Werkzeug generiert wurde, das die Sprache SDL implementiert, und wie die durch die Umsetzung der formalen Semantikdefinition in ein Werkzeug Fehler in dieser Definition aufgedeckt und behoben werden konnten. / With the latest revision of ITU-T SDL (Specification and Description Language), the semantic foundations of the formal language definition were completely revised; the formal definition is now based on the calculus of Abstract State Machines (ASMs). In addition, the data type system of SDL was revised, as object-oriented concepts were added. As a result, a new semantical foundation for these new concepts had to be defined. The ACT.ONE calculus that had been used so far was not suitable as a foundation any more, as it is hard to use, unimplementable and not extensible for the object oriented features. In this thesis, we elaborate the principles of a formal language definition, and the realisation of these principles in SDL-2000. We explains that a consistent language definition can only be achieved by developing the formal semantics definition in parallel with the development of the informal definition. The formal language definition covers all aspects of the language: syntax, static semantics, and dynamic semantics. Using the data type semantics as an example, we show how each of these aspects is informally described, and then formalized. For the applicability of the formal semantics definition for practitioners, usage of tools plays a central role. We explain how we transform the formal language definition fully automatically into a tool that implements the language SDL. We also explain how creating the tool allowed us to uncover and correct errors in the informal definition.

Denna uppsats har som syfte att utforska människors upplevelse av skyldigheter mot dem själva. Anser de attdet finns sådana, vad är de i så fall och känns dem? Genom en webbaserad enkät och elva semi-struktureradeintervjuer utforskas detta ämne. Resultatet visar att alla deltagare i intervjustudien anser att man harskyldigheter mot sig själv. Av det 229 svarande i enkätstudien tyckte 84,88 procent att man hade det. Vidarevisade resultatet att dessa skyldigheter främst innefattade postmateriella värderingar och uttryck som ”attvara sann mot sig själv” och ”att stå för sina åsikter” var förhärskande. Förutom detta fanns det också enkonflikt med andra då många av respondenterna i intervjustudien upplevde att de var skyldiga sig själva att”säga nej”. Till sist värderade respondenterna sin egen hälsa högt samt möjligheten att få uttrycka sin person / This paper aims to explore the human experience of obligations towards themselves. Do they believe thatthere are such? If so, what are they and how do they feel? Through a web-based survey and eleven semistructuredinterviews this topic has been explored. The result shows that all participants in the interviewstudy believes that it has obligations to themselves. Of the 229 respondents in the survey 84.88 percentresponded that they thought they had obligations towards themselves. Furthermore, the results showed thatthese obligations mainly comprised post-material values and expressions as "to be true to yourself" and "tostand up for your opinions" were prevalent. Besides this, there was also a conflict with others when many ofthe respondents in the interview study felt that they owed themselves to "say no". Finally, respondents ratedtheir own health as well as high opportunity to express their personality highly.

This dissertation shows that satisfiability procedures are abstract interpreters. This insight provides a unified view of program analysis and satisfiability solving and enables technology transfer between the two fields. The framework underlying these developments provides systematic recipes that show how intuition from satisfiability solvers can be lifted to program analyzers, how approximation techniques from program analyzers can be integrated into satisfiability procedures and how program analyzers and satisfiability solvers can be combined. Based on this work, we have developed new tools for checking program correctness and for solving satisfiability of quantifier-free first-order formulas. These tools outperform existing approaches. We introduce abstract satisfaction, an algebraic framework for applying abstract interpre- tation to obtain sound, but potentially incomplete satisfiability procedures. The framework allows the operation of satisfiability procedures to be understood in terms of fixed point computations involving deduction and abduction transformers on lattices. It also enables satisfiability solving and program correctness to be viewed as the same algebraic problem. Using abstract satisfaction, we show that a number of satisfiability procedures can be understood as abstract interpreters, including Boolean constraint propagation, the dpll and cdcl algorithms, St ̊almarck’s procedure, the dpll(t) framework and solvers based on congruence closure and the Bellman-Ford algorithm. Our work leads to a novel understand- ing of satisfiability architectures as refinement procedures for abstract analyses and allows us to relate these procedures to independent developments in program analysis. We use this perspective to develop Abstract Conflict-Driven Clause Learning (acdcl), a rigorous, lattice-based generalization of cdcl, the central algorithm of modern satisfiability research. The acdcl framework provides a solution to the open problem of lifting cdcl to new prob- lem domains and can be instantiated over many lattices that occur in practice. We provide soundness and completeness arguments for acdcl that apply to all such instantiations. We evaluate the effectiveness of acdcl by investigating two practical instantiations: fp-acdcl, a satisfiability procedure for the first-order theory of floating point arithmetic, and cdfpl, an interval-based program analyzer that uses cdcl-style learning to improve the precision of a program analysis. fp-acdcl is faster than competing approaches in 80% of our benchmarks and it is faster by more than an order of magnitude in 60% of the benchmarks. Out of 33 safe programs, cdfpl proves 16 more programs correct than a mature interval analysis tool and can conclusively determine the presence of errors in 24 unsafe benchmarks. Compared to bounded model checking, cdfpl is on average at least 260 times faster on our benchmark set.

This thesis describes methods for transforming applicative programs with the aim of improving their efficiency. The general justification for these techniques is presented via the concept of abstract interpretation. The work can be seen as providing mechanisms to optimise applicative programs for sequential von Neumann machines. The chapters address the following subjects. Chapter 1 gives an overview and gentle introduction to the following technical chapters. Chapter 2 gives an introduction to and motivation for the concept of abstract interpretation necessary for the detailed understanding of the rest of the work. It includes certain theoretical developments, of which I believe the most important is the incorporation of the concept of partial functions into our notion of abstract interpretation. This is done by associating non-standard denotations with functions just as denotational semantics gives the standard denotations. Chapter 3 gives an example of the ease with which we can talk about function objects within abstract interpretive schemes. It uses this to show how a simple language using call-by-need semantics can be augmented with a system that annotates places in a program at which call-by-value can be used without violating the call-by-need semantics. Chapter 4 extends the work of chapter 3 by showing that under some sequentiality restriction, the incorporation of call-by-value for call-by-need can be made complete in the sense that the resulting program will only possess strict functions except for the conditional. Chapter 5 is an attempt to apply the concepts of abstract interpretation to a completely different problem, that of incorporating destructive operators into an applicative program. We do this in order to increase the efficiency of implementation without violating the applicative semantics by introducing destructive operators into our language. Finally, chapter 6 contains a discussion of the implications of such techniques for real languages, and in particular presents arguments whereby applicative languages should be seen as whole systems and not merely the applicative subset of some larger language.

The purpose of this dissertation was to study how teachers and school leaders perceived a specific set of classroom math innovations, and how those innovations impacted instruction in relation to the Georgia Vision Project (GVP) standards and recommendations. This was a qualitative study conducted in two GVP districts. The participants in the study were five elementary teachers, two school administrators, and two district leaders. The participants were interviewed to gain an understanding of their perceptions of recent math innovations. The innovations included (a) math instruction using manipulatives (such as counting objects and puzzles) that utilize the Concrete Representational Abstract (CRA) model, which engages students to conceive from the concrete to the abstract; (b) differentiation through flexible student grouping; (c) information about how different subgroups of students learn mathematics; and (d) math professional learning. Previous research had focused on these innovations separately. However, no research study had grouped these innovations together to see how teachers perceived them within the context of a math classroom, and how teachers implemented them in their classrooms in order to increase student achievement. This qualitative case study included schoolteacher and educational leader interviews, observations, and artifacts. The two districts in the study were high performing in the area of mathematics. The results indicated that schoolteachers and educational leaders could not directly relate the math innovations to student success and, moreover, to the GVP standards and recommendations. During the study all GVP standards were analyzed at varying levels. The study primarily focused on the teaching and learning standard, which was a significant initiative for both districts. Both districts had varying levels of implementation concerning the innovations in the study: (a) use of manipulatives, (b) differentiation in classrooms, and (c) professional learning. All participants referenced the innovations as a part of their instruction, but could not directly relate the innovations beneficial to the success of the students.

This thesis examines the figurative work of Portuguese-born artist Maria Helena Vieira da Silva (1908-1992) completed between 1930 and 1946, in the cities of Paris, Lisbon and Rio de Janeiro. This thesis divests Vieira’s work of the persistent formalist framework from within which her artistic production has thus far been examined. Unlike any previous study, it explores the artist’s paintings through specific themes, subjects and forms of expression. By uncovering these narrative premises, we are able to re-assess the overall significance and contribution of Vieira’s pre-war work to her post-war oeuvre. Moreover, the interpretative framework that develops from this account re-draws Vieira’s position within the modernist canon; contrary to prevalently held views, her work ceases to be autonomous from its cultural field. The historical awareness embedded in the artist’s choice of subjects and themes captures the significance of the moment in history in which these paintings were completed. Yet, a contextual examination of Vieira's work in relation to the major streams of thought of the twentieth century reflects its elusive aesthetic nature. Each chapter examines specific themes and subjects. The first three chapters explore Vieira’s use of memory and the imagination through the expression of the child-like and the naïve, as ways to escape the mimesis of traditional painting. The introduction of these images alters the third person narrative quality of her work by bringing the artist’s perceptions to the forefront of her artistic production. The following three chapters explore Vieira’s subjective spatial quality, either through the use of linear formations of space, memory as projected on to urban landscapes, or simply by using her own image, in its numerous forms, as a spatial signifier. Moreover, in identifying Vieira’s choice of themes and forms of expression, this study observes the cross-roads of creativity that modernism inspired, disclosing the richness and plurality of sources involved in the production of painting, including literature, print-making and film.

Developing interactive web application systems requires a large amount of effort on designing database, system logic and user interface. These tasks are expensive and error-prone. Web application systems are accessed and used by many different sets of people with different backgrounds and numerous demands. Meeting these demands requires frequent updating for Web application systems which results in a very high cost process. Thus, many attempts have been made to automate, to some degree, the construction of Web user interfaces. Three main directions have been cited for this purpose. The first direction suggested of generating user interfaces from the application's data model. This path was able to generate the static layout of user interfaces with dynamic behaviour specified programmatically. The second tendency suggested deployment of the domain model to generate both, the layout of a user interface and its dynamic behaviour. Web applications built based on this approach are most useful for domain-specific interfaces with a relatively fixed user dialogue. The last direction adopted the notion of deploying database metadata to developing dynamic user interfaces. Although the notion was quite valuable, its deployment did not present a generic solution for generating a variety of types of dynamic Web user interface targeting several platforms and electronic devices. This thesis has inherited the latter direction and presented significant improvements on the current deployment of this tendency. This thesis aims to contribute towards the development of an abstract framework to generate abstract and dynamic Web user interfaces not targeted to any particular domain or platform. To achieve this target, the thesis proposed and evaluates a general notion for implementing a prototype system that uses an internal model (i.e. database metadata) in conjunction with XML technology. Database metadata is richer than any external model and provides the information needed to build dynamic user interfaces. In addition, XML technology became the mainstream of presenting and storing data in an abstract structure. It is widely adopted in Web development society because of its ability to be transformed into many different formats with a little bit of effort. This thesis finds that only Java can provide us with a generalised database metadata based framework. Other programming languages apply some restrictions on accessing and extracting database metadata from numerous database management systems. Consequently, JavaServlets and relational database were used to implement the proposed framework. In addition, Java Data Base Connectivity was used to bridge the two mentioned technologies. The implementation of our proposed approach shows that it is possible and very straightforward to produce different automatic and dynamic Web entry forms that not targeted at any platform. In addition, this approach can be applied to a particular domain without affecting the main notion or framework architecture. The implemented approach demonstrates a number of advantages over the other approaches based on external or internal models.

<P align="justify">Model-checking is an automated technique which aims at verifying properties of computer systems. A model-checker is fed with a model of the system (which capture all its possible behaviors) and a property to verify on this model. Both are given by a convenient mathematical formalism like, for instance, a transition system for the model and a temporal logic formula for the property.</P> <P align="justify">For several reasons (the model-checking is undecidable for this class of model or the model-checking needs too much resources for this model) model-checking may not be applicable. For safety properties (which basically says "nothing bad happen"), a solution to this problem uses a simpler model for which model-checkers might terminate without too much resources. This simpler model, called the abstract model, over-approximates the behaviors of the concrete model. However the abstract model might be too imprecise. In fact, if the property is true on the abstract model, the same holds on the concrete. On the contrary, when the abstract model violates the property, either the violation is reproducible on the concrete model and so we found an error; or it is not reproducible and so the model-checker is said to be inconclusive. Inconclusiveness stems from the over-approximation of the concrete model by the abstract model. So a precise model yields the model-checker to conclude, but precision comes generally with an increased computational cost.</P> <P align="justify">Recently, a lot of work has been done to define abstraction refinement algorithms. Those algorithms compute automatically abstract models which are refined as long as the model-checker is inconclusive. In the thesis, we give a new abstraction refinement algorithm which applies for safety properties. We compare our algorithm with previous attempts to build abstract models automatically and show, using formal proofs that our approach has several advantages. We also give several extensions of our algorithm which allow to integrate existing techniques used in model-checking such as acceleration techniques.</P> <P align="justify">Following a rigorous methodology we then instantiate our algorithm for a variety of models ranging from finite state transition systems to infinite state transition systems. For each of those models we prove the instantiated algorithm terminates and provide encouraging preliminary experimental results.</P> <br> <br> <P align="justify">Le model-checking est une technique automatisée qui vise à vérifier des propriétés sur des systèmes informatiques. Les données passées au model-checker sont le modèle du système (qui en capture tous les comportements possibles) et la propriété à vérifier. Les deux sont donnés dans un formalisme mathématique adéquat tel qu'un système de transition pour le modèle et une formule de logique temporelle pour la propriété.</P> <P align="justify">Pour diverses raisons (le model-checking est indécidable pour cette classe de modèle ou le model-checking nécessite trop de ressources pour ce modèle) le model-checking peut être inapplicable. Pour des propriétés de sûreté (qui disent dans l'ensemble "il ne se produit rien d'incorrect"), une solution à ce problème recourt à un modèle simplifié pour lequel le model-checker peut terminer sans trop de ressources. Ce modèle simplifié, appelé modèle abstrait, surapproxime les comportements du modèle concret. Le modèle abstrait peut cependant être trop imprécis. En effet, si la propriété est vraie sur le modèle abstrait alors elle l'est aussi sur le modèle concret. En revanche, lorsque le modèle abstrait enfreint la propriété : soit l'infraction peut être reproduite sur le modèle concret et alors nous avons trouvé une erreur ; soit l'infraction ne peut être reproduite et dans ce cas le model-checker est dit non conclusif. Ceci provient de la surapproximation du modèle concret faite par le modèle abstrait. Un modèle précis aboutit donc à un model-checking conclusif mais son coût augmente avec sa précision.</P> <P align="justify">Récemment, différents algorithmes d'abstraction raffinement ont été proposés. Ces algorithmes calculent automatiquement des modèles abstraits qui sont progressivement raffinés jusqu'à ce que leur model-checking soit conclusif. Dans la thèse, nous définissons un nouvel algorithme d'abstraction raffinement pour les propriétés de sûreté. Nous comparons notre algorithme avec les algorithmes d'abstraction raffinement antérieurs. A l'aide de preuves formelles, nous montrons les avantages de notre approche. Par ailleurs, nous définissons des extensions de l'algorithme qui intègrent d'autres techniques utilisées en model-checking comme les techniques d'accélérations.</P> <P align="justify">Suivant une méthodologie rigoureuse, nous instancions ensuite notre algorithme pour une variété de modèles allant des systèmes de transitions finis aux systèmes de transitions infinis. Pour chacun des modèles nous établissons la terminaison de l'algorithme instancié et donnons des résultats expérimentaux préliminaires encourageants.</P>