Búsqueda avanzada

Resultados de búsqueda para SMT

Protocol Analysis with Time and Space

Protocols, Strands, and LogicPages: 22-49Year: 2021DOI:

Autores: Damian Aparicio Sanchez / Santiago Escobar / Catherine Meadows / Julia Sapiña / Jose Meseguer / 
Palabras Clave: cryptographic - Maude-npa - process algebra - protocol - SMT - space - time

Context-based Model Checking using SMT-solvers (Trabajo en progreso)

In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.

Autores: Alex Abuin / Unai Díaz de Cerio / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Model checking - SAT - SMT - Solvers - Tableux

Constrained Dynamic Partial Order Reduction (Trabajo ya publicado)

The cornerstone of dynamic partial order reduction (DPOR) is the notion of independence that is used to decide whether each pair of concurrent events p and t are in a race and thus both p·t and t·p must be explored. We present constrained dynamic partial order reduction (CDPOR), an extension of the DPOR framework which is able to avoid redundant explorations based on the notion of conditional independence —the execution of p and t commutes only when certain independence constraints (ICs) are satisfied. ICs can be declared by the programmer, but importantly, we present a novel SMT-based approach to automatically synthesize ICs in a static pre-analysis. A unique feature of our approach is that we have succeeded to exploit ICs within the state-of-the-art DPOR algorithm, achieving exponential reductions over existing implementations.

Palabras Clave: Conditional Independence - Dynamic Partial Order Reduction - Model checking - SMT - Static Analysis

No encuentra los resultados que busca? Prueba nuestra Búsqueda avanzada