131,452 research outputs found
Verifying concurrent programs by memory unwinding
No full textWe describe a new sequentialization-based approach to the symbolic verification of multi-threaded programs with shared memory and dynamic thread creation. Its main novelty is the idea of memory unwinding, i.e., an explicit representation of the sequence of write operations into the shared memory. For the verification, we nondeterministically guess this unwinding and then simulate the behavior of the program according to any scheduling that respects this guess. This approach is complementary to other sequentializations and explores an orthogonal dimension, i.e., the number of write operations. It also simplifies the implementation of several important optimizations, in particular the targeted exposure of individual writes. We implemented this approach as code-to-code transformation from multi-threaded into nondeterministic sequential programs, which allows the reuse of sequential verification tools. Experiments show that our approach is very promising: it found all errors in the concurrency category of SV-COMP15
Bounded model checking of multi-threaded c programs via lazy sequentialization
No full textBounded model checking (BMC) has successfully been used for many practical program verification problems, but concurrency still poses a challenge. Here we describe a new approach to BMC of sequentially consistent C programs using POSIX threads. Our approach first translates a multi-threaded C program into a nondeterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It then re-uses existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so that it produces tight SAT/SMT formulae, and is thus very effective in practice: our prototype won the concurrency category of SV-COMP14. It solved all verification tasks successfully and was 30x faster than the best tool with native concurrency handling.<br/
Projeto de filtros digitais transicionais Cauer-Chebyshev inverso
No full textDissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Engenharia Elétrica.O presente trabalho apresenta uma metodologia de projeto de filtros transicionais a partir de aproximações não-polinomiais. A implementação desses filtros é realizada com base em técnicas de síntese de filtros digitais IIR, com o objetivo de obter o melhor desempenho de respostas de magnitude, fase e tempo visando uma específica aplicação. A utilização de filtros transicionais não-polinomiais, mais especificamente filtros transicionais Cauer-Chebyshev Inverso, deve-se ao fato de a aproximação Cauer apresentar a menor ordem dentre todas as funções de filtros seletores e de a aproximação Chebyshev Inverso ser também não-polinomial e apresentar melhores características de fase e de tempo em relação à aproximação Cauer. Os exemplos de aplicação mostrados são avaliados através de seis técnicas de projeto de filtros digitais utilizando-se uma abordagem de projeto indireta. Na tentativa de obter o melhor desempenho de cada uma delas são consideradas algumas estratégias de projeto, tais como pré-distorção e principalmente transformação espectral, cujo estudo resultou em procedimentos que melhoram a aplicabilidade dessa última. Assim, é possível compará-las entre si, possibilitando a escolha da melhor estratégia de filtragem para cada problema. Para auxiliar no projeto de filtros digitais como também viabilizar algumas medidas de linearidade de fase consideradas, um software em ambiente Matlab foi desenvolvido
Looking at Computations from a Different Angle
No full textWe present a novel framework to reason about programs based on encodings of computations as graphs. The main insight here is to rearrange the programs such that given a bound k, each computation can be explored according to any tree decomposition of width k of the corresponding behaviour graph. This produces under-approximations parameterized on k, which result in a complete method when we restrict to classes of behaviour graphs of bounded tree-width. As an additional feature, the transformation of the input program can be targeted to existing tools for the analysis, and thus, off-the-shelf tools based on fixed-point, or capable of analyzing sequential programs with scalar variables and nondeterminism, can be used.To illustrate our approach, we develop this framework for sequential programs and discuss how to extend it to handle concurrency. For the case of sequential programs, we develop a compositional approach to generate on-the-fly tree decompositions of nested words, which is based on graph-summaries. To illustrate our technique, we also implement our algorithms for C programs
MU-CSeq: sequentialization of c programs by shared memory unwindings (competition contribution)
No full textWe implement a new sequentialization algorithm for multi-threaded C programs with dynamic thread creation as a new CSeq module. The novel basic idea of this algorithm is to fix (by a nondeterministic guess) the sequence of write operations in the shared memory and then simulate the behavior of the program according to any scheduling that respects this choice. Simulation is done thread-by-thread and the thread creation mechanism is replaced by function calls
From Histology to High-Resolution Mapping: The Rise of Spatial Omics in Immunology
No full textThe immune system is deeply shaped by its anatomical context, with spatial organization emerging as a fundamental principle of immune regulation. Recent advances in spatial omics technologies—encompassing transcriptomics, proteomics, metabolomics, lipidomics, and phosphoproteomics—have revolutionized our ability to study immune processes within intact tissue environments. By preserving spatial coordinates while capturing high-dimensional molecular data, these technologies offer unprecedented insight into how immune cell states and functions are governed by local cues and tissue architecture. In this review, we provide an overview of the major spatial omics platforms, emphasizing methodologies that have gained traction within the immunology community and in our own research. We then illustrate how these tools have begun to elucidate the logic of immune compartmentalization across anatomically complex tissues. While not exhaustive, we highlight selected examples from the intestine, secondary lymphoid organs, and liver to show how spatial omics has uncovered region-specific immune programs, microenvironmental niches, and context-dependent signaling pathways. Together, these studies demonstrate how spatial omics technologies are redefining immunological inquiry—shifting the focus from isolated cell types to their spatially embedded roles in tissue physiology and pathology
Intimate interfaces in action: assessing the usability and subtlety of emg-based motionless gestures
No full textMobile communication devices, such as mobile phones and networked personal digital assistants (PDAs), allow users to be constantly connected and communicate anywhere and at any time, often resulting in personal and private communication taking place in public spaces. This private -- public contrast can be problematic. As a remedy, we promote intimate interfaces: interfaces that allow subtle and minimal mobile interaction, without disruption of the surrounding environment. In particular, motionless gestures sensed through the electromyographic (EMG) signal have been proposed as a solution to allow subtle input in a mobile context. In this paper we present an expansion of the work on EMG-based motionless gestures including (1) a novel study of their usability in a mobile context for controlling a realistic, multimodal interface and (2) a formal assessment of how noticeable they are to informed observers. Experimental results confirm that subtle gestures can be profitably used within a multimodal interface and that it is difficult for observers to guess when someone is performing a gesture, confirming the hypothesis of subtlety
- …
