400:
441:
354:
Thomas A. Henzinger; Ranjit Jhala; Rupak
Majumdar & Gregoire Sutre (2003). "Software Verification with Blast". In Ball, Thomas & Rajamani, Sriram K. (eds.).
475:
168:-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed
164:. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs
480:
434:
470:
313:
460:
256:
304:
Pavel Shved; Mikhail
Mandrykin; Vadim Mutilin (2012). "Predicate Analysis with BLAST 2.7.". In Flanagan, Cormac; König, Barbara (eds.).
198:
BLAST came first in the category DeviceDrivers64 in the 3rd
Competition on Software Verification (2014), that was held at TACAS 2014 in
184:
BLAST came first in the category DeviceDrivers64 in the 1st
Competition on Software Verification (2012) that was held at TACAS 2012 in
427:
28:
278:
363:
234:
191:
BLAST came third (category DeviceDrivers64) in the 2nd
Competition on Software Verification (2013) that was held at TACAS 2013 in
41:
52:
286:
Proceedings of the 20th
International Conference on Tools and Algorithms for the Construction and of Analysis Systems
264:
Proceedings of the 19th
International Conference on Tools and Algorithms for the Construction and of Analysis Systems
242:
Proceedings of the 18th
International Conference on Tools and Algorithms for the Construction and of Analysis Systems
161:
325:
Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak (2007). "The
Software Model Checker Blast".
465:
117:
173:
105:
100:
342:
359:
309:
411:
407:
334:
112:
88:
358:. Lecture Notes in Computer Science. Vol. 2648. Springer-Verlag. pp. 235–239.
308:. Lecture Notes in Computer Science. Vol. 7214. Springer-Verlag. pp. 525–527.
165:
157:
454:
346:
399:
338:
219:
169:
35:
22:
356:
Proceedings of the 10th SPIN Workshop on Model
Checking Software (SPIN 2003)
380:
385:
199:
154:
128:
257:"Second Competition on Software Verification (Summary of SV-COMP 2013)"
185:
279:"Third Competition on Software Verification (Summary of SV-COMP 2014)"
93:
81:
306:
Tools and Algorithms for the Construction and Analysis of Systems
192:
327:
International Journal on Software Tools for Technology Transfer
27:
Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar,
415:
147:
Berkeley Lazy Abstraction Software verification Tool
123:
111:
99:
87:
77:
51:
34:
21:
235:"Competition on Software Verification (SV-COMP)"
40:Mikhail Mandrykin, Vadim Mutilin, Pavel Shved,
435:
8:
16:
442:
428:
15:
211:
220:"Files - BLAST - Open-Source Projects"
7:
396:
394:
414:. You can help Knowledge (XXG) by
14:
476:Software using the Apache license
398:
42:Institute for System Programming
481:Computer programming tool stubs
58:2.7.3 / 30 October 2015
288:. Springer-Verlag, Heidelberg.
266:. Springer-Verlag, Heidelberg.
244:. Springer-Verlag, Heidelberg.
1:
471:Static program analysis tools
172:, and only to the requested
461:Free software testing tools
118:Apache License, Version 2.0
497:
393:
339:10.1007/s10009-007-0044-z
73:
47:
410:-related article is a
60:; 8 years ago
106:Static code analysis
277:Dirk Beyer (2014).
255:Dirk Beyer (2013).
233:Dirk Beyer (2012).
18:
23:Original author(s)
423:
422:
386:BLAST 2.7 website
381:BLAST 2.5 website
315:978-3-642-28756-5
143:
142:
488:
444:
437:
430:
408:programming-tool
402:
395:
369:
350:
333:(5–6): 505–525.
319:
290:
289:
283:
274:
268:
267:
261:
252:
246:
245:
239:
230:
224:
223:
216:
139:
136:
134:
132:
130:
89:Operating system
68:
66:
61:
19:
496:
495:
491:
490:
489:
487:
486:
485:
451:
450:
449:
448:
391:
377:
372:
366:
353:
324:
316:
303:
294:
293:
281:
276:
275:
271:
259:
254:
253:
249:
237:
232:
231:
227:
218:
217:
213:
208:
182:
127:
69:
64:
62:
59:
12:
11:
5:
494:
492:
484:
483:
478:
473:
468:
466:Model checkers
463:
453:
452:
447:
446:
439:
432:
424:
421:
420:
403:
389:
388:
383:
376:
375:External links
373:
371:
370:
364:
351:
321:
320:
314:
300:
299:
298:
292:
291:
269:
247:
225:
210:
209:
207:
204:
181:
178:
166:counterexample
158:model checking
141:
140:
125:
121:
120:
115:
109:
108:
103:
97:
96:
91:
85:
84:
79:
75:
74:
71:
70:
57:
55:
53:Stable release
49:
48:
45:
44:
38:
32:
31:
25:
13:
10:
9:
6:
4:
3:
2:
493:
482:
479:
477:
474:
472:
469:
467:
464:
462:
459:
458:
456:
445:
440:
438:
433:
431:
426:
425:
419:
417:
413:
409:
404:
401:
397:
392:
387:
384:
382:
379:
378:
374:
367:
365:3-540-40117-2
361:
357:
352:
348:
344:
340:
336:
332:
328:
323:
322:
317:
311:
307:
302:
301:
296:
295:
287:
280:
273:
270:
265:
258:
251:
248:
243:
236:
229:
226:
221:
215:
212:
205:
203:
201:
196:
194:
189:
187:
179:
177:
175:
171:
167:
163:
159:
156:
152:
148:
138:
126:
122:
119:
116:
114:
110:
107:
104:
102:
98:
95:
92:
90:
86:
83:
80:
76:
72:
56:
54:
50:
46:
43:
39:
37:
33:
30:
26:
24:
20:
416:expanding it
405:
390:
355:
330:
326:
305:
285:
272:
263:
250:
241:
228:
214:
197:
190:
183:
180:Achievements
150:
146:
144:
36:Developer(s)
455:Categories
206:References
170:on the fly
162:C programs
78:Written in
65:2015-10-30
174:precision
160:tool for
135:/projects
200:Grenoble
155:software
29:Berkeley
347:1662778
186:Tallinn
153:) is a
131:.ispras
124:Website
113:License
63: (
362:
345:
312:
137:/blast
406:This
343:S2CID
297:Notes
282:(PDF)
260:(PDF)
238:(PDF)
151:BLAST
129:forge
94:Linux
82:OCaml
17:BLAST
412:stub
360:ISBN
310:ISBN
193:Rome
145:The
101:Type
335:doi
133:.ru
457::
341:.
329:.
284:.
262:.
240:.
202:.
195:.
188:.
176:.
443:e
436:t
429:v
418:.
368:.
349:.
337::
331:9
318:.
222:.
149:(
67:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.