TAP 2023
Tue 18 - Wed 19 July 2023 Leicester, United Kingdom
co-located with STAF 2023

Accepted Papers

Title
Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion CheckingTAP Best Paper
Research Papers
DOI
BIRD: A Binary Intermediate Representation for formally verified Decompilation of x86-64 binaries
Research Papers
DOI Pre-print File Attached
Certified Logic-Based Explainable AI -- The Case of Monotonic Classifiers
Research Papers
DOI File Attached
Context Specification Language for Formal Verification of Consent Properties on Models and Code
Research Papers
DOI File Attached
Low-level Reachability Analysis based on Formal Logic
Research Papers
DOI Pre-print
Proving Properties of Operation Contracts with Test Scenarios
Research Papers
DOI
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
Research Papers
DOI
Symbolic Observation Graph-Based Generation of Test Paths
Research Papers
DOI File Attached
Testing a Formally Verified Compiler
Research Papers
DOI Pre-print
Testing Languages with a Languages-as-databases ApproachTAP Best Paper
Research Papers
DOI

Call for Papers

Aims and Scope

The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.

Research in verification has seen a steady convergence of heterogeneous techniques and a synergy between the traditionally distinct areas of testing (and dynamic analysis) and of proving (and static analysis). Formal techniques for counter-example generation based on, for example, symbolic execution, SAT/SMT-solving or model checking, furnish evidence for the potential of a combination of test and proof. The combination of predicate abstraction with testing-like techniques based on exhaustive enumeration opens the perspective for novel techniques of proving correctness. On the practical side, testing offers cost-effective debugging techniques of specifications or crucial parts of program proofs (such as invariants). Last but not least, testing is indispensable when it comes to the validation of the underlying assumptions of complex system models involving hardware and/or system environments. Over the years, there is growing acceptance in research communities that testing and proving are complementary rather than mutually exclusive techniques.

TAP’s scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Its topics of interest center around the connection between proofs (and other static techniques) and testing (and other dynamic techniques). Papers are solicited on, but not limited to, the following topics:

  • Verification and analysis techniques combining proofs and tests,
  • Program proving with the aid of testing techniques,
  • Deductive techniques supporting the automated generation of test vectors and oracles (theorem proving, model checking, symbolic execution, SAT/SMT solving, constraint logic programming, etc.),
  • Deductive techniques supporting novel definitions of coverage criteria,
  • Specification inference by deductive and dynamic methods,
  • Testing and runtime analysis of formal specifications,
  • Search-based technics for proving and testing,
  • Verification of verification tools and environments,
  • Applications of test and proof techniques in new domains,
  • Combined approaches of test and proof in the context of formal certifications (Common Criteria, CENELEC, …), and
  • Case studies, tool and framework descriptions, and experience

Authors are encouraged (but not required) to make available to the reviewers (and whenever possible publicly) the relevant artifacts. While the artifacts will not be formally reviewed, their availability and - consistency with and replicability of results in the paper, - completeness, - documentation, and - ease of use, will be weighted for the acceptance decision.

Important Dates:

  • March 3rd March 24th, 2023: deadline for abstract submission~~
  • March 17th March 24th, 2023: deadline for full-text submission
  • April 21st, 2023: Acceptance notification
  • May 15th, 2023: Deadline for final papers

Submission Instructions

TAP 2023 accepts papers of four kinds:

  • Regular research papers: full submissions describing original research, of up to 16 pages (excluding references).

  • Tool demonstration papers: submissions describing the design and implementation of an analysis/verification tool or framework, of up to 8 pages (excluding references). The tool/framework described in a tool demonstration paper should be available for public use.

  • Short papers: submissions describing preliminary findings, proofs of concepts, and exploratory studies, of up to 6 pages (excluding references).

  • Journal-first extended abstracts, of up to 4 pages, summarizing recently published articles in high-quality journals. The aim of journal-first papers is to further enrich the program of TAP, as well as to provide an more flexible path to dissemination of results in the field. The summarized journal article should have been published (or accepted) by 1 July 2020 or later, and report new results (as opposed as simply extending prior conference work with ‘appendix’ material, or minor enhancements). Journal-first submissions must be marked as such in the submission’s title, and must explicitly include full bibliographic details (including a DOI) of the journal publication they are based on.

Accepted submissions will be published in Springer’s LNCS series. Papers have to adhere to Springer’s LNCS format and must be submitted in PDF format at the EasyChair submission site: https://easychair.org/conferences/?conf=tap23

Dates
Tracks
Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 18 Jul

Displayed time zone: London change

10:30 - 11:00
Morning CoffeeSTAF Social at The Bar
10:30
30m
Coffee break
Coffee Break
STAF Social

11:00 - 12:30
STAF Keynote / TAP Session 1STAF Keynotes / Research Papers / ECMFA / ICGT Research Papers at Oak
Chair(s): Cristina Seceleanu Mälardalen University

Remote Participants: Zoom Link, YouTube Livestream

11:00
15m
Day opening
TAP Conference Opening
Research Papers
Virgile Prevosto CEA Tech List, Cristina Seceleanu Mälardalen University
11:15
75m
Keynote
Symbolic, Statistical and Randomized Engines in UPPAAL
STAF Keynotes
Kim Larsen Aalborg University
12:30 - 13:30
12:30
60m
Lunch
Lunch
STAF Social

13:30 - 15:00
TAP Session 2: Low-level code verificationResearch Papers at Oak
Chair(s): Julien Signoles Université Paris-Saclay, CEA, List

Remote Participants: Zoom Link

13:30
30m
Talk
BIRD: A Binary Intermediate Representation for formally verified Decompilation of x86-64 binaries
Research Papers
P: Daniel Engel Open University Of The Netherlands, Freek Verbeek Open University of the Netherlands, The Netherlands, Binoy Ravindran Virginia Tech
DOI Pre-print File Attached
14:00
30m
Talk
Low-level Reachability Analysis based on Formal Logic
Research Papers
P: Nico Naus Virginia Tech, Freek Verbeek Open University of the Netherlands, The Netherlands, Marc Schoolderman Radboud University Nijmegen, Binoy Ravindran Virginia Tech
DOI Pre-print
14:30
30m
Talk
Testing a Formally Verified Compiler
Research Papers
P: David Monniaux CNRS/VERIMAG, Léo Gourdin Université Grenoble Alpes, Verimag, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Olivier Lebeltel Université Grenoble Alpes, CNRS, Verimag
DOI Pre-print
15:00 - 15:30
Afternoon CoffeeSTAF Social at The Bar
15:00
30m
Coffee break
Coffee Break
STAF Social

15:30 - 16:30
TAP Session 3: Formal ModelsResearch Papers at Oak
Chair(s): Catherine Dubois ENSIIE Paris-Evry

Remote Participants: Zoom Link

15:30
30m
Talk
Certified Logic-Based Explainable AI -- The Case of Monotonic Classifiers
Research Papers
P: Aurélie Hurault IRIT - ENSEEIHT, Joao Marques-Silva IRIT, CNRS, Toulouse
DOI File Attached
16:00
30m
Talk
Context Specification Language for Formal Verification of Consent Properties on Models and Code
Research Papers
P: Myriam Clouet Université Paris-Saclay, CEA, List, Thibaud Antignac CNIL (Commission nationale de l’informatique et des libertés), Mathilde Arnaud Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List
DOI File Attached

Wed 19 Jul

Displayed time zone: London change

09:00 - 10:15
STAF Keynote / ICGT Session 1STAF Keynotes / Research Papers / ECMFA / ICGT Research Papers at Oak
Chair(s): Maribel Fernandez King's College London

Remote Participants: Zoom Link, YouTube Livestream

09:00
15m
Day opening
ICGT Conference Opening
ICGT Research Papers
Maribel Fernandez King's College London, Chris Poskitt Singapore Management University
File Attached
09:15
60m
Keynote
Syntactic trinitarianism: terms, graphs, diagrams
STAF Keynotes
Dan Ghica Huawei Research and University of Birmingham
Pre-print
10:30 - 11:00
Morning CoffeeSTAF Social at The Bar
10:30
30m
Coffee break
Coffee Break
STAF Social

11:15 - 12:45
TAP Session 4: Model-based test generationResearch Papers at Willow
Chair(s): Nico Naus Virginia Tech

Remote Participants: Zoom Link

11:15
30m
Talk
Symbolic Observation Graph-Based Generation of Test Paths
Research Papers
P: Kais Klai Universit Paris 13, Mohamed Taha Bennani Universty of Tunis El Manar, Jaime Arias CNRS; LIPN; Université Sorbonne Paris Nord, Jörg Desel Fernuniversität in Hagen, Hanen Ochi EFREI
DOI File Attached
11:45
30m
Talk
Testing Languages with a Languages-as-databases ApproachTAP Best Paper
Research Papers
P: Matteo Cimini University of Massachusetts Lowell
DOI
12:15
30m
Talk
Proving Properties of Operation Contracts with Test Scenarios
Research Papers
P: Martin Gogolla Database Systems Group, University of Bremen, Lars Hamann HAW Hamburg
DOI
12:30 - 13:30
12:30
60m
Lunch
Lunch
STAF Social

13:45 - 15:15
TAP Session 5: KeynoteSTAF Keynotes at Willow
Chair(s): Virgile Prevosto CEA Tech List

Remote Participants: Zoom Link

13:45
90m
Keynote
KeY: A Verification Platform For Java
STAF Keynotes
15:00 - 15:30
Afternoon CoffeeSTAF Social at The Bar
15:00
30m
Coffee break
Coffee Break
STAF Social

15:45 - 16:45
TAP Session 6: Abstraction and RefinementResearch Papers at Willow
Chair(s): Matteo Cimini University of Massachusetts Lowell

Remote Participants: Zoom Link

15:45
30m
Talk
Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion CheckingTAP Best Paper
Research Papers
P: Thibaut Benjamin Université Paris-Saclay, CEA, List, Julien Signoles Université Paris-Saclay, CEA, List
DOI
16:15
30m
Talk
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
Research Papers
P: Megan Strauss Carnegie Mellon University, Stefan Mitsch Carnegie Mellon University, USA
DOI
17:15 - 22:30
STAF Excursion & BanquetSTAF Social
17:15
1h45m
Social Event
Excursion to St Mary de Castro
STAF Social

19:00
3h30m
Dinner
Banquet at Bistrot Pierre
STAF Social

Fri 21 Jul

Displayed time zone: London change

09:00 - 10:30
STAF Keynote / ECMFA Session 5STAF Keynotes / Research Papers / ECMFA / ICGT Research Papers at Oak
Chair(s): Steffen Zschaler King's College London

Remote Participants: Zoom Link, YouTube Livestream

09:00
90m
Keynote
How I lost my faith (in language technology research)? There and back again.
STAF Keynotes
Andrzej Wąsowski IT University of Copenhagen, Denmark
Questions? Use the TAP contact form.