Editorial: Special issue on formal methods in computer-aided design Alberto GriggioNeha Rungta EditorialNotes 13 October 2025 Pages: 1 - 2
Formalization of robot collision detection method based on conformal geometric algebra Yingjie WuGuohui WangXimeng Li Research 03 October 2025
Correction: Hypercontracts Inigo IncerAlbert BenvenisteSanjit A. Seshia Correction Open access 05 August 2025 Pages: 529 - 530
Awaiting for Godot: stateless model checking that avoids executions where nothing happens Bengt JonssonMagnus LångKonstantinos Sagonas Research Open access 25 July 2025 Pages: 71 - 105
Predicate abstraction for hyperliveness verification Raven BeutnerBernd Finkbeiner Research Open access 16 July 2025 Pages: 238 - 277
Rounding meets approximate model counting Jiong YangKuldeep S. Meel Research Open access 11 July 2025 Pages: 189 - 221
Automatic assume-guarantee reasoning for safety and liveness using passive learning Ocan Sankur Research 09 July 2025 Pages: 498 - 528
Hypercontracts Inigo IncerAlbert BenvenisteSanjit A. Seshia Research Open access 10 June 2025 Pages: 455 - 497
Linearization, model reduction and reachability in nonlinear odes Michele BorealeLuisa Collodi OriginalPaper Open access 24 May 2025 Pages: 419 - 454
Variable automata over infinite alphabets Orna GrumbergOrna KupfermanSarai Sheinvald Research Open access 20 May 2025 Pages: 376 - 418
Timed causal fanin analysis for symbolic simulation Roope KaivolaNeta Bar Kama Research 16 May 2025 Pages: 3 - 26
Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs Alex OzdemirRiad S. WahbyClark Barrett Research 03 May 2025 Pages: 161 - 188
Automatic WSTS-based repair and deadlock detection of parameterized systems Tom BaumeisterSwen JacobsMarcus Völp Research Open access 18 April 2025 Pages: 335 - 375
Memory-efficient fixpoint computation Sung Kook KimArnaud J. VenetAditya V. Thakur OriginalPaper Open access 10 April 2025 Pages: 133 - 162
Preface of the special issue on the static analysis symposium 2020 and 2022 David PichardieMihaela SighireanuCaterina Urban EditorialNotes 07 April 2025 Pages: 1 - 3
Preface of the special issue on the Conference on Computer-Aided Verification 2022 Sharon ShohamYakir Vizel EditorialNotes 31 March 2025 Pages: 131 - 133
Golem: a flexible and efficient solver for constrained Horn clauses Martin BlichaKonstantin BritikovNatasha Sharygina Research Open access 26 March 2025 Pages: 143 - 160
Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement Stanley BakSergiy BogomolovKostiantyn Potomkin Research 18 March 2025 Pages: 307 - 333
Construction of verifier combinations from off-the-shelf components Dirk BeyerSudeep KanavCedric Richter OriginalPaper Open access 11 March 2025 Pages: 99 - 130
Towards neural-network-guided program synthesis and verification Naoki KobayashiTaro SekiyamaHiroshi Unno OriginalPaper Open access 24 February 2025 Pages: 222 - 254
A scalable entropy estimator Priyanka GoliaBrendan JubaKuldeep S. Meel Research 15 January 2025 Pages: 170 - 194
Data-driven invariant learning for probabilistic programs Jialu BaoNitesh TrivediSubhajit Roy Research 03 December 2024 Pages: 278 - 306
Correction: (Un)Solvable loop analysis Daneshvar AmrollahiEzio BartocciMiroslav Stankovič Correction Open access 20 November 2024
SAT solving for variants of first-order subsumption Robin CoutelierJakob RathLaura Kovács OriginalPaper Open access 11 November 2024 Pages: 27 - 70
Abstraction Modulo Stability Anna BecchiAlessandro Cimatti Research Open access 12 September 2024 Pages: 134 - 169
PAC statistical model checking of mean payoff in discrete- and continuous-time MDP Chaitanya AgarwalShibashis GuhaM. Pazhamalai Research Open access 17 August 2024 Pages: 195 - 237
A verified durable transactional mutex lock for persistent x86-TSO Eleni Vafeiadi BilaBrijesh Dongol Research Open access 31 July 2024 Pages: 237 - 282
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021 Aws AlbarghouthiRustan LeinoCaterina Urban EditorialNotes 25 July 2024 Pages: 1 - 4
Formally understanding Rust’s ownership and borrowing system at the memory level Shuanglong KanZhe ChenYang Liu OriginalPaper 09 July 2024 Pages: 200 - 236
The hexatope and octatope abstract domains for neural network verification Stanley BakTaylor DohmenPiotr Wojciechowski Research 17 June 2024 Pages: 178 - 199
Runtime verification of partially-synchronous distributed system Ritam GangulyAnik MomtazBorzoo Bonakdarpour OriginalPaper 14 June 2024 Pages: 146 - 177
An input–output relational domain for algebraic data types and functional arrays Santiago BautistaThomas JensenBenoît Montagu Research 13 June 2024 Pages: 231 - 304
Partial program analysis for staged compilation systems Aditya AnandManas Thakur Research 13 June 2024 Pages: 195 - 230
(Un)Solvable loop analysis Daneshvar AmrollahiEzio BartocciMiroslav Stankovič Research Open access 11 June 2024 Pages: 163 - 194
Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation Alexander KonradChristoph SchollRolf Drechsler OriginalPaper Open access 24 May 2024 Pages: 106 - 142
Information-flow interfaces Ezio BartocciThomas FerrèreAna Oliveira da Costa OriginalPaper Open access 23 May 2024 Pages: 3 - 48
Dynamic dependability analysis of shuffle-exchange networks Yassmeen ElderhalliOsman HasanSofiène Tahar OriginalPaper 15 May 2024 Pages: 285 - 325
Mining of extended signal temporal logic specifications with ParetoLib 2.0 Akshay MambakamJosé Ignacio Requeno JaraboThao Dang OriginalPaper Open access 06 May 2024 Pages: 260 - 284
Software doping analysis for human oversight Sebastian BiewerKevin BaumFranz Lehr OriginalPaper Open access 04 April 2024 Pages: 49 - 98
Preface for the Formal Methods in System Design special issue on ‘FASE 2022’ Einar Broch JohnsenManuel Wimmer EditorialNotes 02 April 2024 Pages: 1 - 2
Porous invariants for linear systems Engel LefaucheuxJoël OuaknineJames Worrell OriginalPaper Open access 28 February 2024 Pages: 235 - 271
Parameter synthesis for Markov models: covering the parameter space Sebastian JungesErika ÁbrahámMatthias Volk OriginalPaper Open access 17 February 2024 Pages: 181 - 259
Bounded-memory runtime enforcement with probabilistic and performance analysis Saumya ShankarAnkit PradhanYliès Falcone OriginalPaper 14 February 2024 Pages: 141 - 180
Termination of triangular polynomial loops Marcel HarkFlorian FrohnJürgen Giesl OriginalPaper Open access 04 December 2023 Pages: 70 - 132
Extending rely-guarantee thinking to handle real-time scheduling Cliff B. JonesAlan Burns OriginalPaper Open access 30 November 2023 Pages: 119 - 140
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification Thomas PaniGeorg WeissenbacherFlorian Zuleger OriginalPaper Open access 06 October 2023 Pages: 108 - 145
Certified SAT solving with GPU accelerated inprocessing Muhammad OsamaAnton WijsArmin Biere Original Article Open access 02 August 2023 Pages: 79 - 118
Round- and context-bounded control of dynamic pushdown systems Benedikt BolligMathieu LehautNathalie Sznajder Original Article Open access 07 July 2023 Pages: 41 - 78
Memory access protocols: certified data-race freedom for GPU kernels Tiago CogumbreiroJulien LangeHannah Zicarelli OriginalPaper 26 May 2023 Pages: 134 - 171
Compositional verification of priority systems using sharp bisimulation Luca Di StefanoFrédéric Lang OriginalPaper 17 May 2023 Pages: 1 - 40
