As an accepted genre of female composition, song lies in a unique position among musical genres. This allows it to stand largely outside the area of Claude Steele’s notion of “stereotype threat,” and being absent such weighty pressures, it could then furnish an arena in which female composers can do their best work. As a genre that combines the arts of music and poetry, song is based upon a given set of symbols that provide the composer with inspiration. The study of these symbols and their possible metaphorical meanings can offer a guide to that inspiration. By studying two settings by male composers and two settings of female composers, we can compare their individual and gendered approach to those symbols for elements of a masculine or feminine style. Heinrich Heine’s 23rd poem in Die Heimkehr, analyzed thoroughly in Chapter 2, is the focal text in this study. In Chapters 3 through 6 each of the settings is examined at length using both a standard formal analysis and the “Grundgestalt” concept of Schoenberg. The settings examined are “Ihr Bild” by Franz Schubert, “Ich stand in dunkeln Träumen” and “Ihr Bildniss” (two versions of the same work) by Clara Schumann, “Ich stand in dunkeln Träumen” by Hugo Wolf, and a setting of the same name by Ingeborg von Bronsart. Each discussion focuses on the individual reactions to the specific symbols identified in Chapter 2, as well as the global approach to some well-known literary aspects of paternalistic literary culture of the time. The thesis concludes with a summary of the similarities and differences in the preceding four examinations. Chapter 7 also draws conclusions based on those contrasts, which yields an evaluation of gendered reactions and the possibility of a feminine style in the nineteenth century.

Compositional simulation is a complex task that involves solving several equations simultaneously for all grid blocks representing a petroleum reservoir. Usually, these equations are separated into two groups: primary and secondary equations. Similarly, the unknowns of the system are also separated into primary and secondary variables. Considering the large number of unknowns, there are many ways to separate such variables in order to deal with the primary variables. This work aims at comparing a number of formulations for compositional reservoir simulation. It also aims at enhancing the formulations with new features not provided in the original publications. To accomplish these objectives, various formulations prevailing in the literature are implemented in The University of Texas at Austin in-house fully implicit simulator named GPAS (General Purpose Adaptive Simulator) and their performances were compared. Subsequently, some of the formulations were enhanced and tested for various applications. The comparison of the formulations studied indicated differences in efficiency for each approach. These differences come from the fact that when one is solving for a different set of primary variables, the manipulation of the equations is analogous to the use of a preconditioner applied to a linear system of equations. Furthermore, unlike a preconditioner, changing the primary variables affects the non-linear solver. Therefore, differences in terms of the number of Newton-Raphson iterations, used for solution of nonlinear equations resulting from discretization of nonlinear partial differential equations representing fluid flow in the reservoir, are expected. In addition to these differences in the non-linear solver, many formulations explore the fact that a reduced number of equations need to be solved implicitly, thus considerably reducing the CPU time dedicated to the linear solver. Finally, new features not provided in the original published formulations such as three-phase flash calculation, physical dispersion, and unstructured grid were implemented and verified. Additionally, it was demonstrated that, in certain situations, these enhancements are essential to properly model the physical phenomena occurring in oil and gas reservoirs. / text

Multiple hydrocarbon phases are observed during miscible gas floods. The possible phases that result from a gas flood include a vapor phase, an oleic phase, a solvent-rich phase, a solid phase, and an aqueous phase. The solid phase primarily consists of aggregated asphaltene particles. Asphaltenes can block pore throats or change the formation wettability, and thereby reduce the hydrocarbon mobility. The dissolution of injected gas into the aqueous phase can also affect the gas flooding recovery because it reduces the amount of gas available to contact oil. This is more important in CO₂ flooding as the solubility of CO₂ in brine is much higher than hydrocarbons. In this research, we developed efficient and fast multi-phase equilibrium calculation algorithms to model phase behavior of asphaltenes and the aqueous phase in the compositional simulation of gas floods. The PC-SAFT equation of state is implemented in the UTCOMP simulator to model asphaltene precipitation. The additional computational time of PC-SAFT is substantially decreased by improving the root finding algorithm and calculating the derivatives analytically. A deposition and wettability alteration model is then integrated with the thermodynamic model to simulate dynamics of precipitated asphaltenes. Asphaltene deposition is shown to occur with pressure depletion around the production well and/or with gas injection in the reservoir domain that is swept by injected gas. It is observed that the profile of the damaged area by asphaltene deposition depends on the reservoir fluid. A general strategy is proposed to model the phase behavior of CO₂/hydrocarbon/water systems where four equilibrium phases exist. The developed four-phase reduced flash algorithm is used to investigate the effect of introducing water on the phase behavior of CO₂/hydrocarbon mixtures. The results show changes in the phase splits and saturation pressures by adding water to these CO₂/hydrocarbon systems. We used a reduced flash approach to reduce the additional computational time of the four-phase flash calculations,. The results show a significant speed-up in flash calculations using the reduced method. The computational advantage of the reduced method increases rapidly with the number of phases and components. We also decreased the computational time of the equilibrium calculations in UTCOMP by changing the sequential steps in the flash calculation where it checks the previous time-step results as the initial guess for the current time-step. The improved algorithm can skip a large number of flash calculation and stability analyses without loss of accuracy. / text

While evolutionary computation is well suited for automatic discovery in engineering, it can also be used to gain insight into how humans and organizations could perform more effectively. Using a real-world problem of innovation search in organizations as the motivating example, this dissertation formalizes human creative problem solving as competitive multi-agent search. It differs from existing single-agent and team-search problems in that the agents interact through knowledge of other agents' searches and through the dynamic changes in the search landscape caused by these searches. The main hypothesis is that evolutionary computation can be used to discover effective strategies for competitive multi-agent search. This hypothesis is verified in experiments using an abstract domain based on the NK model, i.e. partially correlated and tunably rugged fitness landscapes, and a concrete domain in the form of a social innovation game. In both domains, different specialized strategies are evolved for each different competitive environment, and also strategies that generalize across environments. Strategies evolved in the abstract domain are more effective and more complex than hand-designed strategies and one based on traditional tree search. Using a novel spherical visualization of the fitness landscapes of the abstract domain, insight is gained about how successful strategies work, e.g. by tracking positive changes in the landscape. In the concrete game domain, human players were modeled using backpropagation, and used as opponents to create environments for evolution. Evolved strategies scored significantly higher than the human models by using a different proportion of actions, providing insights into how performance could be improved in social innovation domains. The work thus provides a possible framework for studying various human creative activities as competitive multi-agent search in the future. / text

Concurrent systems are getting more complex with the advent of multi-core processors and the support of concurrent programs. However, errors of concurrent systems are too subtle to detect with the traditional testing and simulation. Model checking is an effective method to verify concurrent systems by exhaustively searching the complete state space exhibited by a system. However, the main challenge for model checking is state explosion, that is the state space of a concurrent system grows exponentially in the number of components of the system. The state space explosion problem prevents model checking from being applied to systems in realistic size. After decades of intensive research, a large number of methods have been developed to attack this well-known problem. Compositional verification is one of the promising methods that can be scalable to large complex concurrent systems. In compositional verification, the task of verifying an entire system is divided into smaller tasks of verifying each component of the system individually. The correctness of the properties on the entire system can be derived from the results from the local verification on individual components. This method avoids building up the global state space for the entire system, and accordingly alleviates the state space explosion problem. In order to facilitate the application of compositional verification, several issues need to be addressed. The generation of over-approximate and yet accurate environments for components for local verification is a major focus of the automated compositional verification. This dissertation addresses such issue by proposing two abstraction refinement methods that refine the state space of each component with an over-approximate environment iteratively. The basic idea of these two abstraction refinement methods is to examine the interface interactions among different components and remove the behaviors that are not allowed on the components' interfaces from their corresponding state space. After the extra behaviors introduced by the over-approximate environment are removed by the abstraction refinement methods, the initial coarse environments become more accurate. The difference between these two methods lies in the identification and removal of illegal behaviors generated by the over-approximate environments. For local properties that can be verified on individual components, compositional reasoning can be scaled to large systems by leveraging the proposed abstraction refinement methods. However, for global properties that cannot be checked locally, the state space of the whole system needs to be constructed. To alleviate the state explosion problem when generating the global state space by composing the local state space of the individual components, this dissertation also proposes several state space reduction techniques to simplify the state space of each component to help the compositional minimization method to generate a much smaller global state space for the entire system. These state space reduction techniques are sound and complete in that they keep all the behaviors on the interface but do not introduce any extra behaviors, therefore, the same verification results derived from the reduced global state space are also valid on the original state space for the entire system. An automated compositional verification framework integrated with all the abstraction refinement methods and the state space reduction techniques presented in this dissertation has been implemented in an explicit model checker Platu. It has been applied to experiments on several non-trivial asynchronous circuit designs to demonstrate its scalability. The experimental results show that our automated compositional verification framework is effective on these examples that are too complex for the monolithic model checking methods to handle.

In this thesis we present a study of the generation of abstract program models from programs in real-world programming languages that are employed in the formal verification of software. The thesis is divided into three parts, which cover distinct types of software systems, programming languages, verification scenarios, program models and properties.The first part presents an algorithm for the extraction of control flow graphs from sequential Java bytecode programs. The graphs are tailored for a compositional technique for the verification of temporal control flow safety properties. We prove that the extracted models soundly over-approximate the program behaviour w.r.t. sequences of method invocations and exceptions. Therefore, the properties that are established with the compositional technique over the control flow graphs also hold for the programs. We implement the algorithm as ConFlEx, and evaluate the tool on a number of test cases.The second part presents a technique to generate program models from incomplete software systems, i.e., programs where the implementation of at least one of the components is not available. We first define a framework to represent incomplete Java bytecode programs, and extend the algorithm presented in the first part to handle missing code. Then, we introduce refinement rules, i.e., conditions for instantiating the missing code, and prove that the rules preserve properties established over control flow graphs extracted from incomplete programs. We have extended ConFlEx to support the new definitions, and re-evaluate the tool, now over test cases of incomplete programs.The third part addresses the verification of multithreaded programs. We present a technique to prove the following property of synchronization with condition variables: "If every thread synchronizing under the same condition variables eventually enters its synchronization block, then every thread will eventually exit the synchronization". To support the verification, we first propose SyncTask, a simple intermediate language for specifying synchronized parallel computations. Then, we propose an annotation language for Java programs to assist the automatic extraction of SyncTask programs, and show that, for correctly annotated programs, the above-mentioned property holds if and only if the corresponding SyncTask program terminates. We reduce the termination problem into a reachability problem on Coloured Petri Nets. We define an algorithm to extract nets from SyncTask programs, and show that a program terminates if and only if its corresponding net always reaches a particular set of dead configurations. The extraction of SyncTask programs and their translation into Petri nets is implemented as the STaVe tool. We evaluate the technique by feeding annotated Java programs to STaVe, then verifying the extracted nets with a standard Coloured Petri Net analysis tool / Den här avhandlingen studerar automatisk konstruktion av abstrakta modeller för formell verifikation av program skrivna i verkliga programmeringsspråk. Avhandlingen består av tre delar som involverar olika typer av program, programmeringsspråk, verifikationsscenarier, programmodeller och egenskaper.Del ett presenterar en algoritm för generation av flödesgrafer från sekventiella program i Java bytekod. Graferna är skräddarsydda för en kompositionell teknik för verifikationen av temporala kontrollflödens säkerhetsegenskaper. Vi visar att de extraherade modellerna sunt överapproximerar programbeteenden med avseende på sekvenser av metodanrop och -undantag. Således gäller egenskaperna som kan fastställas genom kompositionstekniken över kontrollflöden även för programmen. Vi implementerar dessutom algoritmen i form av verktyget ConFlEx och utvärderar verktyget på ett antal testfall.Del två presenterar en teknik för att generera modeller av ofullständiga program. Det vill säga, program där implementationen av åtminstone en komponent inte är tillgänglig. Vi definierar ett ramverk för att representera ofullständiga Java bytekodsprogram och utökar algoritmen från del ett till att hantera ofullständig kod.  Därefter presenterar vi raffineringsregler - villkor för att instansiera den saknade koden - och bevisar att reglerna bevarar relevanta egenskaper av kontrollflödesgrafer. Vi har dessutom utökat ConFlEx till att stödja de nya definitionerna och har omvärderat verktyget på testfall av ofullständiga program.Del tre angriper verifikation av multitrådade program. Vi presenterar en teknik för att bevisa följande egenskap för synkronisering med vilkorsvariabler: "Om varje trådsynkronisering under samma villkor så småningom stiger in i sitt synkroniseringsblock så kommer varje tråd också till slut lämna synkroniseringen". För att stödja verifikationen så introducerar vi först SyncTask - ett enkelt mellanliggande språk för att specificera synkronisering av parallella beräkningar. Därefter presenterar vi ett annoteringsspråk för Java som tillåter automatisk extrahering av SyncTask-program och visar att egenskapen gäller om och endast om motsvarande SyncTask-program terminerar. Vi reducerar termineringsproblemet till ett nåbarhetsproblem på färgade Petrinät samt definierar en algoritm som skapar Petrinät från SyncTask-program där programmet terminerar om och endast om nätet alltid når en särskild mängd av döda konfigurationer. Extraktionen av SyncTask-program och deras motsvarande Petrinät är implementerade i form av verktyget STaVe.  Slutligen utvärderar vi verktyget genom att mata annoterade. / <p>QC 20151101</p>

Three compositional reservoir simulators have been developed in the Department of Petroleum and Geosystems Engineering at The University of Texas at Austin (UT-Austin): UTCOMP (miscible gas flooding simulator), UTCHEM (chemical flooding simulator), and GPAS (General Purpose Adaptive Simulator). UTCOMP and UTCHEM simulators have been used by various oil companies for solving a variety of field problems. The efficiency and accuracy of each simulator becomes critically important when they are used to solve field problems. In this study, two well-developed solver packages, SAMG and HYPRE, along with existing solvers were compared. Our numerical results showed that SAMG can be an excellent solver for the usage in the three simulators for solving problems with a high accuracy requirement and long simulation times, and BoomerAMG in HYPRE package can also be a good solver for application in the UTCHEM simulator. In order to investigate the flexibility and the efficiency of a partitioned coupling method, the second part of this thesis presents a new implementation using a partition method for a thermal module in an equation-of-state (EOS) compositional simulator, the General Purpose Adaptive Simulator (GPAS) developed at The University of Texas at Austin. The finite difference method (FDM) was used for the solution of governing partial differential equations. Specifically, the new coupled implementation was based on the Schur complement method. For the partition method, two suitable acceleration techniques were constructed. One technique was the optimized choice of preconditioner for the Schur complement; the other was the optimized selection of tolerances for the two solution steps. To validate the implementation, we present simulation examples of hot water injection in an oil reservoir. The numerical comparison between the new implementation and the traditional, fully implicit method showed that the partition method is not only more flexible, but also faster than the classical, fully implicit method for the same test problems without sacrificing accuracy. In conclusion, the new implementation of the partition method is a more flexible and more efficient method for coupling a new module into an existing simulator than the classical, fully implicit method.The third part of this thesis presents another type of coupling method, iterative coupling methods, which has been implemented into GPAS with thermal module, FICM (Fully, Iterative Coupling Method) and GICM (General, Iterative Coupling Method), LICM (Loose, Iterative Coupling Method). The results show that LICM is divergent, and GICM and FICM can work normally. GICM is the fastest among the compared methods, and FICM has a similar efficiency as CFIM (Classic Fully Implicit Method). Although GICM is the fastest method, GICM is less accurate than FICM for in the test cases carried out in this study. / text

As a result of the problem of hydrate in multiphase pipelines in offshore production is becoming more and more severe with the increasing of the water depth, the study on oil-gas-water-hydrate has became a hot point of multiphase flow. In this paper, the hydrate particle and liquid phase was treated as pseudo-fluid, the steady hydraulic, thermodynamical and phase equilibrium calculation method of gas-hydrate slurry was developed. Comparison was carried out between calculated data and experimental data from flow loop in our laboratory. With strict flash calculation the following items were determined: the amount of hydrate; phase number; the location that hydrate appeared; flowrate and molar component of gas phase and liquid phase. Then thermodynamic quantities were carried out with proper relational expression. When Compositional model is used to simulate two phase flow, it is required to couple mass, momentum, energy equation and equation of state. In the other word, the parameters in these four equations are interacted. However they are all the functions of p, T and z. In steady condition, it’s assumed that the composition of fluid is unchangeable along the pipeline and the flow can be described by pressure and temperature. In this paper, calculation method of gas-liquid two phase flow which respectively was improved. Liquid holdup and pressure drop were calculated by momentum equation. Enthalpy balance equation was substituted by explicit formulation of temperature calculation which meant that the loop of temperature was not required.

Kompozicinių medžiagų konstrukcijų taikymas aviacijoje didėja. Saugumui aviacijoje užtikrinti reikalingos patikimos kontrolės sistemos. Šiame darbe pateiktas ultragarso greičio matavimo metodo taikymas kompozicinėms struktūroms tirti. Metodas numato akustinių gardelių panaudojimą, sudarant ultragarso bangų sklidimo greičio matavimo kanalą tiriamame sluoksnyje. Šis metodas atitinka keliamus tikslumo, patikimumo ir operatyvumo reikalavimus. Darbo apimtis – 65 p. teksto be priedų, 44 iliustr., 3 lent., 16 bibliografiniai šaltiniai. / Usage of compositional materials in aviation increases. To ensure safety in aviation - reliable control systems are required. Method of examination of compositional materials using ultrasound measuring system is introduced in this work. This method implies usage of acoustic lattice for measurement of created ultrasound waves in examined layer. This method complies with requirements for accuracy, reliability and effectiveness.

Magistrinio darbo teorinėje dalyje nagrinėjama Lietuvos moderniosios architektūros ir vitražo tarpusavio ryšys, bei priklausomybė vienas nuo kito. Nuo XX a. 6-ojo dešimtmečio Lietuvoje užsimezgęs glaudus architektūros ir vitražo ryšys, kai vitražas tapo neatsiejama architektūros dalis, šiandieninėje visuomenėje yra visiškai pakitęs. Remiantis modeliuojamomis meninės raiškos priemonių atžvilgiu, darbe trumpai apžvelgiama architektūros ir vitražo raida nuo XX a. 6-ojo dešimtmečio iki šių dienų. Pateikta glausta apžvalga indentifikuoja vitražo priklausomybę nuo architektūrinių formų bei tendencingą jo kitimą priklausomai nuo vyrayjančių meno srovių šioje meno srityje. Tai pat pateikiami besikeičiančių meno srovių architektūros ir vitražų darbų pavyzdžiai Lietuvoje. Pagrindinę magistro teorinę dalį sudaro dvi architektūros ir vitražo simbiozės analizės, kurios nagrinėjamos formaliaja metodika. Pagrindiniu aspektu traktuojami kompoziciniai sprendimai ir jų poveikis bendrai meninei sąveikai. Analizuojami du visuomeninės paskirties architektūros objektai, kuriuose integruoti Lietuvos vitražistų stiklo darbai: Vilniaus Santuokų rūmų ir Eugenijaus Konstantino Šatūno stiklo darbai bei Nidos Švc. Mergelės Marijos krikščionių pagalbos bažnyčios ir Algirdo Dovydėno vitražai. Analizuojant dviejų meno šakų darnią simbiozę, dėmesys akcentuojamas į kompozicinę plastiką, jos tarpusavio panašumus ir skritumus, kurie turi įtakos lygiaverčiui architektūros ir vitražo užmegztam „pokalbiui“... [toliau žr. visą tekstą] / In the theoretical part of the work the main attention is put on the relation between modern Lithuanian architecture and stained glass. The work analyses how these two art forms influence and complement each other. From the 1950s stained glass became the integral part of architecture but nowadays this connection is completely changed. The main focus of the work is to show the evolution of architecture and stained glass from 1950s until today by analyzing formal elements, aesthetic principles and symbolic signs. The analysis represents stained glass dependence on architectural forms and dominant art tendencies. Various works of architecture and stained glass in Lithuania are also discussed as examples of these tendencies. The main theoretical part of the work is dedicated to analysis of symbiosis between architecture and stained glass from formal perspective. Firstly, the analysis deals with compositional solutions and their effect on general artistic interaction. The base of analysis are two buildings created for public use: Vilnius Santuokų rūmai and glass work by Konstantinas Šatūnas, Saint Mary Church in Nida and stained glass works by Algirdas Dovydėnas. Analysing the relation between two art forms, the emphasis is put on compositional expression, its differences and similiarities that influence the conversation between architecture and stained glass. The analysis is based not only on information found in specific literature and other sources but also on personal remarks... [to full text]