Reasoning About the Unknown in Static Analysis.
Static program analysis techniques cannot know certain values, such as the value of user input or network state, at analysis time. While such unknown values need to be treated as nondeterministic choices made by the program's execution environment, it is still possible to glean very useful informati...
| Publicado en: | Communications of the ACM Vol. 53; no. 8; pp. 115 - 124 |
|---|---|
| Autores principales: | , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Aug2010
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=52564153&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 52564153 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Aug2010 vid: 53 iid: 8 pid: 68 pub: Association for Computing Machinery artinfo: ui: 52564153 10.1145/1787234.1787259 ppf: 115 ppct: 9 formats: tig: atl: Reasoning About the Unknown in Static Analysis. aug: au: Dillig, Isil Dillig, Thomas Aiken, Alex affil: Computer Science Department, Stanford University. su: Computer software testing Computer software correctness Debugging Computer operating systems Computer software execution Computer logic sug: subj: Computer software testing Computer software correctness Debugging Computer operating systems Computer software execution Computer logic ab: Static program analysis techniques cannot know certain values, such as the value of user input or network state, at analysis time. While such unknown values need to be treated as nondeterministic choices made by the program's execution environment, it is still possible to glean very useful information about how such statically unknown values may or must influence computation. We give a method for integrating such nondeterministic choices with an expressive static analysis. Interestingly, we cannot solve the resulting recursive constraints directly, but we give an exact method for answering all may and must queries. We show experimentally that the resulting solved forms are concise in practice, enabling us to apply the technique to very large programs, including an entire operating system. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2010 holdings: @attributes: islocal: N |
|---|