Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

9

CAV
2010
Springer

favoriteEmaildiscussreport

176views Hardware» more CAV 2010»

Lazy Annotation for Program Testing and Verification

13 years 7 months ago

Lazy Annotation for Program Testing and Verification

Download www.kenmcmil.com

Abstract. We describe an interpolant-based approach to test generation and model checking for sequential programs. The method generates Floyd/Hoare style annotations of the program on demand, as a result of failure to achieve goals, in a manner analogous to conflict clause learning in a DPLL style SAT solver.

Kenneth L. McMillan

Real-time Traffic

CAV 2010 | Floyd/Hoare Style Annotations | Hardware | Model Checking | Test Generation |

claim paper

Related Content

» Test Data Generation for Programs with Quantified FirstOrder Logic Specifications

» Creating and Visualizing Test Data from Programming Exercises

» An Integrated Approach to High Integrity Software Verification

» TypeBased Automated Verification of Authenticity in Cryptographic Protocols

» Computing Stack Maps with Interfaces

» Quantitative verification models techniques and tools

» Model Checking of Linearizability of Concurrent List Implementations

» Invariant inference for static checking

» Securing web application code by static analysis and runtime protection

Post Info
More Details (n/a)

Added	29 Sep 2010
Updated	29 Sep 2010
Type	Conference
Year	2010
Where	CAV
Authors	Kenneth L. McMillan

Comments (0)