Catálogo de publicaciones - libros
Título de Acceso Abierto
Tools and Algorithms for the Construction and Analysis of Systems: Tools and Algorithms for the Construction and Analysis of Systems
Parte de: Theoretical Computer Science and General Issues
En conferencia: 24º International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . Thessaloniki, Greece . April 14, 2018 - April 20, 2018
Resumen/Descripción – provisto por la editorial
No disponible.
Palabras clave – provistas por la editorial
computer architecture; computer software selection and evaluation; formal logic; formal methods; model checker; model checking; multi core processors; program compilers; programming languages; semantics; software engineering; specifications; state space; verification
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No requiere | 2018 | Directory of Open access Books |
| |
| No requiere | 2018 | SpringerLink |
|
Información
Tipo de recurso:
libros
ISBN impreso
978-3-319-89962-6
ISBN electrónico
978-3-319-89963-3
Editor responsable
Springer Nature
País de edición
Reino Unido
Fecha de publicación
2018
Tabla de contenidos
Ultimate Taipan with Dynamic Block Encoding
Daniel Dietsch; Marius Greitschus; Matthias Heizmann; Jochen Hoenicke; Alexander Nutz; Andreas Podelski; Christian Schilling; Tanja Schindler
is a software model checker that uses trace abstraction and abstract interpretation to prove correctness of programs. In contrast to previous versions, now uses dynamic block encoding to obtain the best precision possible when evaluating transition formulas of large block encoded programs.
- 7th Competition on Software Verification (SV-COMP) | Pp. 452-456
VeriAbs: Verification by Abstraction and Test Generation
Priyanka Darke; Sumanth Prabhu; Bharti Chimdyalwar; Avriti Chauhan; Shrawan Kumar; Animesh Basakchowdhury; R. Venkatesh; Advaita Datar; Raveendra Kumar Medicherla
VeriAbs is a portfolio software verifier for ANSI-C programs. To prove properties with better efficiency and scalability, this version implements output abstraction with -induction in the presence of resets. VeriAbs now generates post conditions over the abstraction to find invariants by applying Z3’s tactics of quantifier elimination. These invariants are then used to generate validation witnesses. To find errors in the absence of known program bounds, VeriAbs searches for property violating inputs by applying random test generation with fuzz testing for a better scalability as compared to bounded model checking.
- 7th Competition on Software Verification (SV-COMP) | Pp. 457-462