Squeeze All the Power Out of Your Hardware to Verify Your Software!

BARNAT, Jiří a Luboš BRIM. Squeeze All the Power Out of Your Hardware to Verify Your Software! In Leveraging Applications of Formal Methods, Verification and Validation. Berlin Heidelberg: Springer, 2008, s. 604-618. ISBN 978-3-540-88478-1.

Základní údaje

Originální název

Squeeze All the Power Out of Your Hardware to Verify Your Software!

Název česky

Vymačkejte veškerou šťávu svého hardware pro verifikovaci vašeho software

Autoři

BARNAT, Jiří (203 Česká republika, garant) a Luboš BRIM (203 Česká republika)

Vydání

Berlin Heidelberg, Leveraging Applications of Formal Methods, Verification and Validation, od s. 604-618, 15 s. 2008

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Řecko

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/08:00024322

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-88478-1

ISSN

UT WoS

000261596900042

Klíčová slova anglicky

Parallel; LTL Model Checking;

Štítky

LTL model checking, parallel

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

The computer industry is undergoing a paradigm shift. Chip manufacturers are shifting development resources away from single- processor chips to a new generation of multi-processor chips, huge clusters of multi-core workstations are easily accessible everywhere, external memory devices, such as hard disks or solid state disks, are getting more powerful both in terms of capacity and access speed. This fundamental technological shift in core computing architecture will require a fundamental change in how we ensure the quality of software. The key issue is that verification techniques need to undergo a similarly deep technological transition to catch up with the complexity of software designed for the new hardware. In this position paper we would like to advocate the necessity of fully exploiting the power offered by the new computer hardware to make the verification techniques capable of handling next-generation software.

Česky

Počítačový průmysl prochází změnou paradigmatu. Výrobci HW dnes zdokonalují výkon svých čipů spíše než zrychlováním jednoho CPU jádra spíše zaváděním více jader do jednoho CPU. Navíc jsou běžně dostupné klastry pracovních stanic, výkoné a extrémně velké externí paměťová zařízení. Tato technologická změna vyžaduje fundamentální změnu ve způsobu, kterým je zajišťována kvalita software. V tomto článku obhajujeme potřebu změny dosud používaných algoritmů pro verifikaci software.

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky