


default search action
CAV 2025, Zagreb, Croatia - Part I
- Ruzica Piskac

, Zvonimir Rakamaric
:
Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I. Lecture Notes in Computer Science 15931, Springer 2025, ISBN 978-3-031-98667-3
Data Structure Verification
- Marco Faella

, Gennaro Parlato
:
Verifying Tree-Manipulating Programs via CHCs. 3-28 - Matthew Sotoudeh:

Automated Verification of Monotonic Data Structure Traversals in C. 29-55 - Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen, Hossein Hojjat, Philipp Rümmer, Thomas Wies:

Arithmetizing Shape Analysis. 56-80 - Ekanshdeep Gupta, Nisarg Patel, Thomas Wies:

Raven: An SMT-Based Concurrency Verifier. 81-106 - Marco Eilers

, Malte Schwerhoff
, Alexander J. Summers
, Peter Müller:
Fifteen Years of Viper. 107-123
Model Checking
- Lina Gerlach

, Tobias Winkler
, Erika Ábrahám
, Borzoo Bonakdarpour
, Sebastian Junges
:
Efficient Probabilistic Model Checking for Relational Reachability. 127-147 - Venkata Dhavala, Jan Hückelheim

, Paul D. Hovland
, Stephen F. Siegel
:
Verifying PETSc Vector Components Using CIVL. 148-161 - Hanyue Chen, Miaomiao Zhang, Frits W. Vaandrager:

Compositional Abstraction for Timed Systems with Broadcast Synchronization. 162-184 - Yuheng Su, Qiusong Yang, Yiwei Ci, Tianjun Bu, Ziyu Huang:

The rIC3 Hardware Model Checker. 185-199 - Hongjian Jiang, Anthony W. Lin

, Oliver Markgraf
, Philipp Rümmer
, Daniel Stan
:
sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses. 200-214 - Alessandro Cimatti, Alberto Griggio, Christopher Johannsen, Kristin Yvonne Rozier, Stefano Tonetta:

Infinite-State Liveness Checking with rlive. 215-236 - Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang:

Deeply Optimizing the SAT Solver for the IC3 Algorithm. 237-257 - Andrew Luka

, Yakir Vizel
:
Property Directed Reachability with Extended Resolution. 258-280 - Nils Froleyks

, Emily Yu
, Mathias Preiner
, Armin Biere
, Keijo Heljanko
:
Introducing Certificates to the Hardware Model Checking Competition. 281-295 - Zhengyang Lu

, Po-Chun Chien
, Nian-Ze Lee
, Arie Gurfinkel
, Vijay Ganesh
:
Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking. 296-311
Cryptography and Security
- Jon Stephens

, Shankara Pailoor
, Isil Dillig
:
Automated Verification of Consistency in Zero-Knowledge Proof Circuits. 315-338 - Elizaveta Pertseva

, Alex Ozdemir
, Shankara Pailoor
, Alp Bassa
, Sorawee Porncharoenwase
, Isil Dillig
, Clark W. Barrett
:
Integer Reasoning Modulo Different Constants in SMT. 339-362 - Robert J. Colvin

, Roger C. Su
:
Structural Operational Semantics for Functional and Security Verification of Pipelined Processors. 363-388 - Denis Mazzucato

, Abdalrhman Mohamed
, Juneyoung Lee
, Clark W. Barrett
, Jim Grundy, John Harrison, Corina S. Pasareanu
:
Relational Hoare Logic for Realistically Modelled Machine Code. 389-413

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














