Computer aided verification : 38th International Conference, CAV 2026, Lisbon, Portugal, July 26-29, 2026, Proceedings. Part I / 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 16682.

Lecture notes in computer science, 1611-3349 ; 16682

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

Other Title:

CAV 2026

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:

Learning to split : A reinforcement-learning-guided splitting heuristic for neural network verification (invited talk) / Maya Swisa and Guy Katz

On the complexity of checking soundness of natural reductions / Constantin Enea, Azadeh Farzan, and Dominik Klumpp

Deadlock verification via ordering-constrained mutex modeling / Pei Wang, Zhilei Han, Zhihang Sun, and Fei He

Complete local reasoning about parameterized programs over topologies / Ruotong Cheng and Azadeh Farzan

Scalable deductive verification of data-level parallel programs / Lars B. van den Haak, Anton Wijs, and Marieke Huisman

On the verification problem of remote direct memory access programs / Parosh Aziz Abdulla, Mohamed Faouzi Atig, Govind Rajanbabu, and Stephan Spengler

Model checking for flexible network protocols / Andrew Johnson, Dennis Fetterly, Sean Song, and Jonathan Zolla

The TLA+ model checker Apalache / Rodrigo Otoni, Shon Feder, Jure Kukovec, Andrey Kupriyanov, Gabriela Moreira, Philip Offtermatt, Thomas Pani, Thanh-Hai Tran, and Igor Konnov

PSF : A generic and extensible framework for protocol state fuzzing / Konstantinos Sagonas and Thanos Typaldos

Kofola 1.0 : A modular approach to ω-regular complementation and inclusion checking / Ondrej Alexaj, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Yong Li, and Nicolas Mazzocchi

Octopus : Practical equivalence checking of P4 packet parsers / Jort van Leenen and Tobias Kappé

Randomise alone, reach as a team / Léonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, and K. S. Thejaswini

Decoupled planning for multiple omega-regular objectives / Guy Avni, Thomas A. Henzinger, Kaushik Mallik, Suman Sadhukhan, and K. S. Thejaswini

Repairing regex-dependent string-manipulation programs / Nariyoshi Chida and Tachio Terauchi

Liquid tree automata / Ashish Mishra and Suresh Jagannathan

SemML 2.0 : Synthesizing controllers for LTL / Jan Křetínský, Tobias Meggendorfer, and Maximilian Prokop

Fast obligation translation and synthesis / Alexandre Duret-Lutz, Giuseppe De Giacomo, Marcin Jurdzinski, Nir Piterman, Moshe Y. Vardi, and Shufang Zhu

sweap : Reactive synthesis for infinite-state integer problems / Shaun Azzopardi, Luca Di Stefano, and Nir Piterman

A-IC3 : Learning-guided adaptive inductive generalization for hardware model checking / Xiaofeng Zhou, Guangyu Hu, Hongce Zhang, and Wei Zhang

A multi-width parametric bitvector equivalence solver / Luigi Rinaldi, John Wickerson, and Samuel Coward

Massively parallel mining of specifications for hardware designs / Leiqi Ye, Guy Frankel, Jianyi Cheng, and Elizabeth Polgreen

A mechanised, bidirectional type system for bit-width determination in SystemVerilog / Gabriel Desfrene, Quentin Corradi, Michalis Pardalos, and John Wickerson

Differentially private runtime monitoring / Bernd Finkbeiner and Frederik Scheerer

HyperLasso : Bounded model checking of ∀+∃+-liveness hyperproperties / Alcino Cunha, Hugo Pacheco, and Nuno Macedo

The simulator’s blueprint : Automata learning from cybersecurity logs / Tudor Braicu, Benjamin Ylvisaker, Nicolas Espinosa Dice, Yiding Chen, Yiyi Zhang, Nate Foster, and Hossein Hojjat

HyperQB 2.0 : A bounded model checker for hyperproperties / Tzu-Han Hsu, Milad Rabizadeh, Kenneth Rogale, Fedor Filippov, Marco A. de Oliveira Batista, and Borzoo Bonakdarpour

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:

9783032325198

3032325196

OCLC:

1609311700

Access Restriction:

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