Aus der Einleitung: „The Guarded Fragment of first-order logic, introduced by Andréka, van Benthem, and Németi, has been a succesful attempt to transfer many good properties of modal, temporal, and description logics to a larger fragment of predicate logic. Among these are decidability, the finite modal property, invariance under an appropriate variant of bisimulation, and other nice modal theoretic properties. ...”

Concurrent software has been widely utilizing in computer systems owing to the highly efficient computation. However, testing and verifying concurrent software remain challenging tasks. This matter is not only because of the non-deterministic thread interferences which are hard to reason about but also because of the large state space due to the simultaneous path and interleaving explosions. That is, the number of program paths in each thread may be exponential in the number of branch conditions, and also, the number of thread interleavings may be exponential in the number of concurrent operations. This dissertation presents a set of new methods, built upon symbolic execution, a program analysis technique that systematically explores program state space, for testing concurrent programs. By modeling both functional and non-functional properties of the programs as assertions, these new methods efficiently analyze the viable behaviors of the given concurrent programs. The first method is assertion guided symbolic execution, a state space reduction technique that identifies and eliminates redundant executions w.r.t the explored interleavings. The second method is incremental symbolic execution, which generates test inputs only for the influenced program behaviors by the small code changes between two program versions. The third method is SYMPLC, a technique with domain-specific reduction strategies for generating tests for the multitasking Programmable Logic Controller (PLC) programs written in languages specified by the IEC 61131-3 standard. The last method is adversarial symbolic execution, a technique for detecting concurrency related side-channel information leaks by analyzing the cache timing behaviors of a concurrent program in symbolic execution. This dissertation evaluates the proposed methods on a diverse set of both synthesized programs and real-world applications. The experimental results show that these techniques can significantly outperform state-of-the-art symbolic execution tools for concurrent software. / Doctor of Philosophy / Software testing is a technique that runs software as a black-box on computer hardware multiple times, with different inputs per run, to test if the software behavior conforms to the designed functionality by developers. Nowadays, programmers have been increasingly developing multithreaded and multitasking software, e.g., web browser and web server, to utilize the highly efficient multiprocessor hardware. This approach significantly improves the software performance since a large computing job can now decompose to a set of small jobs which can then distribute to concurrently running threads (tasks). However, testing multithreaded (multitask) software is extremely challenging. The most critical problem is the inherent non-determinism. Typically, executing sequential software with the same input data always results in the same output. However, running a multithreaded (multitask) software multiple times, even under the same input data, may yield different output in each run. The root reason is that concurrent threads (tasks) may interleave their running progress at any time; thus the internal software execution order may be altered unexpectedly, causing runtime errors. Meanwhile, finding such faults is difficult, since the number of all possible interleavings can be exponentially growing in the number of concurrent thread (task) operations. This dissertation proposes four methods to test multithreaded/multitask software efficiently. The first method summarizes the already-tested program behaviors to avoid future testing runs that cannot lead to new faults. The second method only tests program behaviors that are impacted by program changes. The third method tests multitask Programmable Logic Controller (PLC) programs by excluding infeasible testing runs w.r.t the PLC semantics. The last method tests non-functional program properties by systematic concurrency analysis. This dissertation evaluates these methods upon a diverse set of benchmarks. The experimental results show that the proposed methods significantly outperform state-of-the-art techniques for concurrent software analysis.

Dans cette thèse, nous présentons une analyse syntaxique du vietnamien de Hô-Chi-Minh-Ville, dans la lignée de la syntaxe fonctionnelle mise en place par André Martinet et développée par la suite par ses continuateurs. Dans un premier temps, nous nous sommes intéressée au degré d’opposition verbo-nominal en vietnamien : nous proposons tout d’abord une synthèse des travaux menés à ce sujet, avant d’exposer notre analyse en classes, en nous appuyant sur des critères strictement syntaxiques. Une étude syntaxique détaillée des modalités (déterminants non déterminables) – les modalités nominalisantes, les modalités de degré, les modalités prédicatives et les modalités injonctives – a été nécessaire. Ces unités permettent de distinguer des comportements différents, et l’identification des grandes classes lexicales du vietnamien : nominaux, adjectifs, modaux et verbaux. Il apparait que ces classes d’unités s’organisent en un continuum, avec à un pôle les nominaux, à l’autre les verbaux. Dans un second temps, l’analyse porte sur les différents types de structures prédicatives du vietnamien. La variété des constructions – nucléaires et connectives – est au centre de l’étude, ainsi que l’identification des différentes fonctions. Enfin, nous exposons une analyse des “séries verbales”, phénomène très courant en vietnamien, mais décrivant en fait des réalités très diverses. Tout au long de l’analyse, nous accordons une importance particulière à la variation et aux zones de changements (réanalyses, lexicalisations, grammaticalisations), faisant état de la dynamique des différentes structures et de la langue elle-même. / We present here a syntaxic analysis of the Vietnamese language spoken in Ho Chi Minh City, in line with the functional syntax introduced by André Martinet and developed later by his followers. In a first part, we examined the extent of noun/verb opposition in Vietnamese. After a synthesis of work on this subject, we present our own analysis of the lexical classes, relying on strictly syntactic criteria. A detailed study of the syntactic modalités (undeterminable determinants) - nominalizing undeterminable determinants, undeterminable determinants of degree, predicative undeterminable determinants and injunctive undeterminable determinants - was necessary. These units are used to distinguish different behaviors, and leads to the identification of major lexical classes in Vietnamese: nominals, adjectives, modals and ‘verbals’. It appears that these classes of units are organized along a continuum. In a second part, the analysis focuses on the different types of predicative structures in Vietnamese. The variety of structures - nuclear and connective - is central to the study as well as the identification of the different functions. Finally, we present an analysis of "serial verb constructions" very common in Vietnamese, but actually reflecting very different realities. Throughout this study, we pay particular attention to the variation and change (reanalysis, lexicalizations, grammaticalizations), referring to the dynamics of the various structures and of the Vietnamese language itself.

A presente dissertação tem por objetivo geral analisar como a estrutura de construções que apresentam predicação complexa (PC) no Português Brasileiro (PB) é representada pela perspectiva tradicional e pela perspectiva gerativa, de modo a verificar a existência de padrões nessas construções. Neste trabalho, entendemos por PC a atribuição de propriedades a um mesmo constituinte por predicados diferentes. No primeiro capítulo, apresentamos a representação dessas estruturas à luz da abordagem tradicional, em que são tratadas como predicados verbo-nominais ou como orações reduzidas de infinitivo, particípio e de gerúndio. Nesse capítulo, também discutimos a ambiguidade entre predicativo do objeto e adjunto adnominal, assim como a possibilidade de predicativos do objeto indireto. No segundo capítulo, apresentamos a análise segundo a perspectiva gerativa, mais precisamente, de acordo com a Teoria de Princípios e Parâmetros, em que essas construções não são representadas como orações propriamente ditas, mas sim como small clauses (SCs). Ainda nesse capítulo, revisamos a proposta de Williams (1983, 1994) sobre as SCs e propomos que a projeção da SC seja dominada por AgrP. No terceiro capítulo, a partir da revisão das abordagens tradicional e gerativa, concluímos este trabalho com o estabelecimento de 18 possibilidades de estruturas com PC no PB. / This dissertation aims to analyze how the structure of constructions which present complex predication (CP) in Brazilian Portuguese (BP) is represented by the traditional perspective and by the generative perspective, in order to verify the existence of patterns of these constructions. In this study, CP is understood as the attribution of properties to a same constituent by different predicates. In the first chapter, we present how these structures are represented by the traditional approach, which treats them as noun-verb predicates or as reduced clauses of infinitive, participle and gerund. This chapter also discusses the ambiguity between object predicative and noun phrases, as well as the possibility of indirect object predicatives. In the second chapter, we present an analysis according to the generative perspective, particularly according to the Theory of Principles and Parameters, in which these constructions are not represented as clauses, but rather as small clauses (SCs). Also in this chapter, we revise Williams’ (1983, 1994) proposal on SCs and propose that the projection of the SC is ruled by AgrP. In the third chapter, based on the revision of traditional and generative approaches, we conclude this dissertation with the establishment of 18 possibilities of structures with CP in BP.

A presente dissertação tem por objetivo geral analisar como a estrutura de construções que apresentam predicação complexa (PC) no Português Brasileiro (PB) é representada pela perspectiva tradicional e pela perspectiva gerativa, de modo a verificar a existência de padrões nessas construções. Neste trabalho, entendemos por PC a atribuição de propriedades a um mesmo constituinte por predicados diferentes. No primeiro capítulo, apresentamos a representação dessas estruturas à luz da abordagem tradicional, em que são tratadas como predicados verbo-nominais ou como orações reduzidas de infinitivo, particípio e de gerúndio. Nesse capítulo, também discutimos a ambiguidade entre predicativo do objeto e adjunto adnominal, assim como a possibilidade de predicativos do objeto indireto. No segundo capítulo, apresentamos a análise segundo a perspectiva gerativa, mais precisamente, de acordo com a Teoria de Princípios e Parâmetros, em que essas construções não são representadas como orações propriamente ditas, mas sim como small clauses (SCs). Ainda nesse capítulo, revisamos a proposta de Williams (1983, 1994) sobre as SCs e propomos que a projeção da SC seja dominada por AgrP. No terceiro capítulo, a partir da revisão das abordagens tradicional e gerativa, concluímos este trabalho com o estabelecimento de 18 possibilidades de estruturas com PC no PB. / This dissertation aims to analyze how the structure of constructions which present complex predication (CP) in Brazilian Portuguese (BP) is represented by the traditional perspective and by the generative perspective, in order to verify the existence of patterns of these constructions. In this study, CP is understood as the attribution of properties to a same constituent by different predicates. In the first chapter, we present how these structures are represented by the traditional approach, which treats them as noun-verb predicates or as reduced clauses of infinitive, participle and gerund. This chapter also discusses the ambiguity between object predicative and noun phrases, as well as the possibility of indirect object predicatives. In the second chapter, we present an analysis according to the generative perspective, particularly according to the Theory of Principles and Parameters, in which these constructions are not represented as clauses, but rather as small clauses (SCs). Also in this chapter, we revise Williams’ (1983, 1994) proposal on SCs and propose that the projection of the SC is ruled by AgrP. In the third chapter, based on the revision of traditional and generative approaches, we conclude this dissertation with the establishment of 18 possibilities of structures with CP in BP.

Cette thèse étudie le fonctionnement des déterminations définie et indéfinie au sein des syntagmes nominaux génériques en anglais contemporain à partir d’un corpus essentiellement composé de textes encyclopédiques et scientifiques. La catégorisation générique peut relever de processus cognitifs et de niveaux d’abstraction distincts signifiés par les déterminations définie et indéfinie. La première partie décrit successivement le cadre référentiel de cette étude, la formalisation morphosyntaxique de la généricité nominale, la spécification dont sont porteurs les articles définis et indéfinis, ainsi que les contraintes déterminatives liées à la classe lexico-grammaticale des substantifs et au contexte prédicatif. La deuxième partie étudie les possibilités et impossibilités déterminatives au regard des contextes prédicatifs lorsque le syntagme nominal est associé à un prédicat d’espèce. Nous considérons plus spécifiquement l’interaction entre la classification des espèces, le nombre singulier ou pluriel et la détermination définie ou indéfinie en nous intéressant aux espèces conçues dans leur pluralité interne. La troisième partie examine le fonctionnement de l’article défini comme opérateur d’abstraction. L’étude des spécialisations de the montre qu’il est lié à une visée référentielle externalisante et synthétique. La quatrième partie traite du fonctionnement des syntagmes nominaux génériques définis et indéfinis au sein des textes génériques eu égard à la structuration du discours. L’article défini sous-tend une dimension anaphorique au générique également, et reste la marque de la saillance cognitive du référent. / This dissertation deals with the use of definite and indefinite determiners in generic noun phrases in contemporary English, using a corpus based on encyclopedic and scientific texts mainly. The categorization which genericity is based on results from various cognitive processes and levels of abstraction which are signified in the use of definite and indefinite determiners. The first part successively describes the referential framework of our study, the morphosyntactical forms of generic noun phrases, the values of definite and indefinite articles, as well as the pattern of constraints on definite and indefinite articles established by the lexico-grammatical features of nouns and the predicative context. The second part examines determiner possibilities and impossibilities with regard to the predicative context when a generic noun phrase is combined with a kind-predicate. More specifically, we correlate species classification, singular/plural number marking and definite/indefinite determination as we examine the plural structure of generic referents. The third part studies the use of the definite article as an abstraction operator. As we consider cases in which the use of definite noun phrases is favored, we show that its reference involves an externalizing and synthetic dimension. The fourth part deals with the way generic definite and indefinite noun phrases combine in generic texts with regard to the discourse structure. The use of the definite article presupposes an anaphoric dimension in generic reference also and indicates that the referent is salient in a cognitive perspective.

This thesis deals with verb-noun predicate with a light verb which occur in the European legislative texts. The first, theoretical part is divided into two chapters. The first one focuses on the predicate and the other covers the linguistic particularities of the legal documents. The other, research part is focused on the detailed analysis of selected verb-noun predicates which are found in the corpus of the European Union legislative texts. In conclusion, a small French-Czech dictionary of the investigated verb-noun predicates is attached.

A presente dissertação tem por objetivo geral analisar como a estrutura de construções que apresentam predicação complexa (PC) no Português Brasileiro (PB) é representada pela perspectiva tradicional e pela perspectiva gerativa, de modo a verificar a existência de padrões nessas construções. Neste trabalho, entendemos por PC a atribuição de propriedades a um mesmo constituinte por predicados diferentes. No primeiro capítulo, apresentamos a representação dessas estruturas à luz da abordagem tradicional, em que são tratadas como predicados verbo-nominais ou como orações reduzidas de infinitivo, particípio e de gerúndio. Nesse capítulo, também discutimos a ambiguidade entre predicativo do objeto e adjunto adnominal, assim como a possibilidade de predicativos do objeto indireto. No segundo capítulo, apresentamos a análise segundo a perspectiva gerativa, mais precisamente, de acordo com a Teoria de Princípios e Parâmetros, em que essas construções não são representadas como orações propriamente ditas, mas sim como small clauses (SCs). Ainda nesse capítulo, revisamos a proposta de Williams (1983, 1994) sobre as SCs e propomos que a projeção da SC seja dominada por AgrP. No terceiro capítulo, a partir da revisão das abordagens tradicional e gerativa, concluímos este trabalho com o estabelecimento de 18 possibilidades de estruturas com PC no PB. / This dissertation aims to analyze how the structure of constructions which present complex predication (CP) in Brazilian Portuguese (BP) is represented by the traditional perspective and by the generative perspective, in order to verify the existence of patterns of these constructions. In this study, CP is understood as the attribution of properties to a same constituent by different predicates. In the first chapter, we present how these structures are represented by the traditional approach, which treats them as noun-verb predicates or as reduced clauses of infinitive, participle and gerund. This chapter also discusses the ambiguity between object predicative and noun phrases, as well as the possibility of indirect object predicatives. In the second chapter, we present an analysis according to the generative perspective, particularly according to the Theory of Principles and Parameters, in which these constructions are not represented as clauses, but rather as small clauses (SCs). Also in this chapter, we revise Williams’ (1983, 1994) proposal on SCs and propose that the projection of the SC is ruled by AgrP. In the third chapter, based on the revision of traditional and generative approaches, we conclude this dissertation with the establishment of 18 possibilities of structures with CP in BP.

Le point de départ de cette thèse est la classe « P » (« verbes psychologiques ») du dictionnaire électronique Les Verbes français de J. Dubois et F. Dubois-Charlier, et porte plus précisément sur les verbes de sentiment. Les critères de cette classification n’étant pas toujours explicites, l’objectif est, dans un premier temps, d’en comprendre les paramètres syntactico sémantiques puis de l'affiner afin d'obtenir des classes plus petites, mais homogènes du point de vue du sentiment exprimé, et d’y intégrer les noms et / ou adjectifs morphologiquement apparentés aux verbes et partageant les mêmes propriétés syntactico-sémantique. Nos analyses, appuyées sur un corpus d’énoncés attestés, aboutissent à la caractérisation des prédicats de « nostalgie », de « regret »,de « dés)agrément » et d’« étonnement ». / The starting point of this work is “P” class (“verbes psychologiques”) of Les Verbes françaisof J. Dubois and F. Dubois-Charlier's electronic dictionary. It deals, more precisely, with feeling verbs.Because of the classification's criterions which are not that explicit, our main target is to try tounderstand their syntactic and semantic parameters, then to refine it in order to make small classes,but sharing in common the feeling expressed. Nouns and / or adjectives, morphologically connectedto verbs, and sharing the same syntactic and semantic properties, will be integrated to them. Ouranalysis, based on a large attested Corpus, lead to predicates characterization of “nostalgia”, “regret”,“annoyance” and “astonishment”.

The diploma thesis deals with the distinction of attributive and predicative adjectives in contemporary Czech. Although this distinction is very important for defining adjectives as a word class in many languages, there was only little attention paid to it in Czech so far. This thesis is based on the work of František Čermák Lexikon a sémantika (2010). It is strongly inspired by english tradition of linguistics, which is also a reason, why he introduces a new term predicative adjectives in Czech. The thesis is divided into two parts. The first part contains theoretical description of predicative and attributive function of adjectives. It is based on information contained in czech and foreign grammarbooks, handbooks or research papers. The goal is to summarize these separate information. The theoretical part deals with the basic characteristic of both types of adjectives, it focuses also on description of their semantics, word form and valency, which depends on it. This part contains definitions of some questionable points or inaccuracies of these descriptions too. The second part of this thesis is given to corpus research. The questionable points or inaccuracies of the descriptions defined in the first part of this thesis are examined on the material of Czech national corpus, concretely the corpus SYN2010....