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 II / 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 ; 16506.

Lecture notes in computer science, 1611-3349 ; 16506

Language:

English

Subjects (All):

System design--Congresses.

System design.

Computer software--Verification--Congresses.

Computer software.

System analysis--Congresses.

System analysis.

Genre:

proceedings (reports)

Conference papers and proceedings.

Physical Description:

1 online resource (xxvii, 603 pages) : illustrations (chiefly color).

Other Title:

TACAS 2026

Place of Publication:

Cham, Switzerland : Springer, [2026]

Summary:

The 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-16m 2026.

Contents:

Verifying floating-point programs in Stainless / Andrea Gilot, Axel Bergström, and Eva Darulova

Efficient verification of Lingua Franca programs / Peter Csaba Ölveczky, Mario Reja, Mikheil Rukhaia, Kyungmin Bae, and Mircea Marin

A case study in firmware verification : Applying formal methods to Intel TDX module / Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee, and Thomas Lemberger

Extending FRET with SLEEC rules : Formalization, obligation inference, and monitoring / Mahrokh Mirani, Paola Inverardi, Patrizio Pelliccione, Franco Raimondi, and Nicolas Troquard

Deciding serializability in network systems / Guy Amir, Mark Barbone, Nicolas Amat, and Jules Jacobs

VeriStruct : AI-assisted automated verification of data-structure modules in Verus / Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill, and Clark Barrett

On deciding constant runtime of linear loops / Florian Frohn, Jürgen Giesl, Peter Giesl, and Nils Lommen

Integrating string reasoning in symbolic execution of C programs / Rachel Cleaveland and Clark Barrett

Same engine, multiple gears : Parallelizing fixpoint iteration at different granularities / Ali Rasim Kocal, Michael Schwarz, Simmo Saan, and Helmut Seidl

Gillian debugging : Swinging through the (compositional symbolic execution) trees / Nat Karmios, Sacha-Élie Ayoun, and Philippa Gardner

ReCheck : Automated contextual improvement verifier for functional calculi across user-defined operational semantics / Makoto Hamana and Kento Emoto

Data structure analysis for binaries / Sadra Bayat Tork, Nicholas Coughlin, Alicia Michael, James Tobler, and Kirsten Winter

jMT : Testing correctness of Java memory models / Lukas Panneke and Heike Wehrheim

Demonstrating ARG-V’s generation of realistic Java benchmarks for SV-COMP / Charles Moloney, Robert Dyer, and Elena Sherman

CTL\* model checking on infinite families of finite-state labeled transition systems / Roberto Pettinau and Christoph Matheja

ReVEAL : GNN-guided reverse engineering for formal verification of optimized multipliers / Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang, and Cunxi Yu

EvolveGen : Algorithmic level hardware model checking benchmark generation through reinforcement learning / Guangyu Hu, Xiaofeng Zhou, Wei Zhang, and Hongce Zhang

Verifying first-order temporal properties of infinite-state systems via timers and rankings / Raz Lotan, Neta Elad, Oded Padon, and Sharon Shoham

Revisiting stateful partial-order reduction / Frédéric Herbreteau, Gérald Point, Gautham Viswanathan, and Igor Walukiewicz

Deconstructing subset construction : Reducing while determinizing / John Nicol and Markus Frohme

Equivalence checking of quantum circuits via path-sum and weighted model counting / Wei-Jia Huang, Christophe Chareton, Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Alfons Laarman, and Jingyi Mei

Error-tolerant quantum state discrimination : Optimization and quantum circuit synthesis / Chien-Kai Ma, Bo-Hung Chen, Tian-Fu Chen, Dah-Wei Chiou, and Jie-Hong R. Jiang

Evaluating software verifiers for C, Java, and SV-LIB (Report on SV-COMP 2026) / Dirk Beyer and Jan Strejček

DASA : Fully gradient-based program analysis (Competition contribution) / Felix Mächtle, Jan-Niclas Serr, Nils Loose, and Thomas Eisenbarth

EmergenTheta : Experimental analyses within the Theta framework (Competition contribution) / Milán Mondok, Csanád Telbisz, Levente Bajczi, Dániel Kovács, Mihály Dobos-Kovács, and Vince Molnár

Goblint : A portfolio for mixed flow-sensitive abstract interpretation (Competition contribution) / Simmo Saan, Ali Rasim Kocal, Michael Petter, Karoliine Holter, Julian Erhard, Michael Schwarz, Vesal Vojdani, and Helmut Seidl

Goblitch : Combining abstract interpretation with symbolic execution via witnesses (Competition contribution) / Karoliine Holter, Paulína Ayaziová, Simmo Saan, Jan Strejček, and Vesal Vojdani

Hornix : From LLVM IR to constrained Horn clauses and back (Competition contribution) / Martin Blicha, Jan Kofroň, and Oliver Glitta

Iekkë : A SAT-based bounded-round verifier for multi-threaded programs (Competition contribution) / Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, and Gennaro Parlato

JLiSA : The Java frontend of the library for static analysis (Competition contribution) / Vincenzo Arceri, Luca Negrini, Giacomo Zanatta, Filippo Bianchi, Teodors Lisovenko, Luca Olivieri, and Pietro Ferrara

Mopsa-C : Towards incorrectness and termination verdicts (Competition contribution) / Marco Milanese, Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné

Re3ver : Reverse and verify (Competition contribution) / Adéla Štěpková, Martin Jonáš, and Jan Strejček

ReFuncTion : Conditional termination by abstract interpretation of numerical C programs (Competition contribution) / Naïm Moussaoui Remil and Caterina Urban

Seal : Symbolic execution with separation logic (Competition contribution) / Tomáš Brablec, Tomáš Dacík, and Tomáš Vojnar

SWAT : Improvements to the symbolic executor (Competition contribution) / Nils Loose, Florian Sieck, Felix Mächtle, and Thomas Eisenbarth

Symbiotic 11 : Predicate abstraction joins the party (Competition contribution) / Paulína Ayaziová, Martin Jonáš, Vincent Mihalkovič, Jindřich Sedláček, and Jan Strejček

Ultimate Automizer with a one-dimensional memory model (Competition contribution) / Manuel Bentele, Max Barth, Marcel Ebbinghaus, Jan Körner, Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, and Andreas Podelski

Ultimate Paralizer : Parallel trace abstraction (Competition contribution) / Max Barth, Daniel Dietsch, Matthias Heizmann, and Marie-Christine Jakobs.

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:

9783032227492

3032227496

OCLC:

1586811023

Access Restriction:

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