168,905 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
Lazy-CSeq 0.6c: An improved lazy sequentialization tool for C (competition contribution)
No full textMU-CSeq 0.3: Sequentialization by read-implicit and coarse-grained memory unwindings (competition contribution)
No full textWe describe a new CSeq module that implements improved algorithms for the verification of multi-threaded C programs with dynamic thread creation. It is based on sequentializing the programs according to a guessed sequence of write operations in the shared memory (memory unwinding, MU). The original algorithm (implemented in MU-CSeq 0.1) stores the values of all shared variables for each write (read-explicit fine-grained MU), which requires multiple copies of the shared variables. Our new algorithms store only the writes (readimplicit MU) or only a subset of the writes (coarse-grained MU), which reduces the memory footprint of the unwinding and so allows larger unwinding bounds
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
Lazy-CSeq: a lazy sequentialization tool for c (competition contribution)
No full textWe describe a version of the lazy sequentialization schema by La Torre, Madhusudan, and Parlato that is optimized for bounded programs, and avoids the re-computation of the local state of each process at each context switch. Lazy-CSeq implements this sequentialization schema for sequentially consistent C programs using POSIX threads. Experiments show that it is very competitive
O semigrupo inverso das extensões abelianas parciais
No full textO objetivo principal desta tese e a construção do semigrupo inverso das classes de isomorfismo das extensões abelianas parciais de um anel comutativo.The main purpose of this thesis is the construction of the inverse semigroup of the isomorphism classes of the partial abelian extensions of a commutative ring
- …
