FramewORk for embedded system verification: (competition contribution)

Pablo Gonzalez-De-Aledo, Pablo Sanchez

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

8 Citations (Scopus)

Abstract

Forest is a bounded model checker that implements symbolic execution on top of the LLVM intermediate language and is able to detect errors in programs developed in C. Forest transforms a program into a set of SMT formulas describing each feasible path and decides these formulas with an SMT solver. This enables it to prove the satisfiability of reachability conditions such as the ones presented in SV-COMP. Forest implements different ways of representing SMT formulas: linear arithmetic, polynomials and generic bit-accurate and not bit-accurate representations.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
EditorsChristel Baier, Cesare Tinelli
PublisherSpringer, Springer Nature
Pages429-431
Number of pages3
Volume9035
ISBN (Electronic)9783662466803
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: 11 Apr 201518 Apr 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9035
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
CountryUnited Kingdom
CityLondon
Period11/04/1518/04/15

Fingerprint Dive into the research topics of 'FramewORk for embedded system verification: (competition contribution)'. Together they form a unique fingerprint.

Cite this