abstract: Assemblers and compilers provide feedback to a programmer in the form of error messages. These error messages become input to the debugging model of the programmer. For the programmer to fix an error, they should first locate the error in the program, understand what is causing that error, and finally resolve that error. Error messages play an important role in all three stages of fixing of errors. This thesis studies the effects of error messages in the context of teaching programming. Given an error message, this work investigates how it effects student’s way of 1) understanding the error, and 2) fixing the error. As part of the study, three error message types were developed – Default, Link and Example, to better understand the effects of error messages. The Default type provides an assembler-centric single line error message, the Link type provides a program-centric detailed error description with a hyperlink for more information, and the Example type provides a program centric detailed error description with a relevant example. All these error message types were developed for assembly language programming. A think aloud programming exercise was conducted as part of the study to capture the student programmer’s knowledge model. Different codes were developed to analyze the data collected as part of think aloud exercise. After transcribing, coding, and analyzing the data, it was found that the Link type of error message helped to fix the error in less time and with fewer steps. Among the three types, the Link type of error message also resulted in a significantly higher ratio of correct to incorrect steps taken by the programmer to fix the error. / Dissertation/Thesis / Masters Thesis Software Engineering 2017

Orientador: Nelson Luis Saldanha da Fonseca / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-13T20:11:45Z (GMT). No. of bitstreams: 1 Michel_NeilaFernanda_M.pdf: 1961141 bytes, checksum: f4470a332c9b5f764b7bd3b912c27db1 (MD5) Previous issue date: 2008 / Resumo: O protoloco TCP Reno começou a operar em 01 de Janeiro de 1983. Desde sua concepção, houveram expressivos avanços nas tecnologias de transmissão de dados, como a introdução de enlaces ópticos e de satélites, 'que permitem altas taxas de transmissão. O TCP Reno continua sendo o protocolo padrão na Internet. Entretanto existem inúmeras dificuldades na sua operação, que causam baixo desempenho em redes com produto banda-atraso elevado, devido ao mecanismo de atualização do tamanho da janela de congestionamento. Para superar suas deficiências, vários protocolos variantes do TCP Reno têm sido propostos com o objetivo de melhorar a utilização de recursos em redes de alta velocidade, e por esta razão são denominados "Protocolos para Redes de Alta Velocidade" . Para que as proposições de variantes do TCP levem a protocolos que operem eficientemente em redes com alto valor do produto banda-atraso, é necessário que se avalie quais variações da dinâmica do crescimento da janela de transmissão são efetivas. Nesta dissertação avalia-se um conjunto de protocolos variantes do TCP para redes de alta velocidade através de simulações. Diversas propriedades importantes para protocolos do tipo TCP são investigadas / Abstract: The importance of the Reno TCP protocol started operating in January 01 st, 1983. Since this milestone, there were expressive advances on data transmission technologies, such as those of optical fibers and satellite channels which allow high transmission rates on long distances. Reno TCP remains the Internet standard protocol. However, its operation presents several dificulties in networks with high bandwidth-delay product, producing poor performance due its window congestion mechanism. In order to overcome its deficiencies, several variants have been proposed with the aim of enhancing its utilization in high speed networks. These variants are generally called "High Speed Networks Protocols". Transmission chàracteristics, properties and performance evaluation are essencial to the identification of problems and avoidance of poor performance. In this dissertation a set of TCP variants protocols for high speed networks is evaluated. Several important properties of these protocols are investigated / Mestrado / Redes de Computadores / Mestre em Ciência da Computação

The area of formal analysis of cryptographic protocols has been an active one since the mid 80’s. The idea is to verify communication protocols that use encryption to guarantee secrecy and that use authentication of data to ensure security. Formal methods are used in protocol analysis to provide formal proofs of security, and to uncover bugs and security flaws that in some cases had remained unknown long after the original protocol publication, such as the case of the well known Needham-Schroeder Public Key (NSPK) protocol. In this thesis we tackle problems regarding the three main pillars of protocol verification: modelling capabilities, verifiable properties, and efficiency. This thesis is devoted to investigate advanced features in the analysis of cryptographic protocols tailored to the Maude-NPA tool. This tool is a model-checker for cryptographic protocol analysis that allows for the incorporation of different equational theories and operates in the unbounded session model without the use of data or control abstraction. An important contribution of this thesis is relative to theoretical aspects of protocol verification in Maude-NPA. First, we define a forwards operational semantics, using rewriting logic as the theoretical framework and the Maude programming language as tool support. This is the first time that a forwards rewriting-based semantics is given for Maude-NPA. Second, we also study the problem that arises in cryptographic protocol analysis when it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the protocol equational theory. We also study techniques to extend Maude-NPA capabilities to support the verification of a wider class of protocols and security properties. First, we present a framework to specify and verify sequential protocol compositions in which one or more child protocols make use of information obtained from running a parent protocol. Second, we present a theoretical framework to specify and verify protocol indistinguishability in Maude-NPA. This kind of properties aim to verify that an attacker cannot distinguish between two versions of a protocol: for example, one using one secret and one using another, as it happens in electronic voting protocols. Finally, this thesis contributes to improve the efficiency of protocol verification in Maude-NPA. We define several techniques which drastically reduce the state space, and can often yield a finite state space, so that whether the desired security property holds or not can in fact be decided automatically, in spite of the general undecidability of such problems. / Santiago Pinazo, S. (2015). Advanced Features in Protocol Verification: Theory, Properties, and Efficiency in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/48527

Tesis por compendio / [ES] La herramienta criptográfica Maude-NPA es un verificador de modelos especializado para protocolos de seguridad criptográficos que tienen en cuenta las propiedades algebraicas de un sistema criptográfico. En la literatura, las propiedades criptográficas adicionales han descubierto debilidades de los protocolos de seguridad y, en otros casos, son parte de los supuestos de seguridad del protocolo para funcionar correctamente. Maude-NPA tiene una base teórica en la rewriting logic, la unificación ecuacional y el narrowing para realizar una búsqueda hacia atrás desde un patrón de estado inseguro para determinar si es alcanzable o no. Maude-NPA se puede utilizar para razonar sobre una amplia gama de propiedades criptográficas, incluida la cancelación del cifrado y descifrado, la exponenciación de Diffie-Hellman, el exclusive-or y algunas aproximaciones del cifrado homomórfico. En esta tesis consideramos nuevas propiedades criptográficas, ya sea como parte de protocolos de seguridad o para descubrir nuevos ataques. También hemos modelado diferentes familias de protocolos de seguridad, incluidos los Distance Bounding Protocols or Multi-party key agreement protocolos. Y hemos desarrollado nuevas técnicas de modelado para reducir el coste del análisis en protocolos con tiempo y espacio. Esta tesis contribuye de varias maneras al área de análisis de protocolos criptográficos y muchas de las contribuciones de esta tesis pueden ser útiles para otras herramientas de análisis criptográfico. / [CA] L'eina criptografica Maude-NPA es un verificador de models especialitzats per a protocols de seguretat criptogràfics que tenen en compte les propietats algebraiques d'un sistema criptogràfic. A la literatura, les propietats criptogràfiques addicionals han descobert debilitats dels protocols de seguretat i, en altres casos, formen part dels supòsits de seguretat del protocol per funcionar correctament. Maude-NPA te' una base teòrica a la rewriting lògic, la unificació' equacional i narrowing per realitzar una cerca cap enrere des d'un patró' d'estat insegur per determinar si es accessible o no. Maude-NPA es pot utilitzar per raonar sobre una amplia gamma de propietats criptogràfiques, inclosa la cancel·lació' del xifratge i desxifrat, l'exponenciacio' de Diffie-Hellman, el exclusive-or i algunes aproximacions del xifratge homomòrfic. En aquesta tesi, considerem noves propietats criptogràfiques, ja sigui com a part de protocols de seguretat o per descobrir nous atacs. Tambe' hem modelat diferents famílies de protocols de seguretat, inclosos els Distance Bounding Protocols o Multi-party key agreement protocols. I hem desenvolupat noves tècniques de modelització' de protocols per reduir el cost de l'analisi en protocols amb temps i espai. Aquesta tesi contribueix de diverses maneres a l’àrea de l’anàlisi de protocols criptogràfics i moltes de les contribucions d’aquesta tesi poden ser útils per a altres eines d’anàlisi criptogràfic. / [EN] The Maude-NPA crypto tool is a specialized model checker for cryptographic security protocols that take into account the algebraic properties of the cryptosystem. In the literature, additional crypto properties have uncovered weaknesses of security protocols and, in other cases, they are part of the protocol security assumptions in order to function properly. Maude-NPA has a theoretical basis on rewriting logic, equational unification, and narrowing to perform a backwards search from an insecure state pattern to determine whether or not it is reachable. Maude-NPA can be used to reason about a wide range of cryptographic properties, including cancellation of encryption and decryption, Diffie-Hellman exponentiation, exclusive-or, and some approximations of homomorphic encryption. In this thesis, we consider new cryptographic properties, either as part of security protocols or to discover new attacks. We have also modeled different families of security protocols, including Distance Bounding Protocols or Multi-party key agreement protocols. And we have developed new protocol modeling techniques to reduce the time and space analysis effort. This thesis contributes in several ways to the area of cryptographic protocol analysis and many of the contributions of this thesis can be useful for other crypto analysis tools. / This thesis would not have been possible without the funding of a set of research projects. The main contributions and derivative works of this thesis have been made in the context of the following projects: - Ministry of Economy and Business of Spain : Project LoBaSS Effective Solutions Based on Logic, Scientific Research under award number TIN2015-69175-C4-1-R, this project was focused on using powerful logic-based technologies to analyze safety-critical systems. - Air Force Office of Scientific Research of United States of America : Project Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA Scientific Research under award number FA9550-17-1-0286 - State Investigation Agency of Spain : Project FREETech: Formal Reasoning for Enabling and Emerging Technologies Scientific I+D-i Research under award number RTI2018-094403-B-C32 / Aparicio Sánchez, D. (2022). Modeling and Analysis of Advanced Cryptographic Primitives and Security Protocols in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/190915 / Compendio

<p dir="ltr">This thesis presents an in depth study and evaluation of a class of secure multiparty protocols that enable execution of a confidential software program $\mathcal{P}$ owned by Alice, on confidential data $\mathcal{D}$ owned by Bob, without revealing anything about $\mathcal{P}$ or $\mathcal{D}$ in the process. Our initial adverserial model is an honest-but-curious adversary, which we later extend to a malicious adverarial setting. Depending on the requirements, our protocols can be set up such that the output $\mathcal{P(D)}$ may only be learned by Alice, Bob, both, or neither (in which case an agreed upon third party would learn it). Most of our protocols are run by only two online parties which can be Alice and Bob, or alternatively they could be two commodity cloud servers (in which case neither Alice nor Bob participate in the protocols' execution - they merely initialize the two cloud servers, then go offline). We implemented and evaluated some of these protocols as prototypes that we made available to the open source community via Github. We report our experimental findings that compare and contrast the viability of our various approaches and those that already exist. All our protocols achieve the said goals without revealing anything other than upper bounds on the sizes of program and data.</p><p><br></p>

Background: This study investigates the role of gut feelings in early-stage venture investments, particularly in environments characterized by high uncertainty. By examining how both inexperienced and experienced investors utilize intuition, the research aims to uncover the cognitive and emotional foundations that influence investment decisions. Purpose: The research aims to understand how gut feelings impact investment decisions across different levels of investor experience. It compares the strategies of seasoned investors with those of novices, providing insights into how intuition and analytical reasoning are integrated. The objective is to offer practical guidance for investors on effectively combining gut feelings with analytical methods to navigate uncertain investment landscapes. Method: A multi-method qualitative approach was employed, combining semi-structured interviews and think-aloud protocols to capture real-time decision-making processes. Data were gathered from 11 investors, resulting in 14 hours of verbal protocols, which were subsequently analyzed using protocol analysis. A hypothetical investment scenario involving a fictional company, EcoPower Innovations, was used to elicit detailed responses from participants. Conclusion: The study finds significant differences in how gut feelings influence investment decisions based on the level of investor experience. Experienced investors skillfully blend intuition with data analysis, leveraging their expertise to manage uncertainty more effectively. In contrast, inexperienced investors tend to rely more on emotional impulses, demonstrating less integration of intuitive judgment with analytical reasoning. These findings highlight the importance of investor education in promoting the balanced use of gut feelings and analytical techniques, thereby improving decision-making in uncertain environments. Additionally, the research offers valuable insights for entrepreneurs on tailoring their approaches to potential investors based on their level of experience and expertise.

Cette thèse s’intéresse à la relation complexe entre processus ascendants (bottom-up) et processus descendants (top-down) dans la compréhension de l’oral L2 ; c’est-à-dire entre l’utilisation du signal sonore et de l’input linguistique d’une part, et l’intégration de connaissances diverses (linguistiques, discursives, pragmatiques, générales) d’autre part. Malgré de nombreux travaux en psycholinguistique, en acquisition des langues étrangères (L2) et en didactique (par exemple, Cutler & Clifton, 1999 ; Field, 2008; Rost, 2002 ; Brown, 1990), notre connaissance des processus cognitifs complexes de l’écoute ainsi que l’effet de certains facteurs sur la compréhension de l’oral restent à approfondir. Une appréciation plus fine de ces processus est indispensable aux questions relatives à l’enseignement et à l’apprentissage de la compréhension de l’oral en L2.Partant du principe que l’écoute a la même architecture cognitive en L1 et L2, nous commençons par un résumé – et une synthèse – des modèles psycholinguistiques récents de la compréhension de l’oral en L1. Nous examinons également les principaux facteurs rendant la compréhension difficile. Notre résumé des études en L2 consacrées au rôle de l'information descendante et au comportement stratégique des auditeurs L2 souligne la contribution importante de la métacognition. Nous tenterons donc ici de clarifier un certain flou terminologique qui caractérise ces travaux, et nous proposerons un modèle qui fait part de la métacognition dans la compréhension unidirectionnelle de l’oral en L2. Nous présentons ensuite les résultats d'une étude que nous avons menée pour analyser la contribution exacte de certains facteurs à l'écoute en L2.Les participants à cette étude sont des enseignants (n=23) et surtout des apprenants (n=226) français et tunisiens de l’anglais. En s’appuyant sur des méthodes multiples, à la fois quantitatives (différent tests et questionnaires) et qualitatives (questionnaires, tâches de réflexion à haute voix - Ericsson & Simon, 1993 - et de dévoilement graduel - gating, Grosjean, 1980), nous nous interrogeons: 1) sur les facteurs perçus par les apprenants et les enseignants comme étant déterminants dans la compréhension de l’anglais oral ; 2) sur la contribution relative de la compétence linguistique en L2, la discrimination auditive, la reconnaissance lexicale, et les compétences en méta-compréhension à une compréhension auditive réussie; 3) sur les problèmes que rencontrent nos auditeurs L2 lors de l’écoute, et sur les comportements stratégiques adoptés pour y faire face. Nous regardons plus particulièrement (pour ces différents paramètres) les différents niveaux de compétence en compréhension des sujets (avec une analyse poussée des auditeurs compétents et des auditeurs moins-compétents), ainsi qu’à de possibles influences de deux langues maternelles distinctes (français vs arabe tunisien). Nos analyses montrent : 1) ce que les apprenants et les enseignant perçoivent comme facteurs influant la compréhension de l’oral diffère relativement de ce qui la rend réellement problématique; 2) que la reconnaissance des mots et la connaissance lexicale contribuent significativement à la variation dans la compréhension, avec la reconnaissance des mots étant le prédicteur le plus fort ; 3) que les problèmes rencontrés en temps réel sont principalement de bas-niveau (segmentation de la parole), et que si les stratégies généralement contribuent à la compréhension, elles ne sont pas discriminatoires. Ce qui distingue donc l’auditeur expert du novice est son traitement formel (plus efficace et automatique) et non pas stratégique de l’information orale. Ces résultats sont discutés en rapport avec notre cadre théorique et selon une perspective pédagogique. / This thesis focuses on the complex relationship between bottom-up and top-down processes in L2 speech comprehension; i.e. between the use of the signal and the linguistic input on one hand, and the integration of various types of knowledge (linguistic, discourse, pragmatic, general) on the other hand. Despite a large body of research on the cognitive processes underlying listening in psycholinguistics, foreign language (L2) acquisition and teaching (e.g., Cutler & Clifton, 1999; Field, 2008a; Rost, 2002; Brown, 1990), there are still gaps in our understanding of these processes and the impact certain factors have on listening comprehension. Assuming that L1 and L2 listening follow the same cognitive architecture, we first review recent psycholinguistic models of L1 listening. We also examine the main factors constraining L2 listening comprehension. As our summary of the few SLA studies that have investigated the role of bottom-up information and the strategic behavior of L2 listeners points to the important contribution of metacognition, we clarify the terminological fuzziness characterizing this concept, and propose a model of metacognition in real-world unidirectional L2 listening. We then present the results of a study that we conducted to investigate the exact contribution of these different factors to L2 listening. The participants in this study were EFL French and Tunisian teachers (n=23) and learners (n=226). Using mixed quantitative (different tests and questionnaires) and qualitative (protocol analysis and gating experiments - Ericsson & Simon, 1993; Grosjean, 1980) methods, our aim was to investigate: 1) the factors perceived by learners and teachers as influencing L2 listening; 2) the relative contribution of linguistic knowledge, auditory discrimination, spoken word recognition (SWR), and meta-comprehension knowledge to successful L2 listening; 3) on-line listening problems and strategy use. For all of these parameters, we looked more closely at different levels of listening proficiency (various analyses of the performance of skilled and unskilled L2 listeners), as well as the possible influence of the two L1s (French and Tunisian Arabic) involved in the study.Our analyses show that: 1) there is a general discrepancy between what is perceived as making L2 listening difficult and what really renders it problematic; 2) SWR and vocabulary knowledge contribute significantly to the variance in L2 listening, with SWR being a stronger predictor; 3) listening problems encountered on-line are mainly lower-level (segmentation) and, although strategies contribute to speech comprehension, they are not discriminatory. What characterizes a proficient L2 listener seems to be accurate formal processing, not strategic processing of oral input. The findings are discussed from a theoretical and pedagogical perspective. Keywords: listening comprehension, French and Tunisian learners of L2 English, bottom-up and top-down processes, formal processing, integration and situation model, attentional resources, gating, protocol analysis, comparative analysis