Tomb et al., 2012 - Google Patents
Detecting inconsistencies via universal reachability analysisTomb et al., 2012
View PDF- Document ID
- 16789294027807593550
- Author
- Tomb A
- Flanagan C
- Publication year
- Publication venue
- Proceedings of the 2012 International Symposium on Software Testing and Analysis
External Links
Snippet
Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally …
- 238000004458 analytical method 0 title abstract description 80
Classifications
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/3604—Software analysis for verifying properties of programs
- G06F11/3608—Software analysis for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/3604—Software analysis for verifying properties of programs
- G06F11/3612—Software analysis for verifying properties of programs by runtime analysis
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
- G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
- G06F21/55—Detecting local intrusion or implementing counter-measures
- G06F21/56—Computer malware detection or handling, e.g. anti-virus arrangements
- G06F21/562—Static detection
- G06F21/563—Static detection by source code analysis
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F8/00—Arrangements for software engineering
- G06F8/40—Transformations of program code
- G06F8/41—Compilation
- G06F8/43—Checking; Contextual analysis
- G06F8/436—Semantic checking
- G06F8/437—Type checking
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/362—Software debugging
- G06F11/3636—Software debugging by tracing the execution of the program
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/36—Preventing errors by testing or debugging software
- G06F11/3668—Software testing
- G06F11/3672—Test management
- G06F11/3676—Test management for coverage analysis
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
- G06F21/50—Monitoring users, programs or devices to maintain the integrity of platforms, e.g. of processors, firmware or operating systems
- G06F21/57—Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities
- G06F21/577—Assessing vulnerabilities and evaluating computer system security
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/30—Monitoring
- G06F11/34—Recording or statistical evaluation of computer activity, e.g. of down time, of input/output operation; Recording or statistical evaluation of user activity, e.g. usability assessment
- G06F11/3466—Performance evaluation by tracing or monitoring
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F9/00—Arrangements for programme control, e.g. control unit
- G06F9/06—Arrangements for programme control, e.g. control unit using stored programme, i.e. using internal store of processing equipment to receive and retain programme
- G06F9/44—Arrangements for executing specific programmes
- G06F9/445—Programme loading or initiating
- G06F9/44589—Programme code verification, e.g. Java bytecode verification, proof-carrying code
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/07—Error detection; Error correction; Monitoring responding to the occurence of a fault, e.g. fault tolerance
- G06F11/0703—Error or fault processing not based on redundancy, i.e. by taking additional measures to deal with the error or fault not making use of redundancy in operation, in hardware, or in data representation
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F8/00—Arrangements for software engineering
- G06F8/70—Software maintenance or management
- G06F8/75—Structural analysis for program understanding
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F17/00—Digital computing or data processing equipment or methods, specially adapted for specific functions
- G06F17/50—Computer-aided design
- G06F17/5009—Computer-aided design using simulation
- G06F17/504—Formal methods
-
- G—PHYSICS
- G06—COMPUTING; CALCULATING; COUNTING
- G06F—ELECTRICAL DIGITAL DATA PROCESSING
- G06F2201/00—Indexing scheme relating to error detection, to error correction, and to monitoring
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| Baldoni et al. | A survey of symbolic execution techniques | |
| Csallner et al. | Check'n'crash: combining static checking and testing | |
| Khurshid et al. | TestEra: Specification-based testing of Java programs using SAT | |
| Møller et al. | Static program analysis | |
| Snelting et al. | Efficient path conditions in dependence graphs for software safety analysis | |
| Xie et al. | Saturn: A scalable framework for error detection using boolean satisfiability | |
| Rodrigues et al. | A fast and low-overhead technique to secure programs against integer overflows | |
| Xie et al. | Archer: using symbolic, path-sensitive analysis to detect memory access errors | |
| D'silva et al. | A survey of automated techniques for formal software verification | |
| Dor et al. | CSSV: Towards a realistic tool for statically detecting all buffer overflows in C | |
| Regehr et al. | Eliminating stack overflow by abstract interpretation | |
| Chin et al. | Semantic type qualifiers | |
| Foster et al. | Flow-insensitive type qualifiers | |
| Sotirov | Automatic vulnerability detection using static source code analysis | |
| Godefroid et al. | Statically validating must summaries for incremental compositional dynamic test generation | |
| Devecsery et al. | Optimistic hybrid analysis: Accelerating dynamic analysis through predicated static analysis | |
| Ye et al. | Accelerating dynamic detection of uses of undefined values with static value-flow analysis | |
| Alberti et al. | An extension of lazy abstraction with interpolation for programs with arrays | |
| Even-Mendoza et al. | CsmithEdge: more effective compiler testing by handling undefined behaviour less conservatively | |
| Tomb et al. | Detecting inconsistencies via universal reachability analysis | |
| Moy et al. | Modular inference of subprogram contracts for safety checking | |
| Schmid et al. | Smt-based checking of predicate-qualified types for scala | |
| Khoo et al. | Mixing type checking and symbolic execution | |
| Yang et al. | Object model construction for inheritance in C++ and its applications to program analysis | |
| Maurer | Holmes: Binary analysis integration through datalog |