Tools and Algorithms for the Construction and Analysis of Systems : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II / edited by Sriram Sankaranarayanan, Natasha Sharygina.

Format:

Book

Contributor:

Sharygina, Natasha, editor.

Sankaranarayanan, Sriram, editor.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 13994

Language:

English

Subjects (All):

Computer science.

Theory of Computation.

Local Subjects:

Theory of Computation.

Physical Description:

1 online resource (xxiv, 604 pages) : illustrations (some color).

Edition:

1st ed. 2023.

Place of Publication:

Cham : Springer Nature Switzerland : Imprint: Springer, 2023.

Summary:

This open access book constitutes the proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, during April 22-27, 2023, in Paris, France. The 56 full papers and 6 short tool demonstration papers presented in this volume were carefully reviewed and selected from 169 submissions. The proceedings also contain 1 invited talk in full paper length, 13 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report. TACAS is a forum for researchers, developers, and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility, and efficiency of tools and algorithms for building computer-controlled systems.

Contents:

Tool Demos

EVA: a Tool for the Compositional Verification of AUTOSAR Models

WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification

Multiparty Session Typing in Java, Deductively

PyLTA: A Verification Tool for Parameterized Distributed Algorithms

FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format

Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit

Combinatorial Optimization/Theorem Proving

New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization

Verified reductions for optimization

Specifying and Verifying Higher-order Rust Iterators

Extending a High-Performance Prover to Higher-Order Logic

Tools (Regular Papers)

The WhyRel Prototype for Relational Verification of Pointer Programs

Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter

CoPTIC: Constraint Programming Translated Into C

Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability

Synthesis

Computing Adequately Permissive Assumptions for Synthesis

Verification-guided Programmatic Controller Synthesis

Taming Large Bounds in Synthesis from Bounded-Liveness Specifications

Lockstep Composition for Unbalanced Loops

Synthesis of Distributed Agreement-Based Systems with Effciently Decidable Verification

LTL Reactive Synthesis with a Few Hints

Timed Automata Verification and Synthesis via Finite Automata Learning

Graphs/Probabilistic Systems

A Truly Symbolic Linear-Time Algorithm for SCC Decomposition

Transforming quantified Boolean formulas using biclique covers

Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants

Runtime Monitoring/Program Analysis

Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote

Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis

Explainable Online Monitoring of Metric Temporal Logic

12th Competition on Software Verification — SV-COMP 2023

Competition on Software Verification and Witness Validation: SV-COMP 2023

Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution)

2LS: Arrays and Loop Unwinding (Competition Contribution)

Bubaak: Runtime Monitoring of Program Verifiers (Competition Contribution)

EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution)

Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution)

Java Ranger: Supporting String and Array Operations (Competition Contribution)

Korn–Software Verification with Horn Clauses (Competition Contribution)

Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)

PIChecker: A POR and Interpolation based Verifierfor Concurrent Programs (Competition Contribution)

Ultimate Automizer and the CommuHash Normal Form (Competition Contribution)

Ultimate Taipan and Race Detection in Ultimate (Competition Contribution)

VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution)

VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution). .

Notes:

Includes bibliographical references and index.

ISBN:

9783031308208

3031308204

OCLC:

1377209783