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, such as model checking, that<br>produce counterexamples when verification fails are a clear example of<br>the duality of testing and proving. The combination of static<br>techniques such as satisfiability modulo theory and predicate<br>abstraction has provided means of proving correctness by complementing<br>exhaustive enumeration testing–like techniques. More practically,<br>testing supports the cost–effective debugging of complex models and<br>formal specifications, and is applicable in conditions that are beyond<br>the reach of formal techniques –– for example, components whose source<br>code is not accessible. Testing and proving are increasingly seen as<br>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>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 (theorem proving, model checking, symbolic<br>execution, SMT solving, constraint logic programming, etc.) to<br>support testing: generating testing inputs and oracles, supporting<br>coverage criteria, and so on.<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>– Model–based testing and verification<br>– Using model checking to generate test cases<br>– Testing of verification tools and environments<br>– Applications of testing and proving to new domains, such as<br>security, configuration management, and language–based techniques<br>– Bridging the gap between concrete and symbolic reasoning techniques<br>– Innovative approaches to verification such as crowdsourcing and<br>serious games<br>– Case studies, tool and framework descriptions, and experience<br>reports about combining tests and proofs<br>
Abbrevation
iFM
City
Marburg
Country
Germany
Deadline Paper
Start Date
End Date
Abstract