Broom: A Static Analyzer for C Based on Separation Logic and the Principle of Bi-Abductive Reasoning

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F22%3APR36279" target="_blank" >RIV/00216305:26230/22:PR36279 - isvavai.cz</a>

Result on the web

<a href="https://pajda.fit.vutbr.cz/rogalew/broom/-/tree/v0.0.1" target="_blank" >https://pajda.fit.vutbr.cz/rogalew/broom/-/tree/v0.0.1</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Broom: A Static Analyzer for C Based on Separation Logic and the Principle of Bi-Abductive Reasoning

Original language description

Broom is a static analyzer for C written in OCaml. Broom primarily aims at programs that use low-level pointer manipulation to deal with various kinds of linked lists. It is based on separation logic and the principle of bi-abductive reasoning.

Czech name

—

Czech description

—

Type

R - Software

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2022

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Internal product ID

broom

Technical parameters

Software je dostupný pod licencí GPL (http://www.gnu.org/licenses/gpl-3.0.txt). Pro informace o licenčních podmínkách prosím kontaktujte: Ing. Kristýna Dvořáčkova, MSc., Výzkumné centrum informačních technologií, Fakulta informačních technologií VUT v Brně, Božetěchova 2, 612 66 Brno, tel. 541 141 466.

Economical parameters

Software je dostupný pod licencí GPL (http://www.gnu.org/licenses/gpl-3.0.txt).

Owner IČO

00216305

Owner name

Vysoké učení technické v Brně