%0 Journal Article %1 1175942 %A Jackson, Michael %C Los Alamitos, CA, USA %D 2006 %I IEEE Computer Society Press %J Computer %K phd %N 10 %P 65--71 %R http://dx.doi.org/10.1109/MC.2006.363 %T What Can We Expect from Program Verification? %U http://portal.acm.org/citation.cfm?id=1175942&coll=GUIDE&dl=GUIDE&CFID=46688192&CFTOKEN=39233820 %V 39 %X Program verification assumes a formal program specification. In software-intensive systems,such specifications must depend on formalization of the natural, nonformal problem world.This formalization is inevitably imperfect and poses major difficulties of structure andreasoning. Appropriate verification tools can help address these difficulties and improvesystem reliability.

@article{1175942, abstract = {Program verification assumes a formal program specification. In software-intensive systems,such specifications must depend on formalization of the natural, nonformal problem world.This formalization is inevitably imperfect and poses major difficulties of structure andreasoning. Appropriate verification tools can help address these difficulties and improvesystem reliability.}, added-at = {2007-12-13T15:25:59.000+0100}, address = {Los Alamitos, CA, USA}, author = {Jackson, Michael}, biburl = {https://www.bibsonomy.org/bibtex/2436af08fd02dd8e6f341743cebf83881/cedricmesnage}, description = {What Can We Expect from Program Verification?}, doi = {http://dx.doi.org/10.1109/MC.2006.363}, interhash = {df7e27a9b3dcefc027c564feb9b58e61}, intrahash = {436af08fd02dd8e6f341743cebf83881}, issn = {0018-9162}, journal = {Computer}, keywords = {phd}, number = 10, pages = {65--71}, publisher = {IEEE Computer Society Press}, timestamp = {2007-12-13T15:25:59.000+0100}, title = {What Can We Expect from Program Verification?}, url = {http://portal.acm.org/citation.cfm?id=1175942&coll=GUIDE&dl=GUIDE&CFID=46688192&CFTOKEN=39233820}, volume = 39, year = 2006 }