Automated deduction for verification Export

@article{Shankar09, abstract = {Automated deduction uses computation to perform symbolic logical reasoning. It has been a core technology for program verification from the very beginning. Satisfiability solvers for propositional and first-order logic significantly automate the task of deductive program verification. We introduce some of the basic deduction techniques used in software and hardware verification and outline the theoretical and engineering issues in building deductive verification tools. Beyond verification, deduction techniques can also be used to support a variety of applications including planning, program optimization, and program synthesis.}, address = {New York, NY, USA}, author = {Shankar, Natarajan}, citeulike-article-id = {5973437}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1592434.1592437}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1592434.1592437}, doi = {10.1145/1592434.1592437}, issn = {0360-0300}, journal = {ACM Computing Surveys}, keywords = {2009, automatic, hardware, logic, reasoning, sat-solver, software, verification}, number = {4}, pages = {1--56}, posted-at = {2009-10-20 10:23:09}, priority = {2}, publisher = {ACM}, title = {Automated deduction for verification}, url = {http://dx.doi.org/10.1145/1592434.1592437}, volume = {41}, year = {2009} }

TY - JOUR ID - Shankar09 L3 - citeulike-article-id:5973437 N2 - Automated deduction uses computation to perform symbolic logical reasoning. It has been a core technology for program verification from the very beginning. Satisfiability solvers for propositional and first-order logic significantly automate the task of deductive program verification. We introduce some of the basic deduction techniques used in software and hardware verification and outline the theoretical and engineering issues in building deductive verification tools. Beyond verification, deduction techniques can also be used to support a variety of applications including planning, program optimization, and program synthesis. IS - 4 JF - ACM Computing Surveys SN - 0360-0300 AD - New York, NY, USA EP - 56 TI - Automated deduction for verification PB - ACM VL - 41 SP - 1 KW - 2009 KW - automatic KW - hardware KW - logic KW - reasoning KW - sat-solver KW - software KW - verification AU - Shankar, Natarajan PY - 2009/// UR - http://dx.doi.org/10.1145/1592434.1592437 ER -