The TAP conference promotes research in verification and formal<br>methods that targets the interplay of proofs and testing: the<br>advancement of techniques of each kind and their combination, with the<br>ultimate goal of improving software and system dependability.<br>Research in verification has recently seen a steady convergence of<br>heterogeneous techniques and a synergy between the traditionally<br>distinct areas of testing (and dynamic analysis) and of proving (and<br>static analysis). Formal techniques for counter–example generation<br>based on, for example, symbolic execution, SAT/SMT–solving or<br>model checking, furnish evidence for the potential of a combination of<br>test and proof. The combination of predicate abstraction with testing–like<br>techniques based on exhaustive enumeration opens the perspective<br>for novel techniques of proving correctness. On the practical side,<br>testing offers cost–effective debugging techniques of specifications<br>or crucial parts of program proofs (such as invariants). Last but not<br>least, testing is indispensable when it comes to the validation of the<br>underlying assumptions of complex system models involving<br>hardware and/or system environments. Over the years, there is<br>growing acceptance in research communities that testing and proving<br>are complementary rather than mutually exclusive techniques.<br>The TAP conference aims to promote research in the intersection of<br>testing and proving by bringing together researchers and practitioners<br>from both areas of verification.<br>Topics of Interest<br>––––––––––––––––––<br>TAP′s scope encompasses many aspects of verification technology,<br>including foundational work, tool development, and empirical<br>research. Its topics of interest center around the connection between<br>proofs (and other static techniques) and testing (and other dynamic<br>techniques). Papers are solicited on, but not limited to, the<br>following topics:<br>– Verification and analysis techniques combining proofs and tests<br>– Program proving with the aid of testing techniques<br>– Deductive techniques supporting the automated generation of test vectors and oracles<br>(theorem proving, model checking, symbolic execution, SAT/SMT solving, constraint logic programming, etc.)<br>– Deductive techniques supporting novel definitions of coverage criteria,<br>– Program analysis techniques combining static and dynamic analysis<br>– Specification inference by deductive and dynamic methods<br>– Testing and runtime analysis of formal specifications<br>– Search–based technics for proving and testing<br>– Verification of verification tools and environments<br>– Applications of test and proof techniques in new domains,<br>such as security, configuration management, learning<br>– Combined approaches of test and proof in the context of formal<br>certifications (Common Criteria, CENELEC, …)<br>– Case studies, tool and framework descriptions, and experience<br>reports about combining tests and proofs<br>
Abbrevation
TAP
City
Toulouse
Country
France
Deadline Paper
Start Date
End Date
Abstract