Rewriting modulo SMT and open system analysis

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nond...

Full description

Autores:

Rocha, Camilo
Meseguer, José
Muñoz, César

Tipo de recurso:

Article of journal

Fecha de publicación:

2016

Institución:

Escuela Colombiana de Ingeniería Julio Garavito

Repositorio:

Repositorio Institucional ECI

Idioma:

eng

OAI Identifier:

oai:repositorio.escuelaing.edu.co:001/1866

Acceso en línea:

https://repositorio.escuelaing.edu.co/handle/001/1866

Palabra clave:

Relaciones de conjuntos sincrónicos
Semántica síncrona
Reescritura de lógica
Simulación formal y verificación
Synchronous set relations
Synchronous semantics
Rewriting logic
Formal simulation and verification
PLEXIL

Rights

openAccess

License

© 2016 Elsevier Inc. All rights reserved.