Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
Software model checkers are able to exhaustively explore different bounded program executions arising from various sources of nondeterminism. These tools provide statements to produce non-determinis- tic values for certain variables, thus forcing the corresponding model checker to consider all possi...
Guardado en:
| Autores principales: | Ponzio, Pablo Daniel, Godio, Ariel, Rosner, Nicolás, Arroyo, Marcelo, Aguirre, Nazareno Matías, Frias, Marcelo F. |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Español |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/140433 http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-12.pdf |
| Aporte de: |
Ejemplares similares
-
TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
por: Galeotti, Juan Pablo, et al.
Publicado: (2013) -
TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds
por: Galeotti, J.P., et al. -
Analysis of invariants for efficient bounded verification
por: Galeotti, Juan Pablo, et al.
Publicado: (2010) -
BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support
por: Rosner, Nicolás, et al.
Publicado: (2015) -
Analysis of invariants for efficient bounded verification
por: Galeotti, J.P., et al.