Skip to main content
PPGEE/UFAM

Artigo em periódico

Applying symbolic bounded model checking to the 2012 RERS greybox challenge

MORSE, J.2014MORSE, J.; CORDEIRO, L. C.; NICOLE, D.; FISCHER, BERND

2014 • International Journal on Software Tools for Technology Transfer • 8 citações

Resumo

Resumo

We describe the application of ESBMC, a symbolic bounded model checker for C programs, to the 2012 RERS greybox challenge. We checked the reachability properties via reachability of the error labels, and the behavioral properties via a bounded LTL model checking approach. Our approach could solve about 700 properties for the small and medium problems from the offline phase, and scored overall about 5,000 marks but still ranked last in the competition.

palavras-chave

Palavras-chave

ESBMCC programsreachability analysislinear temporal logicbounded model checkingsoftware verification

Volume

16

Número

5

Páginas

519-529

Editora

Springer Science and Business Media LLC

Status

Published

links

DOI

10.1007/s10009-014-0335-0

Link Externo

https://doi.org/10.1007/s10009-014-0335-0

Repositório

https://research.manchester.ac.uk/en/publications/5fcc5d6f-7d64-4f1b-9278-19ebb08c525f

Artigo em periódico

Electrocardiographic signal compression based on distributed source codingDE SOUZA, PATRESE E.B.2027DE SOUZA, PATRESE E.B.; DE LIMA FILHO, EDDIE B.; CORDEIRO, LUCAS C.; DE MELO, WHEIDIMA C.; DA SILVA, WALDIR S.; CARVALHO, CELSO B2027 • Biomedical Signal Processing and Control
Handling Asynchronous Scheduling Functions in Periodic Event-Triggered Gain-Scheduled Control With Guaranteed Polytopic InclusionCOUTINHO, Pedro Henrique Silva2026 COUTINHO, Pedro Henrique Silva; PESSIM, Paulo Sérgio Pereira; BESSA, Iury Valente; PEIXOTO, Márcia Luciana da Costa; PALHARES, Reinaldo Martinez2026 • IEEE Transactions on Cybernetics2citações
Systematic LMI approaches to design multivariable sliding mode controllers for uncertain systemsCOUTINHO, Pedro Henrique Silva2026COUTINHO, Pedro Henrique Silva; BESSA, Iury Valente; RODRIGUES, Victor Hugo Pereira; OLIVEIRA, Tiago Roux2026 • Automatica1citações
Finding software vulnerabilities in large C projects via bounded model checkingDE SOUSA, JANISLLEY O.2026DE SOUSA, JANISLLEY O.; DE FARIAS, BRUNO C.; DA SILVA, THALES A.; TIHANYI, NORBERT; DUBNICZKY, RICHARD A.; FILHO, EDDIE B. L.; CORDEIRO, LUCAS C2026 • International Journal on Software Tools for Technology Transfer

Ver todas as publicações