Publications

Model Checking of Distributed Algorithms Using Synchronous Programs

PDF
Stabilization, Safety, and Security of Distributed Systems
Abstract: The development of trustworthy self-stabilizing algorithms requires the verification of some key properties with respect to the formal specification of the expected system executions. The atomic-state model (ASM) is the most commonly used computational model to reason on self-stabilizing algorithms. In this work, we propose methods and tools to automatically verify the self-stabilization of distributed algorithms defined in that model. To that goal, we exploit the similarities between the ASM and computational models issued from the synchronous programming area to reuse their associated verification tools, and in particular their model checkers. This allows the automatic verification of all safety (and bounded liveness) properties of any algorithm, regardless of any assumptions on network topologies and execution scheduling.

[Re] A Multi-Functional Synthetic Gene Network

PDF
ReScience C: Volume 8, Issue 1
Abstract: Studies in the field of synthetic biology are constantly making additions to biological circuit repositories, as well as to the theoretical understanding of their capabilities. The ability to compute with biomolecules has been demonstrated by many synthetic gene networks, but until recently the majority of such models were engineered to implement the functionality of a single circuit part. Purcell et al. have proposed a network capable of multiple functions, switching between three different behaviours in a programmable fashion. This work provides an open-source implementation in which their in silico experiments were replicated.

Relying on a rate constraint to reduce Motion Estimation complexity

PDF
IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)
Abstract: This paper proposes a rate-based candidate elimination strategy for Motion Estimation, which is considered one of the main sources of encoder complexity. We build from findings of previous works that show that selected motion vectors are generally near the predictor to propose a solution that uses the motion vector bitrate to constrain the candidate search to a subset of the original search window, resulting in less distortion computations. The proposed method is not tied to a particular search pattern, which makes it applicable to several ME strategies. The technique was tested in the VVC reference software implementation and showed complexity reductions of over 80% at the cost of an average 0.74% increase in BD-Rate with respect to the original TZ Search algorithm in the LDP configuration.

Eliminação de Candidatos Baseada em Taxa para Algoritmos de Estimação de Movimento na Codificação de Vídeo

PDF
REIC: Artigos do 40º Concurso de Trabalhos de Iniciação Científica (CTIC/CSBC)
Resumo: Este trabalho propõe e avalia uma técnica dedicada à redução do espaço de busca da Estimação de Movimento, uma das etapas mais importantes na codificação de vídeo. Partindo de evidências na literatura que indicariam uma correlação entre o custo estimado da representação de vetores de movimento e as decisões do codificador, o algoritmo proposto utiliza um critério de eliminação de candidatos considerando somente a taxa de bits dos seus respectivos vetores. A técnica foi avaliada no software de referência do padrão VVC e demonstrou, em uma das configurações do codificador, reduções de mais de 80% na área de busca da Estimação de Movimento, com perdas médias na eficiência de codificação de apenas 0,74% em relação ao algoritmo original.