Tools and algorithms for the construction and analysis of systems : 32nd international conference, TACAS 2026, held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, proceedings. Part I / Sebastian Junges, Guy Katz, editors.

Format:

Book

Conference/Event

Contributor:

Junges, Sebastian, editor.

Katz, Guy, editor.

Conference Name:

TACAS (Conference) (32nd : 2026 : Turin, Italy)

Series:

Lecture notes in computer science ; 16505.

Lecture notes in computer science, 1611-3349 ; 16505

Language:

English

Subjects (All):

System design--Congresses.

System design.

Computer software--Verification--Congresses.

Computer software.

System analysis--Congresses.

System analysis.

Computer software--Verification.

Genre:

proceedings (reports)

Conference papers and proceedings

Conference papers and proceedings.

Physical Description:

1 online resource (xxvi, 682 pages) : illustrations (chiefly color).

Other Title:

TACAS 2026

Place of Publication:

Cham, Switzerland : Springer, [2026]

Summary:

The open access book set LNCS 16505 + 16506 constitutes the proceedings of the 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2026, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, in Turin, Italy, during April 11-16, 2026. The 52 full papers, 4 short papers and 16 SV-COMP papers included in the proceedings were carefully reviewed and selected from 177 submissions. They were organized in topical sections as follows: Part I: SAT/SMT; Proofs and QUantified Elimination; Automata; Verification of Probabilistic Systems; Cyber-Physical Systems; Part II: Software Verification; Program Verification; Java Analysis; Hardware Verification and Model Checking; Quantum; SV-COMP. .

Contents:

Robustness verification of graph neural networks via lightweight satisfiability testing / Chia-Hsuan Lu, Tony Tan, and Michael Benedikt

Smt.ml : a multi-backend frontend for SMT solvers in OCaml / João Madeira Pereira, Filipe Marques, Pedro Adão, Hichem Rami Ait-El-Hara, Léo Andrès, Arthur Carcano, Pierre Chambart, Petar Maksimović, Nuno Santos, and José Fragoso Santos

Syntactically convex model-based projection for linear real arithmetic / Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel, and Lev Nachmanson

Bit-precise interpolation in Bitwuzla / Aina Niemetz and Mathias Preiner

Orbitopal fixing in SAT / Markus Anders, Cayden Codel, and Marijn J. H. Heule

Automatically tightening access control policies with Restricter / Ka Lok Wu, Christa Jenkins, Scott D. Stoller, and Omar Chowdhury

Parallel SMT solving via iterative tree partitioning / Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh, and Natasha Sharygina

Exploring the SMT-LIB benchmark library / Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark Barrett, Pascal Fontaine, and Cesare Tinelli

Massively parallel bit-precise verification with Bitwuzla and Mallob / Dominik Schreiber, Aina Niemetz, and Mathias Preiner

SMT(LIA) sampling with high diversity / Yong Lai, Junjie Li, and Chuan Luo

BDD-based formula approximations for quantified bit-vector satisfiability / Jakub Horák and Martin Jonáš

SMTScope : automated and efficient analysis of SMT traces / Jonáš Fiala and Peter Müller

Hint-based SMT proof reconstruction / Joshua Clune, Haniel Barbosa, and Jeremy Avigad

Incremental forward reasoning for white-box proof search / Xavier Généreux and Jannis Limperg

Enumerating choice terms in model-based quantifier instantiation / Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, and Cesare Tinelli

Fast Ramsey quantifier elimination in LIRA (with applications to liveness checking) / Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche

QSOLE : automatic QBF equivalence checking / Peter Pfeiffer, Mark Peyrer, Daniel Große, and Martina Seidl

Real-time proof checking for distributed incremental SAT solving / Dominik Schreiber, Mathias Fleury, Katalin Fazekas, and Armin Biere

Quantifier elimination meets treewidth / Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, and Naijun Zhan

Concurrent permissive strategy templates / Ashwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak, and Anne-Kathrin Schmuck

Modular attractor acceleration in infinite-state games / Philippe Heim and Rayna Dimitrova

A Myhill–Nerode characterization and active learning for one-clock timed automata / Kyveli Doveri, Pierre Ganty, and B. Srivathsan

Faster signature refinement for branching bisimilarity minimization / Jan Martens and Maurice Laveaux

MightyPPL : model checking MITL with past and Pnueli modalities / Hsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Paritosh Pandya

LTLf learning meets Boolean set cover / Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon, and Pierre Vandenhove

Robust verification of concurrent stochastic games / Angel Y. He and David Parker

Multiple long-run and ω-regular objectives in MDPs / Julius Ide, Joost-Pieter Katoen, Hannah Mertens, and Tim Quatmann

Computing fixpoints of learned functions : chaotic iteration and simple stochastic games / Paolo Baldan, Sebastian Gurke, Barbara König, and Florian Wittbold

DeGAS : gradient-based optimization of probabilistic programs without sampling / Francesca Randone, Romina Doz, Mirco Tribastone, and Luca Bortolussi

AKR : a model checker for an adaptative probabilistic knowing-how logic / Valentin Cassano, Pablo F. Castro, Pedro R. D’ Argenio, and Raul Fervar

Driving by disproof : a practical model checking approach to fleet coordination / Lukas König, Christian Schildwächter, Michaela Klauck, and Christian Heinzemann

VeriLHyS : a framework for LTL specification and verification of hybrid systems / Ludovico Battista, Stefano Tonetta, and Gianni Zampedri

TEMPORA : efficient verification of metric temporal properties with past in pointwise semantics / S. Akshay, Prerak Contractor, Paul Gastin, R. Govind, and B. Srivathsan

Trace repair for temporal behavior trees / Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner, and Sriram Sankaranarayanan.

Notes:

International conference proceedings.

Includes bibliographical references and index.

Online resource; title from PDF title page (Springer Nature Link, viewed April 29, 2026).

Other Format:

Print version: TACAS (Conference) (32nd : 2026 : Turin, Italy) Tools and algorithms for the construction and analysis of systems

ISBN:

9783032227522

3032227526

OCLC:

1586810925

Access Restriction:

Some versions: Open access versions available from some providers open access