|
| | Preview | Authors / Editors | Title | Type | Issue Date |
| 1 |  | Dutertre, Bruno ; Könighofer, Bettina | Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026 | Proceedings Tagungsband    | Sep-2026 |
| 2 |  | Barth, Max ; Jakobs, Marie-Christine | Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement | Inproceedings Konferenzbeitrag | Sep-2026 |
| 3 |  | Kinská, Tereza ; Kretinsky, Jan ; Meggendorfer, Tobias ; Rieder, Sabine ; Weininger, Maximilian | dtControl2+ε: Trading Optimality for Explainability in MDPs via Decision Trees | Inproceedings Konferenzbeitrag | Sep-2026 |
| 4 |  | Looney, Jesse ; Bjørner, Nikolaj ; Wu, Haoze ; Narodytska, Nina | Weight-Aware Transformations for MaxSAT | Inproceedings Konferenzbeitrag | Sep-2026 |
| 5 |  | Tan, Yong Kiam ; Schreiber, Dominik ; Åman Pohjola, Johannes ; Myreen, Magnus O. | Verified Real-time Proof Checking for Large-Scale SAT Solving | Inproceedings Konferenzbeitrag | Sep-2026 |
| 6 |  | Onderka, Jan ; Biere, Armin ; Fleury, Mathias | Lean Certified Bitvector Solving without Bitblasting | Inproceedings Konferenzbeitrag | Sep-2026 |
| 7 |  | Nadel, Alexander ; Slonimski, Yam ; Strichman, Ofer | Aperture: an Anytime, Complete and Incremental MaxSAT Solver | Inproceedings Konferenzbeitrag | Sep-2026 |
| 8 |  | Mohamed, Mudathir ; Reynolds, Andrew ; Tinelli, Cesare ; Barrett, Clark | Solving LIA⋆ Constraints Using Hilbert Bases | Inproceedings Konferenzbeitrag | Sep-2026 |
| 9 |  | Kovacs, Laura | The Vampire Diary | Inproceedings Konferenzbeitrag | Sep-2026 |
| 10 |  | Wolf, Claire Xenia | The Parable of the Square-Dancing Witches and Wizards | Inproceedings Konferenzbeitrag | Sep-2026 |
| 11 |  | Barrett, Clark | CSLib: Building a Platform for AI-assisted Formal Verification in Lean | Inproceedings Konferenzbeitrag | Sep-2026 |
| 12 |  | Hance, Travis | Verifying Rust code with Verus | Inproceedings Konferenzbeitrag | Sep-2026 |
| 13 |  | Alshnakat, Anoud ; Guanciale, Roberto ; Dam, Mads | PolyGram: A Certifying Compiler for Network Policies | Inproceedings Konferenzbeitrag | Sep-2026 |
| 14 |  | frankel, guy ; Schneider, Rudi ; Steuwer, Michel ; Polgreen, Elizabeth | Synthesis with Counterexample Guided Observational Equivalence Graphs | Inproceedings Konferenzbeitrag | Sep-2026 |
| 15 |  | Saccomani, Pedro ; Mohamed, Abdalrhman ; Pertseva, Elisaveta ; Kaufmann, Daniela ; Tinelli, Cesare ; Barrett, Clark ; Barbosa, Haniel | Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean | Inproceedings Konferenzbeitrag | Sep-2026 |
| 16 |  | Gallego Hernández, Jorge ; Lipparini, Enrico ; Mansutti, Alessio | MCSAT Modulo Transcendental Arithmetics | Inproceedings Konferenzbeitrag | Sep-2026 |
| 17 |  | Kafshdar Goharshady, Amir ; Hader, Thomas ; Kovacs, Laura ; Motwani, Harshit Jitendra | Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields | Inproceedings Konferenzbeitrag | Sep-2026 |
| 18 |  | Cheung, Andrew ; Nandi, Chandrakana ; Lerner, Sorin | Conditional Rewrite Rule Synthesis Using E-Graphs and Implication Propagation | Inproceedings Konferenzbeitrag | Sep-2026 |
| 19 |  | Shalmon, Yogev ; Nadel, Alexander ; Strichman, Ofer | NobleCount: Revisiting a Forgotten Data Structure for Local Search in SAT | Inproceedings Konferenzbeitrag | Sep-2026 |
| 20 |  | Ehlers, Rüdiger ; Hölzner, Nils ; Kühnel, Tobias | Translating LTL to Lasso Automata | Inproceedings Konferenzbeitrag | Sep-2026 |
| 21 |  | Wojciechowski, Piotr ; Subramani, K. | F-QLPs over unit relative constraints | Inproceedings Konferenzbeitrag | Sep-2026 |
| 22 |  | Isac, Omri ; Refaeli, Idan ; Wu, Haoze ; Barrett, Clark ; Katz, Guy | PICID: Proof-Driven Clause Learning in Neural Network Verification | Inproceedings Konferenzbeitrag | Sep-2026 |
| 23 |  | Sankur, Ocan ; Jeron, Thierry ; Markey, Nicolas ; David, Mentré ; Noguchi, Reiya | Requirement-Based Testing: Enhancing Reinforcement Learning with Game Theory | Inproceedings Konferenzbeitrag | Sep-2026 |
| 24 |  | Zhang, Shimin ; Xia, Yechuan ; Li, Chunxiao ; Li, Jianwen ; M.Y. Vardi ; Ganesh, Vijay | Understanding CDCL Solvers via Scalability Studies and Proofdoors | Inproceedings Konferenzbeitrag | Sep-2026 |
| 25 |  | Paul, Sheryl ; Kudalkar, Vidisha ; Balakrishnan, Anand ; Lindemann, Lars ; Speranzon, Alberto ; Deshmukh, Jyotirmoy V. | Multi-Agent Planning with Spatio-Temporal and Topological Constraints using STL-GO | Inproceedings Konferenzbeitrag | Sep-2026 |
| 26 |  | Elsaleh, Raya ; Davis, Liam ; Wu, Haoze ; Katz, Guy | Incremental Neural Network Verification via Learned Conflicts | Inproceedings Konferenzbeitrag | Sep-2026 |
| 27 |  | Aniva, Leni ; Oikawa, Iori ; Dill, David ; Barrett, Clark | Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4 | Inproceedings Konferenzbeitrag | Sep-2026 |
| 28 |  | Looney, Jesse ; McDonald, Jonah ; Klingler, Allison ; Wu, Gloria ; Pulaj, Jonad ; Wu, Haoze | Solution Space Partitioning for Extremal Set Theory | Inproceedings Konferenzbeitrag | Sep-2026 |
| 29 |  | Gupta, Ekanshdeep ; Wies, Thomas | An Extension API for the Concurrent Program Verifier Raven | Inproceedings Konferenzbeitrag | Sep-2026 |
| 30 |  | Kakishita, Sinai ; Hasegawa, Akira ; Aoki, Toshiaki ; Kambe, Ryuta ; Takano, Yuuki | Verifying a Memory Allocator for Rust | Inproceedings Konferenzbeitrag | Sep-2026 |
| 31 |  | Choi, Jaehyeok ; Miner, Andrew | Binary Decision Diagrams Unchained | Inproceedings Konferenzbeitrag | Sep-2026 |
| 32 |  | Kabra, Aditi ; Laurent, Jonathan ; Martins, Ruben ; Mitsch, Stefan ; Platzer, André | LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Games | Inproceedings Konferenzbeitrag | Sep-2026 |
| 33 |  | Bartoletti, Massimo ; Marchesin, Riccardo ; Zunino, Roberto | Certifying optimal MEV strategies with Lean | Inproceedings Konferenzbeitrag | Sep-2026 |
| 34 |  | Campos, Tiago ; Tourret, Sophie ; Jasmin Blanchette ; Barbosa, Haniel | IsaAbduct: A Multi-Strategy Abduction Pipeline for Isabelle/HOL | Inproceedings Konferenzbeitrag | Sep-2026 |
| 35 |  | Christopher Johannsen ; Kristin Y. Rozier | Shrinking Mission-time LTL Runtime Monitors with Equality Saturation | Inproceedings Konferenzbeitrag | Sep-2026 |
| 36 |  | Lee A. Barnett ; D’Antoni, Loris ; Goel, Amit ; Kıcı, Rami Gökhan ; King, Tim ; Luckow, Kasper ; Rungta, Neha ; Sharoda, Yasmine | Efficient Enumeration of Cloud Access Permissions | Inproceedings Konferenzbeitrag | Sep-2026 |
| 37 |  | Weiss, Gera ; Zisser, Jules | Conditional Sampling of Symbolic Markov Chains | Inproceedings Konferenzbeitrag | Sep-2026 |
| 38 |  | Schmidt, Jule ; Weininger, Maximilian ; Dubslaff, Clemens ; Parker, David ; Jansen, Nils | Property-driven Causal Abstractions for Markov Decision Processes | Inproceedings Konferenzbeitrag | Sep-2026 |
| 39 |  | Joseph Tafese ; Gurfinkel, Arie ; Bayless, Sam ; Feng, Nick ; Hooshyar, Milad | Verifiable Checks for Business Rule Consistency | Inproceedings Konferenzbeitrag | Sep-2026 |
| 40 |  | Torlak, Emina | SymCert: Verifying SMT-Based Policy Analyses | Inproceedings Konferenzbeitrag | Sep-2026 |
| 41 |  | Fantinato, Filippo ; Cimatti, Alessandro ; Tonetta, Stefano | Symbolic Automata for MTL∞0 with Super-Dense Semantics | Inproceedings Konferenzbeitrag | Sep-2026 |
| 42 |  | Adame, Berhan Oumer ; Bogaerts, Bart ; Bogø, Benjamin ; Dold, Simon ; GONTIER, Arthur ; Koops, Wietze ; McCreesh, Ciaran ; McIlree, Matthew ; Nordström, Jakob ; Oertel, Andy ; Rebola Pardo, Adrian ; Turnbull, Mark Paul | Trimming Pseudo-Boolean Proofs | Inproceedings Konferenzbeitrag | Sep-2026 |
| 43 |  | Rowney, Tate ; Ahuja, Riyaz ; Avigad, Jeremy ; Welleck, Sean | DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs | Inproceedings Konferenzbeitrag | Sep-2026 |
| 44 |  | Rigi-Luperti, Niccolò ; Biere, Armin ; Schreiber, Dominik | Parallel SAT Sweeping on CNFs | Inproceedings Konferenzbeitrag | Sep-2026 |
| 45 |  | Lyu, Shuangyu ; Luo, Chuan ; Shi, Ruizhi ; Duan, Yuechen ; Hu, Chunming | SATDiv: An Effective Solver for Diverse SAT Problem | Inproceedings Konferenzbeitrag | Sep-2026 |
| 46 |  | Fiege, Nicolai ; Lange, Martin | Optimising Constant Matrix Multiplication Circuits is NP-complete | Inproceedings Konferenzbeitrag | Sep-2026 |
| 47 |  | Kouteili, Sam ; Fishell, William ; Santolucito, Mark ; Piskac, Ruzica | Learning GR(1) Specifications from Traces | Inproceedings Konferenzbeitrag | Sep-2026 |
| 48 |  | Schindler, Tanja ; Lee A. Barnett | The FMCAD 2026 Student Forum | Inproceedings Konferenzbeitrag | Sep-2026 |
| 49 |  | Sheth, Kunal ; Achour, Sara | Lemma Pattern Matching for SMT-based Verification of Analog Mixed-Signal Hardware | Inproceedings Konferenzbeitrag | Sep-2026 |
| 50 |  | Seufert, Tobias ; Scholl, Christoph | Certified Sequential Sweep Without Unrolling | Inproceedings Konferenzbeitrag | Sep-2026 |
| 51 |  | Shapiro, Ilana ; Lerner, Sorin ; Bjørner, Nikolaj | Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection | Inproceedings Konferenzbeitrag | Sep-2026 |
| 52 |  | Ng, Chi-Kit ; Chuang, Chih-Hsiang ; Jiang, Jie-Hong R. | Stochastic Boolean Satisfiability for Two-Player Sequential Games under Uncertainty | Inproceedings Konferenzbeitrag | Sep-2026 |
| 53 |  | Grieskamp, Wolfgang ; Zhang, Teng ; Kashyap, Vineeth ; Silverman, Jake | Formal Verification of Imperative First-Class Functions in Move | Inproceedings Konferenzbeitrag | Sep-2026 |
| 54 |  | Ceragioli, Lorenzo ; GALLETTA, LETTERIO ; Lunati, Edoardo | Checking Information Flow in Cloud-based IoT Access Control Policies | Inproceedings Konferenzbeitrag | Sep-2026 |
| 55 |  | Koll, Charles ; Rosulek, Mike ; Abbas, Houssam | Privacy-Preserving Robust Monitoring of Dense-Time Temporal Logic | Inproceedings Konferenzbeitrag | Sep-2026 |
| 56 |  | Ratners, Jakovs ; Tihomorskis, Nikolajs ; Aboltins, Arturs | Ordering-Relation Abstraction for Formal Verification of Bubble Errors in CARRY8-Based Tapped Delay Lines | Inproceedings Konferenzbeitrag | Sep-2026 |
| 57 |  | Jonáš, Martin ; Petřivalská, Lea ; Šárník, Jakub | On the Complexity of Word-Level Model Checking with Arrays | Inproceedings Konferenzbeitrag | Sep-2026 |
| 58 |  | Michael, Alicia ; Coughlin, Nicholas ; Lam, Kait ; Winter, Kirsten | Validated Binary Decompilation Without Tears | Inproceedings Konferenzbeitrag | Sep-2026 |
| 59 |  | Egolf, Derek ; Zhou, Yuhao ; Tripakis, Stavros | Can LLMs Perform Synthesis? | Inproceedings Konferenzbeitrag | Sep-2026 |
| 60 |  | Shih, Yu-An ; Cho, Soohyuk ; Gupta, Aarti ; Malik, Sharad | SVAEval: An Evaluation Framework for LLM-based SVA Property Generators | Inproceedings Konferenzbeitrag | Sep-2026 |
| 61 |  | Liu, Jun ; Liu, Jingxuan ; Yuan, Shenghao ; Sanan, David ; Chen, Kang ; Cao, Donggang ; Zhao, Yongwang | Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees | Inproceedings Konferenzbeitrag | Sep-2026 |
| 62 |  | Demir, Arınç ; Ulus, Dogan | Multi-Property Temporal Logic Monitoring | Inproceedings Konferenzbeitrag | Sep-2026 |
| 63 |  | Frenkel, Hadar ; Sheinvald, Sarai | On the Hierarchy of Finite-Word Hyperlanguages | Inproceedings Konferenzbeitrag | Sep-2026 |
| 64 |  | Kent, Zachary ; Shah, Amar | Parallelizing Congruence Closure | Inproceedings Konferenzbeitrag | Sep-2026 |
| 65 |  | Vlačić, Verner | Beyond Lemma Sharing – Novel Parallelization Strategies for PDR | Inproceedings Konferenzbeitrag | Sep-2026 |
| 66 |  | Peyrer, Cynthia ; Maximilian Heisinger ; Seidl, Martina | ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework | Inproceedings Konferenzbeitrag | Sep-2026 |
| 67 |  | Austin, Pete ; Dell'Erba, Daniele ; Totzke, Patrick | The Game Graph Gym | Inproceedings Konferenzbeitrag | Sep-2026 |
| 68 |  | Schwartz, Noah ; Nagesh, Chandra Kanth ; Sankaranarayanan, Sriram ; Kaur, Ramneet ; Sahai, Tuhin ; Jha, Susmit | Optimized Piecewise Affine Abstractions of Neural Networks with Learnable Activation Functions | Inproceedings Konferenzbeitrag | Sep-2026 |
| 69 |  | Chang, Tung-Che ; Park, Sehyeok ; Lim, Jay ; Nagarakatte, Santosh | Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean | Inproceedings Konferenzbeitrag | Sep-2026 |
| 70 |  | Ferdowsi, Arman ; Kovacs, Laura | Certificate-Aware Property-Directed Reachability | Inproceedings Konferenzbeitrag | Sep-2026 |
| 71 |  | Elboher, Yizhak ; Peleg, Reuven ; Shi, Zhouxing ; Katz, Guy ; Kretinsky, Jan | Talking with Verifiers: Automatic Specification Generation for Neural Network Verification | Inproceedings Konferenzbeitrag | Sep-2026 |
| 72 |  | Zhang, Dexin ; Alberdingk Thijm, Timothy ; Walker, David ; Gupta, Aarti | CB-VER: A Stable Foundation for Modular Network Control Plane Verification | Inproceedings Konferenzbeitrag | Sep-2026 |
| 73 |  | Yang, Dao Bo ; Gurfinkel, Arie ; Trefler, Richard | Prophecy Variables and Invariants in the Move Prover | Inproceedings Konferenzbeitrag | Sep-2026 |
| 74 |  | Bai, Alexander ; Hawblitzel, Chris ; Lattuada, Andrea | Tunable Automation in Automated Program Verification | Inproceedings Konferenzbeitrag | Sep-2026 |
| 75 |  | Mafra, Augusto ; Barbosa, Haniel | Formal Verification of Mixed-Signal Systems Using Real Number Modeling with SMT-based Model Checking | Inproceedings Konferenzbeitrag | Sep-2026 |
| 76 |  | Li, Xuyang ; Xia, Jiahao ; Adnan, Ahmed ; Wang, Jingbo | PSouffĺe: Scaling Exact Probabilistic Logic Inference for Program Analysis | Inproceedings Konferenzbeitrag | Sep-2026 |
