Tools and Algorithms for the Construction and Analysis of Systems

SAT and SMT.- Decomposing Farkas Interpolants.- Parallel SAT Simplification on GPU Architectures.- Encoding Redundancy for Satisfaction-Driven Clause Learning.- WAPS: Weighted and Projected Sampling.- Building Better Bit-Blasting for Floating-Point Problems.- The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations.- On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition.- Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework.- SAT Solving and Theorem Proving.- Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks.- Incremental Analysis of Evolving Alloy Models.- Extending a Brainiac Prover to Lambda-Free Higher-Order Logic.- Verification and Analysis LCV: A Verification Tool for Linear Controller Software.- Semantic Fault Localization and Suspiciousness Ranking.- Computing Coupled Similarity.- Reachability Analysis for Termination and Confluence of Rewriting.- Model Checking.- VoxLogicA: a Spatial Model Checker for Declarative Image Analysis.- On Reachability in Parameterized Phaser Programs.- Abstract Dependency Graphs and Their Application to Model Checking.- Tool Demo.- nonreach - A Tool for Nonreachability Analysis.- The Quantitative Verification Benchmark Set.- ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions.- MetAcsl: Specification and Verification of High-Level Properties.- ROLL 1.0: !-Regular Language Learning Library.- Symbolic Regex Matcher.- COMPASS 3.0.- Debugging of Behavioural Models with CLEAR.- Machine Learning.- Omega-Regular Objectives in Model-Free Reinforcement Learning.- Verifiably Safe Off-Model Reinforcement Learning.