Tools and Algorithms for the Construction and Analysis of Systems. 25th International Conference, TACAS 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 Prague, Czech Republic, April 6–11, 2019 Proceedings

ETAPS Foreword
Preface
Organization
Contents – Part I
Contents – Part II
SAT and SMT I
Decomposing Farkas Interpolants
	1 Introduction
	2 Motivation
	3 Preliminaries
	4 Decomposed Interpolants
		4.1 Strength-Based Ordering of Decompositions
		4.2 Strength of the Dual Interpolants
	5 Finding Decompositions
		5.1 Trivial Elements
		5.2 Decomposing in the Presence of Local Variables
	6 Experiments
	7 Conclusion
	References
Parallel SAT Simplification on GPU Architectures
	1 Introduction
	2 Preliminaries
	3 GPU Challenges: Memory and Data
	4 Algorithm Design and Implementation
		4.1 Parallel Variable Elimination
		4.2 Parallel Subsumption Elimination
	5 Benchmarks
	6 Related Work
	7 Conclusion
	References
Encoding Redundancy for Satisfaction-Driven Clause Learning
	1 Introduction
	2 Preliminaries
	3 Pruning Predicates and Redundant Clauses
	4 The Filtered Positive Reduct
	5 The PR Reduct
	6 Implementation
	7 Evaluation
	8 Conclusion
	References
WAPS: Weighted and Projected Sampling
	1 Introduction
	2 Related Work
	3 Notations and Preliminaries
		3.1 Weighted and Projected Generators
		3.2 Deterministic Decomposable Negation Normal Form (d-DNNF)
	4 Algorithm
		4.1 Compilation
		4.2 Annotation
		4.3 Sampling
		4.4 Conditioned Sampling
	5 Theoretical Analysis
	6 Evaluation
	7 Conclusion
	References
SAT and SMT II
Building Better Bit-Blasting for Floating-Point Problems
	1 Introduction
	2 The Challenges of Floating-Point Reasoning
		2.1 Techniques
	3 Floating-Point Circuits
	4 SymFPU
	5 Correctness
		5.1 PyMPF
	6 Experimental Results
		6.1 Experimental Setup
		6.2 Benchmarks
		6.3 Solvers
		6.4 Results
		6.5 Replication
	7 Conclusion
	References
The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations
	1 Introduction
	2 Background and Running Example
	3 A Debugging Recipe for SMT Quantifiers
	4 Visualising Quantifier Instantiations
	5 Manual Analysis of Instantiation Problems
	6 Automated Explanation of Matching Loops
	7 Implementation and Evaluation
	8 Related Work
	9 Conclusions
	References
On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition
	1 Introduction
	2 Scale-Free Formulas and Heterogeneity
		2.1 The Solubility Phase Transition
		2.2 Characterizing the Scale-Free Phase Transition
	3 Scaling Across Solver Types
	4 Effect of Heterogeneity on Search Trees
		4.1 Relaxed Bounded Model Checking Instances
	5 Conclusions
	References
Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework
	1 Introduction
	2 Background
	3 Divide-and-Conquer Based Parallel SAT Solvers
		3.1 Dividing the Search Space
		3.2 Load Balancing
		3.3 Exchanging Learnt Clauses
	4 Implementation of a Divide-and-Conquer
		4.1 About the Painless Framework
		4.2 The Divide-and-Conquer Component in Painless
		4.3 Implemented Heuristics
	5 Evaluation
		5.1 Comparing the Implemented Divide-and-Conquer Solvers
		5.2 Comparison with State-of-the-Art Divide-and-Conquer
	6 Conclusion
	References
SAT Solving and Theorem Proving
Quantitative Verification of Masked Arithmetic Programs Against Side-Channel Attacks
	1 Introduction
	2 Preliminaries
		2.1 Cryptographic Programs
		2.2 Quantitative Masking Strength
	3 Three Key Techniques
		3.1 Type System
		3.2 Model-Counting Based Reasoning
		3.3 Reduction Heuristics
	4 Overall Algorithms
		4.1 Perfect Masking Verification
		4.2 QMS Computing
	5 Practical Evaluation
		5.1 Experimental Results on Boolean Programs
		5.2 Experimental Results on Arithmetic Programs
	6 Conclusion
	References
Incremental Analysis of Evolving Alloy Models
	1 Introduction
	2 Background
		2.1 Alloy
		2.2 MuAlloy
		2.3 Regression Test Selection for Imperative Code
	3 Motivating Example
	4 Techniques
		4.1 Regression Command Selection (RCS)
		4.2 Solution Reuse (SR)
	5 Experimental Evaluation
		5.1 Experimental Setup
		5.2 RQ1: Speed-up Effectiveness
		5.3 RQ2: Command Selection and Solution Reuse Effectiveness
		5.4 RQ3: Time Consumption
	6 Related Work
	7 Conclusion and Future Work
	References
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
	1 Introduction
	2 Logic
	3 Types and Terms
	4 Unification and Matching
	5 Indexing Data Structures
	6 Inference Rules
	7 Heuristics
	8 Evaluation
	9 Discussion and Related Work
	10 Conclusion
	References
Verification and Analysis
LCV: A Verification Tool for Linear Controller Software
	1 Introduction
	2 Related Work
	3 Verification Flow of Linear Controller Verifier
	4 Evaluation
		4.1 Case Study
		4.2 Scalability
	5 Conclusion
	References
Semantic Fault Localization and Suspiciousness Ranking
	1 Introduction
	2 Guided Tour
	3 Semantic Fault Localization
		3.1 Programming Language
		3.2 Trace-Aberrant Statements
		3.3 Program-Aberrant Statements
		3.4 k-Aberrance
	4 Semantic Suspiciousness Ranking
	5 Implementation
	6 Experimental Evaluation
		6.1 Benchmark Selection
		6.2 Experimental Setup
		6.3 Experimental Results
	7 Related Work
	8 Conclusion
	References
Computing Coupled Similarity
	1 Introduction
	2 Coupled Similarity
		2.1 Transition Systems with Silent Steps
		2.2 Defining Coupled Similarity
		2.3 Order Properties and Coinduction
		2.4 Reduction of Weak Simulation to Coupled Simulation
	3 Fixed-Point Algorithm for Coupled Similarity
		3.1 The Algorithm
		3.2 Correctness and Complexity
	4 Game Algorithm for Coupled Similarity
		4.1 The Coupled Simulation Game
		4.2 Deciding the Coupled Simulation Game
		4.3 Tackling the -closure
		4.4 Optimizing the Game Algorithm
	5 A Scalable Implementation
		5.1 Prototype Implementation
		5.2 Evaluation
	6 Conclusion
	References
Reachability Analysis for Termination and Confluence of Rewriting
	1 Introduction
	2 Preliminaries
	3 Reachability Constraint Satisfaction
	4 Reachability in Term Rewriting
		4.1 Symbol Transition Graphs
		4.2 Look-Ahead Reachability
	5 Conditional Rewriting
		5.1 Infeasibility
		5.2 Symbol Transition Graphs in the Presence of Conditions
		5.3 Look-Ahead Reachability in the Presence of Conditions
	6 Assessment
	7 Related Work
	8 Conclusion
	References
Model Checking
VoxLogicA: A Spatial Model Checker for Declarative Image Analysis
	1 Introduction and Related Work
	2 The Spatial Logic Framework
		2.1 Foundations: Spatial Logics for Closure Spaces
		2.2 Region Similarity via Statistical Cross-correlation
	3 The Tool VoxLogicA
		3.1 Functionality
		3.2 Implementation Details
		3.3 Design and Data Structures
	4 Experimental Evaluation
		4.1 ImgQL Segmentation Procedure
		4.2 Validation Results
		4.3 Comparison with topochecker
	5 Conclusions and Future Work
	References
On Reachability in Parameterized Phaser Programs
	1 Introduction
	2 Motivating Example
	3 Phaser Programs and Reachability
	4 A Gap-Based Symbolic Representation
	5 A Symbolic Verification Procedure
	6 Limitations of Deciding Reachability
	7 Conclusion
	References
Abstract Dependency Graphs and Their Application to Model Checking
	1 Introduction
	2 Preliminaries
	3 Abstract Dependency Graphs
	4 On-the-Fly Algorithm for ADGs
	5 Applications of Abstract Dependency Graphs
		5.1 Liu and Smolka Dependency Graphs
		5.2 Certain-Zero Dependency Graphs
		5.3 Weighted Symbolic Dependency Graphs
	6 Implementation and Experimental Evaluation
		6.1 Bisimulation Checking for CCS Processes
		6.2 CTL Model Checking of Petri Nets
		6.3 Weighted CTL Model Checking
	7 Conclusion
	References
Tool Demos
nonreach – A Tool for Nonreachability Analysis
	1 Introduction
	2 Role
	3 Installation and Usage
	4 Design and Techniques
	5 Experiments
	References
The Quantitative Verification Benchmark Set
	1 Introduction
	2 A Collection of Quantitative Models
	3 An Archive of Results
	4 Accessing the Benchmark Set
	5 Conclusion
	References
ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions
	1 Introduction
	2 The ILAng Platform
		2.1 Background
		2.2 Constructing ILAs
		2.3 Verification Using ILAs
		2.4 Generating Verification Targets
	3 Tutorial Case Studies
		3.1 Advanced Encryption Standard (AES)
		3.2 A Simple Instruction Execution Pipeline
	4 Other ILAng Applications
	References
MetAcsl: Specification and Verification of High-Level Properties
	1 Introduction
	2 Specification of Meta-properties
		2.1 Target Functions and Quantification
		2.2 Notion of Context
	3 Verification of Meta-properties
	4 Results on Case Studies and Conclusion
	References
ROLL 1.0: -Regular Language Learning Library
	1 Introduction
	2 ROLL 1.0 Architecture and Usage
	References
Symbolic Regex Matcher
	1 Motivation
	2 Matching with Derivatives
	3 Implementation
	4 Evaluation
	References
COMPASS 3.0
	1 Introduction
	2 Toolset Overview
	3 Input Language
	4 New Functionalities in COMPASS 3.0
	5 Related Work and Conclusion
	References
Debugging of Behavioural Models with CLEAR
	1 Introduction
	2 Tagged LTSs
	3 Visualization Techniques
	4 Abstraction Techniques
	5 Experiments
	6 Concluding Remarks
	References
Machine Learning
Omega-Regular Objectives in Model-Free Reinforcement Learning
	1 Introduction
	2 Preliminaries
		2.1 Markov Decision Processes
		2.2 -Regular Performance Objectives
		2.3 The Product MDP
		2.4 Limit-Deterministic Büchi Automata
		2.5 Linear Time Logic Objectives
		2.6 Reinforcement Learning
	3 Problem Statement and Motivation
	4 Model-Free RL from Omega-Regular Rewards
	5 Experimental Results
	6 Conclusion
	References
Verifiably Safe Off-Model Reinforcement Learning
	1 Introduction
	2 Background
	3 Verification-Preserving Model Updates
	4 Verifiably Safe RL with Multiple Models
		4.1 Active Verified Model Update Learning
	5 A Model Update Library
	6 Experimental Validation
	7 Related Work
	8 Conclusions
	References
Correction to: \\mathsf {WAPS}: Weighted and Projected Sampling
	Correction to: Chapter “\\mathsf {WAPS}: Weighted and Projected Sampling” in: T. Vojnar and L. Zhang (Eds.): Tools and Algorithms for the Construction and Analysis of Systems, LNCS 11427, https://doi.org/10.1007/978-3-030-17462-0_4
Author Index