Model Checking: Algorithmic Verification and Debugging.
The authors discuss their formulation of the process of model checking and its historical background. Mathematical logic is used in model checking to confirm that computer program behavior conforms to the correct specifications. While the Floyd-Hoare style deductive verification method was used sinc...
| Published in: | Communications of the ACM Vol. 52; no. 11; pp. 75 - 85 |
|---|---|
| Main Authors: | , , |
| Format: | Article |
| Published: |
Association for Computing Machinery
Nov2009
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=45021159&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 45021159 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Nov2009 vid: 52 iid: 11 pid: 68 pub: Association for Computing Machinery artinfo: ui: 45021159 10.1145/1592761.1592781 ppf: 75 ppct: 10 formats: tig: atl: Model Checking: Algorithmic Verification and Debugging. aug: au: Clarke, Edmund M. Emerson, E. Allen Sifakis, Joseph affil: FORE Systems University Professor, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA. Regents Chair and Professor, Department of Computer Science, University of Texas, Austin, TX. Schneider-INRIA Chair, Verimag Laboratory Gieres, Francea. su: Software verification Computer software correctness Technical specifications Philosophy of mathematics Debugging Computer software testing History sug: subj: Software verification Computer software correctness Technical specifications Philosophy of mathematics Debugging Computer software testing History ab: The authors discuss their formulation of the process of model checking and its historical background. Mathematical logic is used in model checking to confirm that computer program behavior conforms to the correct specifications. While the Floyd-Hoare style deductive verification method was used since the 1960s, it was not useful for large programs. Model checking was devised using temporal logic (TL) that describes change over time. Debugging, correctness, expressiveness, efficiency and accounting for architectures and their features in model checking are detailed. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2009 holdings: @attributes: islocal: N |
|---|