BLAST modell checker
| Originalförfattare | Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley |
|---|---|
| Utvecklare | Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institutet för systemprogrammering |
| Stabil frisättning | 2.7.3 / 30 oktober 2015
|
| Skrivet i | Ocaml |
| Operativ system | Linux |
| Typ | Statisk kodanalys |
| Licens | Apache-licens, version 2.0 |
| Hemsida |
Berkeley Lazy Abstraction Software Verification Tool ( BLAST ) är ett kontrollverktyg för mjukvarumodeller för C-program . Uppgiften som tas upp av BLAST är behovet av att kontrollera om programvaran uppfyller beteendekraven för dess tillhörande gränssnitt. BLAST använder motexempel -driven automatisk abstraktionsförfining för att konstruera en abstrakt modell som sedan modellkontrolleras för säkerhetsegenskaper. Abstraktionen är konstruerad i farten och endast med den precision som efterfrågas .
Prestationer
BLAST kom först i kategorin DeviceDrivers64 i den första tävlingen om mjukvaruverifiering (2012) som hölls på TACAS 2012 i Tallinn .
BLAST kom trea (kategori DeviceDrivers64) i den andra tävlingen om mjukvaruverifiering (2013) som hölls på TACAS 2013 i Rom .
BLAST kom först i kategorin DeviceDrivers64 i den tredje tävlingen om mjukvaruverifiering (2014) som hölls på TACAS 2014 i Grenoble .
- Anteckningar
- Pavel Shved; Mikhail Mandrykin; Vadim Mutilin (2012). "Predikatanalys med BLAST 2.7.". I Flanagan, Cormac; König, Barbara (red.). Verktyg och algoritmer för konstruktion och analys av system . Föreläsningsanteckningar i datavetenskap. Vol. 7214. Springer-Verlag. s. 525–527. ISBN 978-3-642-28756-5 .
- Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak (2007). "The Software Model Checker Blast". International Journal on Software Tools for Technology Transfer . 9 (5–6): 505–525. doi : 10.1007/s10009-007-0044-z . S2CID 1662778 .
- Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar & Gregoire Sutre (2003). "Programverifiering med Blast". I Ball, Thomas & Rajamani, Sriram K. (red.). Handlingar från den 10:e SPIN-workshopen om programvara för modellkontroll (SPIN 2003) . Föreläsningsanteckningar i datavetenskap. Vol. 2648. Springer-Verlag. s. 235–239. ISBN 3-540-40117-2 .
externa länkar