Computer aided verification : 38th International Conference, CAV 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings. Part II / Eva Darulova, Anthony W. Lin, Philipp Rümmer, editors

Format:

Book

Conference/Event

Contributor:

Darulova, Eva, editor.

Lin, Anthony Widjaja, editor.

Rümmer, Philipp, editor.

Conference Name:

CAV (Conference) (38th : 2026 : Lisbon, Portugal)

Series:

Lecture notes in computer science ; 1611-3349 16683.

Lecture notes in computer science, 1611-3349 ; 16683

Language:

English

Subjects (All):

Computer software--Verification--Congresses.

Computer software.

Computer software--Verification.

Genre:

Conference papers and proceedings

Physical Description:

1 online resource : illustrations.

black and white

illustrations

Place of Publication:

Cham, Switzerland : Springer, [2026]

Summary:

This open access 3-volume set constitutes the proceedings of the 38th International Conference, CAV 2026, held in Lisbon, Portugal, in July 2026. The 54 full papers, together with 21 short tool papers,and 6 industrial experience reports and case studies, were carefully reviewed and selected from 319 submissions. These papers apply or extend formal methods to a wide range of domains such as concurrency, machine learning and neural networks, quantum systems,as well as hybrid and stochastic systems. This annual conference is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. This year, CAV was held as part of the Federated Logic Conference (FLoC)

Contents:

Improving stability of SMT solvers via context-driven normalization / Xiang Zhang, Mengyu Zhao, Shaohuang Chen, Jian Zhang, and Shaowei Cai

Satisfiability modulo extensional constant arrays / Mathias Preiner, Aina Niemetz, and Clark Barrett

String solving with stabilization and transducers / David Chocholatý, Vojtěch Havlena, Lukáš Holík, Juraj Síč, and Michal Šedý

Lagrangian-based duality for quantified SMT algorithms / Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, and Sharon Shoham

Mallob : scalable automated reasoning on demand / Dominik Schreiber, Niccolò Rigi-Luperti, and Peter Sanders

Modular reasoning about object relations / Micha Greutmann, Marco Eilers, and Peter Müller

Formally verified linear-time invertible lexing / Samuel Chassot and Viktor Kunčak

Automating bitvector and finite field equivalence proofs in Lean / Elizaveta Pertseva, Valentin Robert, Clark Barrett, and James Parker

The cooperating proof calculus : comprehensive proofs for an SMT solver / Andrew Reynolds, Hans-Jörg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Zoe Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert Jones, Clark Barrett, and Cesare Tinelli

Burrow : a proof framework for weak memory / Dennis Sprokholt and Soham Chakraborty

Velvet : a foundational multi-modal verifier for imperative programs in Lean / Vladimir Gladshtein, Vitaly Kurin, Yueyang Feng, Dipesh Kafle, George Pîrlea, Qiyuan Zhao, and Ilya Sergey

Automatic heap-memory diagrams for separation-logic proofs / Yawen Guan, Shardul Chiplunkar, and Clément Pit Claudel

An L# based algorithm for active learning of minimal separating automata / Jasper Laumen, Leonne Snel, and Frits Vaandrager

Upper bound for the determinization of Emerson-Lei automata : a one-fin approach / Runzhe Ma, Cong Tian, Wensheng Wang, and Zhenhua Duan

SMT-based active learning of weighted automata / Tiago Ferreira, Kevin Batz, and Alexandra Silva

Compositional verification of timed automata via violation assumptions / Mehran Moeini Jam, Hamed Kalantari, Ehsan Khamespanah, Marjan Sirjani, and Ali Movaghar

Weighted soundness for workflow nets / Piotr Hofman, Krzysztof Makuracki, and Filip Mazowiecki

Synthesizing POMDP policies : sampling meets model-checking via learning / Debraj Chakraborty, Anirban Majumdar, Prince Mathew, Sayan Mukherjee, and Jean-François Raskin

TACO : a toolsuite for the verification of threshold automata / Paul Eichler, Tom Baumeister, Mouhammad Sakr, Mahboubeh Kalateh Dowlati, Marcus Völp, and Swen Jacobs

Extending QuAK with nested quantitative automata / Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç, and Harun Yılmaz

VNN-LIB 2.0 : rigorous foundations for neural network verification / Ann Roy, Allen Antony, Andrea Gimelli, and Matthew L. Daggitt

QAV-FT : quadratic approximation-based neural network verification via Fourier series and Taylor truncation / Han Wang, Xuyang Ding, Ying Xie, and Yakun Sheng

The Rocq-NN-Roll prover : soundly verifying hyperproperties of neural networks in Rocq / Andrei Aleksandrov, Malte Jackisch, and Kim Völlinger

ATKVerifier : adaptive top-k constraints for tighter verification of semantic segmentation networks / Yuehao Liu, Cong Tian, Yansong Dong, Liang Zhao, Chao Huang, and Wensheng Wang

Precise verification of transformers through ReLU-catalyzed abstraction refinement / Hengjie Liu, Zhenya Zhang, and Jianjun Zhao

Quantifying sensitivity for tree ensembles : a symbolic and compositional approach / Ajinkya Naik, Chaitanya Garg, S. Akshay, Ashutosh Gupta, and Kuldeep S. Meel

Shields to guarantee probabilistic safety in MDPs / Linus Heck, Filip Macák, Roman Andriushchenko, Milan Češka, and Sebastian Junges

A neurosymbolic approach to natural language formalization and verification / Chenyang An, Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Victor Heorhiadi, Marc Hudak, Dejan Jovanović, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamarić, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen, and Jianan Yao

Notes:

Includes bibliographical references and index

Online resource; title from PDF title page (Springer Nature Link, viewed July 31, 2026)

Other Format:

Print version: CAV (Conference) (38th : 2026 : Lisbon, Portugal) Computer aided verification

ISBN:

9783032325266

3032325269

OCLC:

1609313401

Access Restriction:

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