Abbrevation
iFM
City
Marburg
Country
Germany
Deadline Paper
Start Date
End Date
Abstract

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&#046;<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)&#046; 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&#046; 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&#8211;like techniques&#046; More practically,<br>testing supports the cost&#8211;effective debugging of complex models and<br>formal specifications, and is applicable in conditions that are beyond<br>the reach of formal techniques &#8211;&#8211; for example, components whose source<br>code is not accessible&#046; Testing and proving are increasingly seen as<br>complementary rather than mutually exclusive techniques&#046;<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&#046;<br>Topics of Interest<br>TAP&#8242;s scope encompasses many aspects of verification technology,<br>including foundational work, tool development, and empirical<br>research&#046; Its topics of interest center around the connection between<br>proofs (and other static techniques) and testing (and other dynamic<br>techniques)&#046; Papers are solicited on, but not limited to, the<br>following topics:<br>&#8211; Verification and analysis techniques combining proofs and tests<br>&#8211; Program proving with the aid of testing techniques<br>&#8211; Deductive techniques (theorem proving, model checking, symbolic<br>execution, SMT solving, constraint logic programming, etc&#046;) to<br>support testing: generating testing inputs and oracles, supporting<br>coverage criteria, and so on&#046;<br>&#8211; Program analysis techniques combining static and dynamic analysis<br>&#8211; Specification inference by deductive and dynamic methods<br>&#8211; Testing and runtime analysis of formal specifications<br>&#8211; Model&#8211;based testing and verification<br>&#8211; Using model checking to generate test cases<br>&#8211; Testing of verification tools and environments<br>&#8211; Applications of testing and proving to new domains, such as<br>security, configuration management, and language&#8211;based techniques<br>&#8211; Bridging the gap between concrete and symbolic reasoning techniques<br>&#8211; Innovative approaches to verification such as crowdsourcing and<br>serious games<br>&#8211; Case studies, tool and framework descriptions, and experience<br>reports about combining tests and proofs<br>