Knowledge

Polyspace

Source 📝

496: 132: 212:-based static code analysis to verify program execution at the language level. The tool checks each code instruction by taking into account all possible values of every variable at every point in the code, providing a formal diagnostic for each operation in the code under both normal and abnormal usage conditions. 215:
The Bug Finder module identifies software bugs by performing static program analysis on source code. It finds defects such as numerical computation, programming, memory, and other errors. It also produces software metrics such as Comment density of a source file, Cyclomatic complexity, Number of
192:, and others could occur. Software developers and quality assurance managers use this information to identify which parts of the code are faulty or proven to be reliable. Other parts of the code are marked for unproven checks and deserve individual review. 207:
The product family consists of Polyspace Code Prover and Polyspace Bug Finder. The Code Prover module annotates source code with a color-coding scheme to indicate the status of each element in the code. It uses
418: 245: 199:
attempt to address code quality, portability, and reliability. The product checks C and C++ source code for conformance to a subset of rules in these coding standards.
282: 511: 225: 379: 269: 521: 249: 516: 441:"Static Analysis of Dynamic Properties - Automatic Program Verification to Prove the Absence of Dynamic Runtime Errors" 48: 157: 338:
Brat, Guillaume (2004). "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software".
149: 289: 145: 440: 314: 160:
programming languages. The tool also checks source code for adherence to appropriate code standards.
103: 91: 383: 181: 131: 86: 216:
lines, parameters, call levels, etc. in a function, Identified run-time errors in the software.
172:, which was acquired by MathWorks in 2007. The product was subsequently integrated into MATLAB. 404: 355: 347: 189: 98: 74: 464: 351: 495: 180:
Polyspace examines the source code to determine where potential run-time errors such as
209: 185: 79: 505: 489: 114: 148:
to detect, or prove the absence of, certain run-time errors in source code for the
419:"A Formal Methods-based verification approach to medical device software analysis" 32: 360: 37: 380:"Exponent's Investigation of Toyota ETCS-i Vehicle Hardware and Software" 196: 20: 153: 144:
is a static code analysis tool for large-scale analysis by
168:
Polyspace was originally developed by the French company
417:
Jones, Paul; Jetley, Raoul; Abraham, Jay (2010-02-09).
109: 97: 85: 73: 47: 31: 373: 371: 315:"The Mathworks acquires PolySpace Technologies" 246:"The Mathworks acquires PolySpace Technologies" 8: 26: 19:For the computational complexity class, see 283:"Static Verification of Dynamic Properties" 494: 130: 25: 359: 288:. Polyspace Technologies. Archived from 270:The MathWorks - Polyspace - Requirements 236: 446:. Workshop on Applied Program Analysis 226:List of tools for static code analysis 54:R2022b / September 15, 2022 195:Code standards or guidelines such as 7: 313:Pelé, Anne-Françoise (2007-04-25). 244:Pele, Anne-Francoise (2007-04-25). 352:10.1023/B:FORM.0000040027.28662.a4 14: 340:Formal Methods in System Design 1: 512:Static program analysis tools 439:Wissing, Klaus (2007-09-27). 281:Deutsch, Alain (2003-11-27). 16:Static program analysis tool 538: 382:. Exponent. Archived from 18: 465:"Software Metrics-MATLAB" 421:. Embedded Systems Design 248:. EETimes. Archived from 69: 43: 522:Abstract interpretation 378:Exponent (2012-09-24). 146:abstract interpretation 517:Software testing tools 170:PolySpace Technologies 56:; 2 years ago 405:static code analysis 92:static code analysis 182:arithmetic overflow 28: 467:. India: MathWorks 139: 138: 529: 498: 493: 492: 490:Official website 476: 475: 473: 472: 461: 455: 454: 452: 451: 445: 436: 430: 429: 427: 426: 414: 408: 401: 395: 394: 392: 391: 375: 366: 365: 363: 361:2060/20040010327 346:(2/3): 167–198. 335: 329: 328: 326: 325: 310: 304: 303: 301: 300: 294: 287: 278: 272: 267: 261: 260: 258: 257: 241: 190:division by zero 135: 134: 127: 124: 122: 120: 118: 116: 75:Operating system 64: 62: 57: 29: 537: 536: 532: 531: 530: 528: 527: 526: 502: 501: 488: 487: 484: 479: 470: 468: 463: 462: 458: 449: 447: 443: 438: 437: 433: 424: 422: 416: 415: 411: 402: 398: 389: 387: 377: 376: 369: 337: 336: 332: 323: 321: 312: 311: 307: 298: 296: 292: 285: 280: 279: 275: 268: 264: 255: 253: 243: 242: 238: 234: 222: 205: 178: 166: 129: 113: 65: 60: 58: 55: 24: 17: 12: 11: 5: 535: 533: 525: 524: 519: 514: 504: 503: 500: 499: 483: 482:External links 480: 478: 477: 456: 431: 409: 396: 367: 330: 305: 273: 262: 235: 233: 230: 229: 228: 221: 218: 210:formal methods 204: 201: 186:buffer overrun 177: 174: 165: 162: 137: 136: 111: 107: 106: 101: 95: 94: 89: 83: 82: 80:Cross-platform 77: 71: 70: 67: 66: 53: 51: 49:Stable release 45: 44: 41: 40: 35: 15: 13: 10: 9: 6: 4: 3: 2: 534: 523: 520: 518: 515: 513: 510: 509: 507: 497: 491: 486: 485: 481: 466: 460: 457: 442: 435: 432: 420: 413: 410: 406: 400: 397: 386:on 2014-07-27 385: 381: 374: 372: 368: 362: 357: 353: 349: 345: 341: 334: 331: 320: 316: 309: 306: 295:on 2012-03-13 291: 284: 277: 274: 271: 266: 263: 252:on 2012-02-11 251: 247: 240: 237: 231: 227: 224: 223: 219: 217: 213: 211: 202: 200: 198: 193: 191: 187: 183: 175: 173: 171: 163: 161: 159: 155: 151: 147: 143: 133: 126: 112: 108: 105: 102: 100: 96: 93: 90: 88: 84: 81: 78: 76: 72: 68: 52: 50: 46: 42: 39: 36: 34: 30: 22: 469:. Retrieved 459: 448:. Retrieved 434: 423:. Retrieved 412: 399: 388:. Retrieved 384:the original 343: 339: 333: 322:. Retrieved 318: 308: 297:. Retrieved 290:the original 276: 265: 254:. Retrieved 250:the original 239: 214: 206: 203:Capabilities 194: 179: 169: 167: 141: 140: 33:Developer(s) 403:MathWorks: 176:Common uses 104:Proprietary 506:Categories 471:2015-08-27 450:2010-08-13 425:2010-08-16 390:2010-09-07 324:2024-07-12 299:2014-05-17 256:2010-08-13 232:References 123:/polyspace 117:.mathworks 61:2022-09-15 142:Polyspace 121:/products 38:MathWorks 27:Polyspace 319:EE Times 220:See also 197:MISRA C 164:History 110:Website 99:License 59: ( 156:, and 128:  21:PSPACE 444:(PDF) 293:(PDF) 286:(PDF) 125:.html 119:.com 87:Type 356:hdl 348:doi 158:Ada 154:C++ 115:www 508:: 370:^ 354:. 344:25 342:. 317:. 188:, 184:, 152:, 474:. 453:. 428:. 407:. 393:. 364:. 358:: 350:: 327:. 302:. 259:. 150:C 63:) 23:.

Index

PSPACE
Developer(s)
MathWorks
Stable release
Operating system
Cross-platform
Type
static code analysis
License
Proprietary
www.mathworks.com/products/polyspace.html
Edit this on Wikidata
abstract interpretation
C
C++
Ada
arithmetic overflow
buffer overrun
division by zero
MISRA C
formal methods
List of tools for static code analysis
"The Mathworks acquires PolySpace Technologies"
the original
The MathWorks - Polyspace - Requirements
"Static Verification of Dynamic Properties"
the original
"The Mathworks acquires PolySpace Technologies"
doi
10.1023/B:FORM.0000040027.28662.a4

Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.