Wait Times to Rheumatology and Rehabilitation Services for Persons with Arthritis in Quebec

L’arthrite est l’une des causes principales de douleur et d’incapacité auprès de la population canadienne. Les gens atteints d’arthrite rhumatoïde (AR) devraient être évalués par un rhumatologue moins de trois mois suivant l’apparition des premiers symptômes et ce afin de débuter un traitement médical approprié qui leur sera bénéfique. La physiothérapie et l’ergothérapie s’avèrent bénéfiques pour les patients atteints d’ostéoarthrite (OA) et d’AR, et aident à réduire l’incapacité. Notre étude a pour but d’évaluer les délais d’attente afin d’obtenir un rendez-vous pour une consultation en rhumatologie et en réadaptation dans le système de santé public québécois, et d’explorer les facteurs associés. Notre étude est de type observationnel et transversal et s’intéresse à la province de Québec. Un comité d’experts a élaboré trois scénarios pour les consultations en rhumatologie : AR présumée, AR possible, et OA présumée ; ainsi que deux scénarios pour les consultations en réadaptation : AR diagnostiquée, OA diagnostiquée. Les délais d’attente ont été mesurés entre le moment de la requête initiale et la date de rendez-vous fixée. L’analyse statistique consiste en une analyse descriptive de même qu’une analyse déductive, à l’aide de régression logistique et de comparaison bivariée. Parmi les 71 bureaux de rhumatologie contactés, et pour tous les scénarios combinés, 34% ont donné un rendez-vous en moins de trois mois, 32% avaient une attente de plus de trois mois et 34% ont refusé de fixer un rendez-vous. La probabilité d’obtenir une évaluation en rhumatologie en moins de trois mois est 13 fois plus grande pour les cas d’AR présumée par rapport aux cas d’OA présumée (OR=13; 95% Cl [1.70;99.38]). Cependant, 59% des cas d’AR présumés n’ont pas obtenu rendez-vous en moins de trois mois. Cent centres offrant des services publics en réadaptation ont été contactés. Pour tous les scénarios combinés, 13% des centres ont donné un rendez-vous en moins de 6 mois, 13% entre 6 et 12 mois, 24% avaient une attente de plus de 12 mois et 22% ont refusé de fixer un rendez-vous. Les autres 28% restant requéraient les détails d’une évaluation relative à l’état fonctionnel du patient avant de donner un rendez-vous. Par rapport aux services de réadaptation, il n’y avait aucune différence entre les délais d’attente pour les cas d’AR ou d’OA. L’AR est priorisée par rapport à l’OA lorsque vient le temps d’obtenir un rendez-vous chez un rhumatologue. Cependant, la majorité des gens atteints d’AR ne reçoivent pas les services de rhumatologie ou de réadaptation, soit physiothérapie ou ergothérapie, dans les délais prescrits. De meilleures méthodes de triage et davantage de ressources sont nécessaires.

Entourage d'un toxicomane. Profil clinique: besoins, interventions et impacts.

Rapport de stage présenté à la Faculté des Arts et des Sciences en vue de l'obtention du grade de Maîtrise ès sciences (M.Sc.) en criminologie.

Academic and social adjustment of teenagers in social rehabilitation : the role of intrinsic need satisfaction and autonomy support

Les études antérieures ont démontré les bénéfices de la satisfaction des besoins intrinsèques et du soutien à l’autonomie dans le domaine de l’éducation. Or, l’applicabilité des tenants principaux de la Théorie de l’Auto-Détermination (TAD; Deci & Ryan, 2000) n’a pas été investiguée auprès d’une population clinique d’adolescents. L’objectif de cette thèse doctorale est de faire la lumière sur la façon dont l'adaptation scolaire et sociale peut être favorisée par les agents de socialisation dans le contexte de la réadaptation sociale. Cette thèse est composée de deux études s’intéressant à l’application des tenants clés de la TAD auprès de deux échantillons d’adolescents vivant des problèmes d’adaptation et recevant des services d’éducation spécialisée et de réadaptation sociale. Les relations entre les concepts motivationnels de base sont étudiés afin de déterminer si, comme la TAD le propose, la satisfaction des besoins intrinsèques des jeunes peut être soutenue par le style interpersonnel des agents de socialisation (c.-à-d., le soutien à l’autonomie, l’implication et la structure). Il est aussi vérifié si ces concepts motivationnels améliorent la motivation ainsi que d’autres conséquences qui résultent de leur expérience, proposées par la TAD. La première étude a évalué si le style interpersonnel des enseignants peut favoriser la satisfaction des besoins des élèves, leur style de motivationl, tout comme leur ajustement scolaire. Les élèves en difficulté d’adaptation (N = 115) inscrits aux écoles internes des Centres de Réadaptation en raison de leurs problématiques émotionnelles et comportementales ont rempli les questionnaires à deux reprises, au début et à la fin de l’année scolaire. Les analyses de modèles d’équations structurelles révèlent que l’augmentation du soutien à l’autonomie et de l’implication (mais pas de la structure) des enseignants pendant l’année est associée à une augmentation de la satisfaction des besoins des élèves qui, conséquemment, conduit à une motivation scolaire plus auto-déterminée et à une diminution d’intentions de décrochage à la fin de l’année scolaire. De plus, l’amélioration de la satisfaction des besoins mène directement à une meilleure expérience affective à l’école. La deuxième étude consiste en une recherche expérimentale conduite auprès d’adolescentes en difficulté d’adaptation (N = 29). Le devis expérimental a permis de comparer l’impact de la présence (c. absence) du soutien à l’autonomie sur l’internalisation d’une tâche et sur les conséquences motivationnelles et expérientielles des jeunes. La tâche, fastidieuse mais importante, consistait à de la résolution de problèmes interpersonnels (activité clinique). Les résultats suggèrent qu’un style interpersonnel soutenant l’autonomie a augmenté la motivation auto-déterminée, la perception de la valeur de la tâche et son appréciation, ainsi que diminué les affects négatifs comparativement à la condition sans soutien à l’autonomie. Les résultats sont discutés en lien avec les implications théoriques et pratiques d’étendre la portée de la TAD à une population clinique d’adolescents aux prises avec des difficultés d’adaptation.

Santé reproductive et santé mentale des femmes qui ont subi la violence sexuelle en temps de conflit armé : cas de la République Démocratique du Congo

Problématique : Depuis bientôt deux décennies, la République Démocratique du Congo (RDC) est le territoire d’un conflit armé qui, selon l’International Rescue Commite, aurait occasionné plus de 3 millions de décès et autant de déplacés internes. Plusieurs rapports font également cas des nombreux actes de violence sexuelle (les viols, les mutilations, l’esclavage, l’exploitation sexuelle, etc.) commis envers les filles, les femmes et dans une moindre ampleur les hommes. S’il existe un consensus sur le côté barbare des actes de violence sexuelle liés aux conflits armés, rares sont les études qui ont évalué leurs conséquences sur la santé reproductive des survivantes surtout en termes d’issues telles que les fistules, les douleurs pelviennes chroniques (DPC), le désir de rapports sexuels, le désir d’enfant et le désir d’interruption de la grossesse issue de tels actes. Par ailleurs, même si la santé mentale des populations en zones de conflit représente un sujet d’intérêt, l’impact spécifique de la violence sexuelle liée au conflit sur la santé mentale des survivantes a été peu étudié. De plus, ces travaux s’intéressent aux effets de la violence sexuelle liée au conflit sur la santé mentale et sur la santé reproductive séparément et ce, sans évaluer les relations qui peuvent exister entre ces deux dimensions qui, pourtant, s’influencent mutuellement. Aussi, l’impact social de la violence sexuelle liée au conflit, ainsi que la contribution des normes socioculturelles aux difficultés que rencontrent les survivantes, a été peu étudié. Pourtant, l’impact social de la violence sexuelle liée au conflit peut permettre de mieux comprendre comment l’expérience d’un tel acte peut affecter la santé mentale. Enfin, aucune étude n’a évalué les effets de la violence sexuelle liée au conflit en la comparant à la violence sexuelle non liée au conflit (VSNLC). Pourtant, il est reconnu qu’à de nombreux égards, la violence sexuelle liée au conflit est bien différente de la VSNLC puisqu’elle est perpétrée avec l’intention de créer le maximum d’effets adverses pour la victime et sa communauté. Objectifs : Les objectifs poursuivis dans cette thèse visent à : 1) évaluer les effets de la violence sexuelle liée au conflit sur la santé reproductive; 2) évaluer les effets de la violence sexuelle liée au conflit sur la santé mentale en termes de sévérité des symptômes de stress posttraumatique (PTSD), de sévérité des symptômes de détresse psychologique et de probabilité de souffrir de troubles mentaux communs (TMC); 3) évaluer la contribution des troubles physiques de santé reproductive, en particulier les fistules et les douleurs pelviennes chroniques (DPC), aux effets de la violence sexuelle liée au conflit sur la santé mentale; 4) évaluer la contribution de l’état de santé mentale aux effets de la violence sexuelle liée au conflit sur le désir de rapports sexuels et le désir d’enfant; et 5) étudier l’impact de la violence sexuelle liée au conflit sur le plan social ainsi que la contribution des normes socioculturelles à ses effets adverses et la façon dont ces effets pourraient à leur tour influencer la santé des femmes et leur relation avec l’enfant issu de l’acte de violence sexuelle subi. Méthodologie : Un devis mixte de nature convergente a permis de collecter des données quantitatives auprès de l’ensemble des participantes (étude transversale) et des données qualitatives sur un nombre plus restreint de femmes (étude phénoménologique). Une étude transversale populationnelle a été conduite entre juillet et août 2012 auprès de 320 femmes âgées de 15 à 45 ans habitant quatre (4) quartiers de la ville de Goma située dans la province du Nord-Kivu en RDC. Les femmes ont été recrutées à travers des annonces faites par les responsables des programmes d’alphabétisation et de résolution de conflits implantés dans les différents quartiers par le Collectif Alpha Ujuvi, une ONG locale. Les issues de santé reproductive évaluées sont : les fistules, les DPC, le désir de rapports sexuels, le désir d’enfant et le désir d’interruption de la grossesse issue d’un acte de violence sexuelle. Les variables de santé mentale d’intérêt sont : la sévérité des symptômes de détresse psychologique, la sévérité des symptômes de PTSD et la probabilité de souffrir de TMC. Pour les analyses, l’exposition a été définie en trois (3) catégories selon l’expérience passée de violence sexuelle : les femmes qui ont vécu des actes de violence sexuelle liée au conflit, celles qui ont vécu des actes de VSNLC et celles qui ont déclaré n’avoir jamais subi d’acte de violence sexuelle au cours de leur vie. Les variables de confusion potentielles mesurées sont : l’âge, le statut matrimonial, le nombre d’enfants, le niveau d’éducation le plus élevé atteint et l’occupation professionnelle. Les mesures d’associations ont été évaluées à l’aide de modèles de régressions logistiques et linéaires simples et multiples. Des tests d’interaction multiplicative et des analyses stratifiées ont été également conduits pour évaluer l’effet potentiellement modificateur de quelques variables (âge, statut matrimonial, nombre d’enfants) sur la relation entre la violence sexuelle et les variables de santé reproductive ou de santé mentale. Ces tests ont également été utilisés pour évaluer la contribution d’une variable de santé reproductive ou de santé mentale aux effets de la violence sexuelle sur l’autre dimension de la santé d’intérêt dans cette étude. Une étude phénoménologique a été conduite dans le même intervalle de temps auprès de 12 femmes ayant participé à la partie quantitative de l’étude qui ont vécu la violence sexuelle liée au conflit et ont eu un enfant issu d’une agression sexuelle. Les sujets explorés incluent : la perception de l’acte de violence sexuelle liée au conflit vécu et de la vie quotidienne par les victimes; la perception de l’acte de violence sexuelle liée au conflit par la famille et l’entourage et leurs réactions après l’agression; la perception de la grossesse issue de l’acte de violence sexuelle par la victime; la perception de l’enfant issu de la violence sexuelle liée au conflit par la victime ainsi que son entourage; les conséquences sociales de l’expérience de violence sexuelle liée au conflit et les besoins des victimes pour leur réhabilitation. Une analyse thématique avec un codage ouvert a permis de ressortir les thèmes clés des récits des participantes. Par la suite, l’approche de théorisation ancrée a été utilisée pour induire un cadre décrivant l’impact social de l’expérience de la violence sexuelle liée au conflit et les facteurs y contribuant. Résultats : Le premier article de cette thèse montre que, comparées aux femmes qui n’ont jamais vécu un acte de violence sexuelle, celles qui ont vécu la violence sexuelle liée au conflit ont une probabilité plus élevée d’avoir une fistule (OR=11.1, IC 95% [3.1-39.3]), des DPC (OR=5.1, IC 95% [2.4-10.9]), de rapporter une absence de désir de rapports sexuels (OR=3.5, IC 95% [1.7-6.9]) et une absence de désir d’enfant (OR=3.5, IC 95% [1.6-7.8]). Comparées aux mêmes femmes, celles qui ont vécu la VSNLC ont plus de probabilité de souffrir de DPC (OR=2.3, IC 95% [0.95-5.8]) et de rapporter une absence de désir d’enfant (OR=2.7, IC 95% [1.1-6.5]). Comparées aux femmes qui ont vécu la VSNLC, celles qui ont vécu la violence sexuelle liée au conflit ont également une probabilité plus élevée d’avoir une fistule (OR=9.5, IC 95% [1.6-56.4]), des DPC (OR=2.2, IC 95% [0.8-5.7]) et de rapporter une absence de désir de rapports sexuels (OR=2.5, IC 95% [1.1-6.1]). En ce qui concerne les grossesses issues des viols, comparées aux femmes qui ont vécu la VSNLC, celles qui ont vécu la violence sexuelle liée au conflit sont plus nombreuses à souhaiter avorter (55% vs 25% pour celles qui ont vécu la VSNLC). Elles sont également plus nombreuses à déclarer qu’elles auraient avorté si les soins appropriés étaient accessibles (39% vs 21% pour celles qui ont vécu la VSNLC). Le second article montre qu’en comparaison aux femmes qui n’ont jamais subi de violence sexuelle, celles qui ont vécu la violence sexuelle liée au conflit présentent des symptômes de détresse psychologique (moyennes de score respectives 8.6 et 12.6, p<0.0001) et des symptômes de PTSD (moyennes de score respectives 2.2 et 2.6, p<0.0001) plus sévères et ont plus de probabilité d’être dépistées comme un cas de TMC (30% vs 76%, p<0.0001). De plus, comparées aux femmes qui ont vécu la VSNLC, celles qui ont vécu la violence sexuelle liée au conflit présentent des symptômes de détresse psychologique (moyennes de score respectives 10.1 et 12.6, p<0.0001) et des symptômes de PTSD (moyennes de score respectives 2.2 et 2.6, p<0.0001) plus sévères et ont plus de probabilité d’être dépistées comme un cas de TMC (48% vs 76%, p<0.001). Les valeurs minimales et maximales de score de sévérité de symptômes de détresse psychologique sont de 0/12 pour les femmes qui n’ont jamais vécu de violence sexuelle, 4/19 pour celles qui ont vécu la VSNLC et de 5/18 pour celles qui ont vécu la violence sexuelle liée au confit. En ce qui concerne la sévérité des symptômes de PTSD, les scores minimal et maximal sont respectivement de 0.36/3.22, 0.41/3.41 et 0.95/3.45. Le fait d’avoir développé une fistule ou de souffrir de DPC après l’agression sexuelle augmente la force des associations entre la violence sexuelle et la santé mentale. Les femmes qui ont subi la violence sexuelle liée au conflit et qui ont souffert de fistules présentent des symptômes de détresse psychologique et de PTSD plus sévères comparées aux femmes qui ont subi la violence sexuelle liée au conflit mais n’ont pas de fistules. Les résultats sont similaires pour les femmes qui ont subi la violence sexuelle liée au conflit et qui souffrent de DPC. Des résultats complémentaires suggèrent que le statut matrimonial modifie l’effet de la violence sexuelle sur la sévérité des symptômes de détresse psychologique, les femmes divorcées/séparées et les veuves étant celles qui ont les moyennes de score les plus élevées (respectivement 11.3 et 12.1 vs 9.26 et 9.49 pour les célibataires et les mariées). Par ailleurs, la sévérité des symptômes de détresse psychologique modifie l’association entre la violence sexuelle liée au conflit et le désir d’enfant. Le troisième article montre que, sur le plan social, l’expérience de violence sexuelle liée au conflit entraine également de lourdes conséquences. Toutes celles qui ont vécu ce type d’acte décrivent leur vie de survivante et de mère d’un enfant issu d’une agression sexuelle comme difficile, oppressive, faite de peines et de soucis et sans valeur. Plusieurs facteurs influencent la description que les victimes de violence sexuelle liée au conflit font de leur vie quotidienne, et ils sont tous reliés aux normes socioculturelles qui font de la femme une citoyenne de seconde zone, ne font aucune différence entre un viol et un adultère, condamnent les victimes de violence sexuelle plutôt que leurs agresseurs, rejettent et stigmatisent les victimes de tels actes ainsi que l’enfant qui en est issu. En réponse au rejet et au manque de considération, les femmes victimes de violence sexuelle liée au conflit ont tendance à s’isoler pour éviter les insultes et à garder le silence sur leur agression. En plus, les réactions de leur entourage/communauté ont tendance à leur faire revivre l’agression sexuelle subie, autant d’éléments qui nuisent davantage à leur réhabilitation. D’autres résultats démontrent que les enfants issus d’actes de violence sexuelle liée au conflit sont également rejetés par leur communauté, leur famille adoptive ainsi que le conjoint de leur mère, ce qui affecte davantage les survivantes. Avec leurs mères, les relations développées varient entre le rejet, la résignation et l’affection. Néanmoins, ces relations sont plus souvent tendues probablement à cause de la stigmatisation de la communauté. Conclusion: La violence sexuelle liée au conflit a des effets adverses sur la santé reproductive, la santé mentale mais également sur le plan social. Ces trois dimensions sont loin d’être isolées puisque cette étude a permis de démontrer qu’elles s’influencent mutuellement. Ceci suggère que la prise en charge des victimes de violence sexuelle liée au conflit ne doit pas se concentrer sur un aspect ou un autre de la santé mais prendre en compte l’ensemble des dimensions de la femme pour offrir une aide holistique, plus adaptée et qui sera plus efficace à long terme.

Insights from youth workers regarding young people's engagement in out-of-school-time youth development programs

L’objectif de cette étude exploratoire était de mieux comprendre, du point de vue des animateurs/animatrices qui oeuvrent auprès des jeunes, le phénomène de l’engagement des jeunes dans les programmes parascolaires. Des entretiens qualitatifs ont été entrepris à cette fin avec six animateur(trices). Plusieurs obstacles à l’engagement ont été identifiés, la plupart étant extérieurs aux jeunes. Quelques actions et attitudes spécifiques des animateur(trices) ont été relevées comme importantes pour aider les jeunes à surmonter ces obstacles. De plus, la structure et le contenu du programme, ainsi que l’environnement de groupe, jouent des rôles primordiaux. Les dimensions soulevées par les animateur(trices) ont permis d’enrichir et rendre plus holistique un modèle d’engagement qui a été développé à partir d’une recension des écrits dans ce domaine. Finalement, les implications pour la formation des animateurs(trices) et pour la structure des programmes pour les jeunes ont été explorées.

The effectiveness of scoliosis screening programs: methods for systematic review and expert panel recommendations formulation

Background: Literature on scoliosis screening is vast, however because of the observational nature of available data and methodological flaws, data interpretation is often complex, leading to incomplete and sometimes, somewhat misleading conclusions. The need to propose a set of methods for critical appraisal of the literature about scoliosis screening, a comprehensive summary and rating of the available evidence appeared essential. METHODS: To address these gaps, the study aims were: i) To propose a framework for the assessment of published studies on scoliosis screening effectiveness; ii) To suggest specific questions to be answered on screening effectiveness instead of trying to reach a global position for or against the programs; iii) To contextualize the knowledge through expert panel consultation and meaningful recommendations. The general methodological approach proceeds through the following steps: Elaboration of the conceptual framework; Formulation of the review questions; Identification of the criteria for the review; Selection of the studies; Critical assessment of the studies; Results synthesis; Formulation and grading of recommendations in response to the questions. This plan follows at best GRADE Group (Grades of Recommendation, Assessment, Development and Evaluation) requirements for systematic reviews, assessing quality of evidence and grading the strength of recommendations. CONCLUSIONS: In this article, the methods developed in support of this work are presented since they may be of some interest for similar reviews in scoliosis and orthopaedic fields.

Le programme cognitif-comportemental au CJM-IU : l'effet du degré d'exposition au programme sur l'ampleur des troubles de comportement des adolescentes six mois après leur admission au CJM-IU

L’implantation de programmes probants dans les milieux d’intervention peut comporter son lot de difficultés pour les gestionnaires ainsi que les intervenants en contexte de réadaptation pour adolescents. En effet, les contraintes auxquelles peuvent être confrontés les milieux de pratique mènent parfois à la modification des programmes, ceci en vue de faciliter leur implantation. Il devient alors important de documenter ainsi qu’identifier l’effet des éléments associés à la fidélité d’implantation lorsque les programmes d’intervention sont évalués. En plus d’évaluer l’effet du degré d’exposition au programme cognitif-comportemental implanté dans les unités d’hébergement du Centre jeunesse de Montréal – Institut universitaire (CJM-IU) sur l’ampleur des troubles de comportement des adolescentes, ce mémoire propose une nouvelle piste de recherche. Puisque la recherche empirique ne permet pas encore d’identifier les conditions selon lesquelles il serait possible de modifier les programmes d’intervention qui sont adoptés dans le contexte de la pratique, cette étude propose d’élaborer une logique d’exposition au programme qui s’inspire des principes d’intervention efficace élaborés par Andrews et ses collègues (1990). Cette approche permettrait d’adapter le niveau d’intervention aux caractéristiques de la clientèle, et ce, tout en s’assurant de l’efficacité du programme cognitif-comportemental. L’échantillon de cette étude est donc constitué de 74 adolescentes hébergées au CJM-IU pour une durée de six mois. Les résultats indiquent d’abord que les activités du programme cognitif-comportemental ont été appliquées de façon plutôt irrégulière et bien en deçà de la fréquence initialement prévue, ce qui rend bien compte des difficultés à implanter des programmes en contexte de pratique. Les résultats suggèrent aussi une diminution de l’ampleur des troubles de comportement six mois après l’admission au CJM-IU pour les adolescentes qui étaient caractérisées par une ampleur des troubles de comportement plus marquée au moment de leur admission et qui ont complété un plus grand nombre d’auto-observations durant leur placement.

Quand la réadaptation blesse? Éducateurs victimes de violence

Cette étude vise à comprendre le phénomène de la violence physique vécue par les éducateurs oeuvrant dans dix Centres Jeunesse (CJ) du Québec. Pour ce faire, un sondage de victimisation a été administré à 586 éducateurs en internat. En premier lieu, la prévalence de cette problématique sera établie. Par la suite, les facteurs individuels et environnementaux prédisposant aux agressions physiques seront identifiés. Des éducateurs sondés, 53,9 % rapportent avoir été victimes de violence physique au cours de la dernière année. Sur le plan individuel, être affecté par les manifestations agressives des clients et la fréquence des violences psychologiques subies augmentent les risques de victimisation physique. Quant au contexte, l’âge de la clientèle et le motif de l’intervention (basé sur la loi justifiant le placement) auprès de l’enfant ou de l’adolescent influencent l’occurrence des actes violents dirigés contre les éducateurs. Nos analyses montrent également que les violences physiques dont sont victimes les éducateurs affectent autant l’individu que l’institution. L’identification de facteurs permettant de prédire les risques de victimisation pourrait notamment servir à orienter les programmes de prévention de la violence dans les CJ, mais aussi à cibler les éducateurs les plus à risque afin de leur fournir un soutien adapté.

Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code.

Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code

A Compilation Strategy for Numerical Programs Based on Partial Evaluation

This work demonstrates how partial evaluation can be put to practical use in the domain of high-performance numerical computation. I have developed a technique for performing partial evaluation by using placeholders to propagate intermediate results. For an important class of numerical programs, a compiler based on this technique improves performance by an order of magnitude over conventional compilation techniques. I show that by eliminating inherently sequential data-structure references, partial evaluation exposes the low-level parallelism inherent in a computation. I have implemented several parallel scheduling and analysis programs that study the tradeoffs involved in the design of an architecture that can effectively utilize this parallelism. I present these results using the 9- body gravitational attraction problem as an example.

Memory Usage Inference for Object-Oriented Programs

We present a type-based approach to statically derive symbolic closed-form formulae that characterize the bounds of heap memory usages of programs written in object-oriented languages. Given a program with size and alias annotations, our inference system will compute the amount of memory required by the methods to execute successfully as well as the amount of memory released when methods return. The obtained analysis results are useful for networked devices with limited computational resources as well as embedded software.

On-the-Fly Maintenance of Series-Parallel Relationships in Fork-Join Multithreaded Programs

A key capability of data-race detectors is to determine whether one thread executes logically in parallel with another or whether the threads must operate in series. This paper provides two algorithms, one serial and one parallel, to maintain series-parallel (SP) relationships "on the fly" for fork-join multithreaded programs. The serial SP-order algorithm runs in O(1) amortized time per operation. In contrast, the previously best algorithm requires a time per operation that is proportional to Tarjan’s functional inverse of Ackermann’s function. SP-order employs an order-maintenance data structure that allows us to implement a more efficient "English-Hebrew" labeling scheme than was used in earlier race detectors, which immediately yields an improved determinacy-race detector. In particular, any fork-join program running in T₁ time on a single processor can be checked on the fly for determinacy races in O(T₁) time. Corresponding improved bounds can also be obtained for more sophisticated data-race detectors, for example, those that use locks. By combining SP-order with Feng and Leiserson’s serial SP-bags algorithm, we obtain a parallel SP-maintenance algorithm, called SP-hybrid. Suppose that a fork-join program has n threads, T₁ work, and a critical-path length of T[subscript ∞]. When executed on P processors, we prove that SP-hybrid runs in O((T₁/P + PT[subscript ∞]) lg n) expected time. To understand this bound, consider that the original program obtains linear speed-up over a 1-processor execution when P = O(T₁/T[subscript ∞]). In contrast, SP-hybrid obtains linear speed-up when P = O(√T₁/T[subscript ∞]), but the work is increased by a factor of O(lg n).