124,552 research outputs found
SMT-based bounded model checking of multi-threaded software in embedded systems
No full textOur reliance on the correct functioning of embedded systems is growing rapidly. Such systems are used in a wide range of applications such as airbag control systems, mobile phones, and high-end television sets. These systems are becoming more and more complex and require multi-core processors with scalable shared memory to meet the increasing computational power demands. The reliability of the embedded (distributed) software is thus a key issue in the system development. In this thesis we describe and evaluate an approach to reason accurately and effectively about large embedded software using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT) techniques. We present three major novel contributions. First, we extend the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, unions and pointers and thus making our approach suitable to reason about embedded software. We then provide new encodings into existing SMT theories and we show that our translations from ANSI-C programs to SMT formulas are as precise as bit-accurate procedures based on Boolean Satisfiability. Second, we develop three related approaches for model checking multi-threaded software in embedded systems. In the lazy approach, we generate all possible interleavings and call the SMT solver on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation and widening approach, we reduce the state space by abstracting the number of interleavings from the proofs of unsatisfiability generated by the SMT solvers. Finally, we describe and evaluate an approach to integrate our SMT-based BMC into the software engineering process by making the verification process incremental. In particular, our approach looks at the modifications suffered by the software system since its last verification, and submits them to a partly static and dynamic verification process, which is thus guided by a set of test cases for coverage. Experiments show that our SMT-based BMC can analyze larger problems and reduce the verification time compared to state-of-the-art techniques that use BMC, iterative context-bounding or counterexample-guided abstraction refinement
Cordeiro, Graça índias, Baptista, Luis Vicente et Costa, António Firmino da (org.), Etnografias urbanas, 2003
No full textCardoso Isabel L. Cordeiro, Graça índias, Baptista, Luis Vicente et Costa, António Firmino da (org.), Etnografias urbanas, 2003. In: Recherches en anthropologie au Portugal, n°1, 2003. Lusodescendance : représentations, pratiques et enjeux. pp. 122-126
Euphorbia blepharadena O. L. M. Silva & Cordeiro, sp. nov.
No full textEuphorbia blepharadena O.L.M.Silva & Cordeiro sp. nov. urn:lsid:ipni.org:names:77214813-1 Figs 1–2 Diagnosis Euphorbia blepharadena O.L.M.Silva & Cordeiro sp. nov. is similar to Euphorbia foliolosa Boiss. but differs in its smaller leaves with a denser indumentum composed of long (ca 1 mm) trichomes, cyathial glands with digitate appendages and pubescent ovary /fruit. Type BRAZIL • Minas Gerais, Jaíba, Furados, “ lado direito da Estrada Jaíba – Mocambinho” [right side of the road Jaíba – Mocambinho]; 15°12′37″ S, 43°51′33″ W; 19 Oct. 2001; J.A. Lombardi et al. 4433; holotype: UEC[018613]; isotype: BHCB[64825]. Etymology The epithet is a reference to the cyathial gland appendages, which look like eyelashes on these glands (Fig. 1G). Description Erect monoecious herbs, up to 30 cm tall; underground system not seen; latex white. Stems terete, irregularly branched, brown when dried, pubescent, with short (<0.25 mm) curved and longer (ca 1 mm) erect simple trichomes. Leaves opposite, persistent, subsessile (petioles reaching up to 1 mm long); stipules interpetiolar, deltoid, inconspicuous (up to 1 mm long), apex fimbriate, indumentum of erect, long (ca 1 mm), simple trichomes; leaf blade membranaceous, pilose on the adaxial surface and densely pilose on the abaxial surface, both surfaces with erect, long (ca 1 mm), simple trichomes, discolorous (abaxial surface slightly lighter), elliptic to oblong, 0.5–0.8(–1) × 0.15–0.2 cm, base asymmetric, margin serrate with a colleter at the apex of each tooth, apex acute, venation hyphodromous. Cyathia solitary, axillary, subsessile; peduncle up to 1.5 mm long, with a few scattered erect, long (ca 1 mm), simple trichomes; involucre turbinate, 1.5–2.5 × 0.8–1.3 mm, actinomorphic, pilose on the outer surface, with erect, long (ca 1 mm), simple trichomes; involucral lobes triangular, pale to greenish when dried, margin fimbriate; cyathial glands 4(5), dark when dried, transversely elliptic and slightly concave, smooth, glabrous, 0.2–0.3 × 0.2–0.3 mm; cyathial gland appendages 6–8-digitate, lobes linear, 1.5–1.8(–2) mm long, white when dried, glabrous. Staminate flowers 25–35, arranged in (4)5 cincinni with 6–7 flowers each; bracteoles lanceolate, ciliate; pedicels up to 2 mm long, filaments up to 1 mm long, anthers ca 0.5 mm wide, dorsifixed, extrorse, transversely dehiscent. Pistillate flowers ca 7 mm long; pedicel up to 2.5 mm long; ovary globose, ca 1.5 × 1.5 mm, densely pubescent, with erect, long (ca 1 mm), simple trichomes; styles 3, 3.5–4 mm long, united only at the base, entire and slightly revolute at the apex, glabrous. Capsules 3-lobed, subglobose, 3.0–3.5 × 3.5–4 mm, pubescent, with erect, long (ca 1 mm) simple trichomes, green; pedicel shortly accrescent, reaching up to 4 mm long; columella 2–2.5 mm long; seeds brown, ovoid, ca 2 × 1 mm, tetragonous in cross section, testa shallowly tuberculate. Distribution, ecology, and phenology Euphorbia blepharadena sp. nov. occurs in clay soils in flat rocky outcrops (ʻlageadoʼ) in northeast Minas Gerais, within the Cerrado domain (Fig. 2). The only specimen found so far was collected in October with both flowers and fruits. Provisional conservation status Euphorbia blepharadena sp. nov. is only known from a single locality (Fig. 2), with AOO <10 km ² and EOO <100 km ². Its habitat is subjected to continuing decline in area, extent and quality. In the light of this, our evaluation suggests it to be classified as Critically Endangered (CR; B2ab[iii]).Published as part of Silva, Otávio Luis Marques da, Braun, Pierre, Riina, Ricarda & Cordeiro, Inês, 2021, Three new species of Euphorbia subgenus Chamaesyce (Euphorbiaceae) endemic to Brazil, pp. 72-86 in European Journal of Taxonomy 733 on pages 74-76, DOI: 10.5852/ejt.2021.733.1223, http://zenodo.org/record/570622
Verifying multi-threaded software using SMT-based context-bounded model checking
No full textWe describe and evaluate three approaches to model check multi-threaded software with shared variables and locks using bounded model checking based on Satisfiability Modulo Theories (SMT) and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the SMT solver on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation and widening approach, we reduce the state space by abstracting the number of interleavings from the proofs of unsatisfiability generated by the SMT solvers. In all three approaches, we bound the number of context switches allowed among threads in order to reduce the number of interleavings explored. We implemented these approaches in ESBMC, our SMT-based bounded model checker for ANSI-C programs. Our experiments show that ESBMC can analyze larger problems and substantially reduce the verification time compared to state-of-the-art techniques that use iterative context-bounding algorithms or counter-example guided abstraction refinement
The 2008 Survey of the use of Unimarc - diaporama
Full text linkDiaporama de l\u27intervention de Maria Inês Cordeiro présentant l\u27enquête 2008 sur l\u27utilisation du format Unimarc dans le monde, à l\u27occasion de la 3e rencontre internationale des utilisateurs d\u27Unimarc
The 2008 worlwide survey of the use of Unimarc
No full textIntervention audio, en anglais, de Maria Inês Cordeiro directrice du Programme Unimarc de l\u27IFLA présentant les résultat d\u27une étude mondiale menée en 2008 sur l\u27utilisation d\u27Unimarc
Towards A Semiformal Development Methodology for Embedded Systems
No full textIn recent days, the amount of functions has increased significantly in embedded products so that systems development methodologies play an important role to ensure the product’s quality, cost, and time. Furthermore, this complexity coupled with constantly evolving specifications, has led to propose a semiformal development methodology to support the building of embedded real-time systems. A platform-based design approach has been used to balance costs and time-to-market in relation to performance and functionality constraints. We performed three expressive case studies and we concluded that the proposed methodology significantly reduces design time and improves software modularity and reliability
Rota do cordeiro.
Full text linkResumo: Pela perspectiva do desenvolvimento regional, reestruturar a cadeia produtiva da ovinocaprinocultura é uma questão estratégica, haja vista o grande número de ocupações e postos de trabalho e renda gerados por essas atividades, especialmente para pequenos produtores rurais em regiões de baixa renda de todo o País. O desenvolvimento do setor é comprometido pela dificuldade de se estabelecer uma ligação mais forte entre produção, processamento e mercado. Malgrado os expressivos rebanhos de ovinos e caprinos existentes, a maioria dos frigoríficos certificados opera com capacidade ociosa, por falta de animais para abate. O pleno aproveitamento do potencial do setor exige a adoção de um conjunto integrado de iniciativas estruturantes, públicas e privadas, situação que justificou a criação da Rota do Cordeiro, no contexto das Rotas de Integração Nacional, iniciativa sob a responsabilidade do Ministério do Desenvolvimento Regional. O objetivo da Rota do Cordeiro é promover o desenvolvimento territorial, urbano e regional por meio do fortalecimento dos sistemas produtivos e inovativos associados à ovinocaprinocultura. Termos de indexação: ovinocaprinocultura, inclusão produtiva, inovação. Abstract: From the perspective of regional development, restructuring the sheep and goat production chain is a strategic issue, given the large number of occupations, jobs, and income generated by these activities, especially for small-scale farmers in lowincome regions throughout Brazil. This sector development is hampered by the difficulty of establishing a stronger link between production, processing and marketing. Despite the significant sheep and goat livestock, most certified slaughterhouse operate at idle capacity due to lack of animals. To fully exploit the sector?s potential it is required the adoption of an integrated set of structuring initiatives, both public and private, which justified the creation of the Lamb Route, in the context of the National Integration Routes, an initiative under the responsibility of the Ministry of Regional Development. The purpose of the Lamb Route is to promote territorial, urban and regional development by strengthening the productive and innovative systems associated with sheep and goat farming
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
O pensamento econômico em saúde de Hésio Cordeiro sobre o financiamento da saúde pública no Brasil e a intervenção anticíclica em Claudio Napoleoni
Full text linkThis paper introduces a theoretical reflection about the problem of health financing from the perspective of Hésio Cordeiro, one of the most important sanitarians of the 1980s in Brazil, and how this author was influenced by the work of Claudio Napoleoni. For this purpose, the essay was used as textual unit and content analysis was incorporated as methodology. The content is structured in three parts. The first describes a brief intellectual and political-institutional biography of Cordeiro and Napoleoni, trying to situate both authors in their historical contexts. The second part shows how Cordeiro was inspired by Napoleoni’s work, which influenced the way Cordeiro addressed countercyclical solutions to rethink public health issues during the 1980s. The third points to a brief final consideration on the importance of Cordeiro as an intellectual who proposed progressist solutions for health back in his time.Neste artigo, realiza-se uma reflexão teórica sobre como Hésio Cordeiro, um dos sanitaristas mais influente dos anos de 1980, tratou o problema do financiamento da saúde em sua obra, sob a influência de Claudio Napoleoni. Para isso, usou-se o ensaio como modalidade textual e, como método, a análise de conteúdo. O texto está estruturado em três partes. A primeira descreve uma breve biografia intelectual e político-institucional de Hésio Cordeiro e de Claudio Napoleoni a fim de situá-los historicamente. A segunda versa sobre como Cordeiro foi inspirado por Napoleoni ao analisarmos as soluções anticíclicas para pensar a saúde pública nos anos de 1980. Por último, a terceira aponta uma breve consideração final para valorizarmos a importância de Cordeiro como um intelectual propositor de soluções progressistas para a saúde no seu tempo.
 
- …
