Tests and Proofs: 17th International Conference, TAP 2023, Leicester, UK, July 18–19, 2023, Proceedings (Lecture Notes in Computer Science, 14066)

Preface
Organization
Invited Talks
	Symbolic, Statistical and Randomized Engines in UPPAAL
	KeY: A Verification Platform for Java
	Contents
Low-Level Code Verification
BIRD: A Binary Intermediate Representation for Formally Verified Decompilation of X86-64 Binaries
	1 Introduction
	2 Related Work
	3 Formalization
		3.1 Generic BIRD
		3.2 Instantiation 1: X86
		3.3 Instantiation 2: Early BIRD
	4 X86to Early BIRD
	5 Conclusion
	References
Low-Level Reachability Analysis Based on Formal Logic
	1 Introduction
	2 The jump Language
	3 Precondition Generation
	4 Litmus Tests
		4.1 Infinite Reachability Space: Long Division
		4.2 Indirect Jumps
	5 Case Studies
		5.1 Faulty Partitioning for Quicksort
		5.2 Karatsuba
	6 Related Work
	7 Conclusion
	References
Testing a Formally Verified Compiler
	1 Introduction
	2 Formally Verified Defensive Tests
	3 Test Suite for Compiler Correctness
	4 Reducing Test Cases
	5 Checking the Trusted Computing Base
	6 Testing the Performance of Generated Code
	7 Conclusion on Testing Formally Verified Software
	References
Formal Models
Certified Logic-Based Explainable AI – The Case of Monotonic Classifiers
	1 Introduction
	2 Preliminaries
	3 Explanations for Monotonic Classifiers
	4 Proofs
		4.1 Coq
		4.2 The Coq Formalization
		4.3 Results
		4.4 Proof Sketch
		4.5 Computing Explanations that Are Guaranteed to Be Correct
	5 Experiments
		5.1 Datasets
		5.2 Models
		5.3 Computing Explanations
		5.4 Comparison with Direct Mono-Language Implementation
	6 Conclusions
	References
Context Specification Language for Formally Verifying Consent Properties on Models and Code
	1 Introduction
	2 Related Work
	3 Running Example
		3.1 Model of the Hospital Information System
		3.2 Implementation of the Information System
		3.3 Goal
	4 Specifying a System with CSpeL
		4.1 Model of a System
		4.2 Execution Traces
		4.3 Consent Properties
		4.4 Concrete Language
	5 Verifying Consent with CASTT
		5.1 CSpeL Offline Runtime Verification
		5.2 Consent Verification on C Source Code
	6 Experimentation and Evaluation
		6.1 Examples Used
		6.2 Offline Runtime Verification Evaluation
		6.3 Translation Mechanism Evaluation
	7 Conclusion and Perspectives
	References
	A  Example of generated file
	B  Proof of Properties of Example 3
		B.1  Traces at Model Level
		B.2  Traces at Program Level
	C  Instantiations using CSpeL
Model-Based Test Generation
Proving Properties of Operation Contracts with Test Scenarios
	1 Introduction
	2 The Basic Idea Through a Prototypical Example
	3 Consistency and Property Reachability
		3.1 General Discussion
		3.2 Example-Specific Discussion
	4 Related Work
	5 Conclusion and Future Work
	References
Testing Languages with a Languages-as-Databases Approach
	1 Introduction
	2 Language Definitions in Lang-SQL
	3 The Lang-SQL Query Language
	4 Examples of Language Tests
	5 A GSOS Validator with Language Tests
	6 Evaluation
	7 Related Work
	8 Conclusion
	References
Symbolic Observation Graph-Based Generation of Test Paths
	1 Introduction
	2 Preliminaries
		2.1 Labelled Transition Systems (LTS)
		2.2 Petri Nets
		2.3 Symbolic Observation Graph (SOG)
		2.4 Test Coverage Criteria
	3 Structure-Based Coverage Relation for Petri Nets
	4 Test Specification Computation
		4.1 On-the-Fly SOG-Based Generation of Observable Traces
		4.2 Extracting Abstract Traces
	5 Experiments
	6 Related Work
	7 Conclusion
	A  Proof of Lemma 1
	B  Proof of Lemma 2
	C  Proof of Lemma 3
	D  Proof of Theorem 2
	References
Abstraction and Refinement
Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars
	1 Introduction and Motivation
	2 Background
		2.1 Responsibility-Sensitive Safety
		2.2 Differential Dynamic Logic and Notation
		2.3 Differential Refinement Logic
		2.4 ModelPlex
	3 Formalization of RSS Safety and Optimality
		3.1 Formalization and Verification of RSS Safety
		3.2 Longitudinal Safety
		3.3 Formalization and Verification of RSS Optimality
	4 Refinement from dL to Python
	5 Testing and Monitoring by Example
		5.1 Monitor Structure
		5.2 Examples of Monitor Usage
	6 Related Work
	7 Conclusion and Future Work
	References
Abstract Interpretation of Recursive Logic Definitions for Efficient Runtime Assertion Checking
	1 Introduction
	2 Illustrated Overview
	3 Language Definition
		3.1 Formal Syntax
		3.2 Program Structure
		3.3 Concrete Semantics
		3.4 Collecting Semantics
	4 Abstract Interpretation Without Logic Functions
		4.1 Lattice of Intervals
		4.2 Inference Rules
		4.3 Improving Precision for Conditionals
	5 Abstract Interpretation with Logic Functions
		5.1 Inference Rules
		5.2 Example of Derivation
		5.3 Termination of the Static Analysis
		5.4 Interval Inference
		5.5 Soundness of the Static Analysis
	6 Experimental Evaluation
		6.1 Practical Widening Operators
		6.2 Evaluation and Comparison of Widening Choices
		6.3 Further Improvements to Widening
	7 Conclusion and Further Work
	References
Author Index