|
| | 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 |  | Kovacs, Laura | The Vampire Diary | Inproceedings Konferenzbeitrag | Sep-2026 |
| 3 |  | Ferdowsi, Arman ; Kovacs, Laura | Certificate-Aware Property-Directed Reachability | Inproceedings Konferenzbeitrag | Sep-2026 |
| 4 |  | 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 |
| 5 |  | Kafshdar Goharshady, Amir ; Hader, Thomas ; Kovacs, Laura ; Motwani, Harshit Jitendra | Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields | Inproceedings Konferenzbeitrag | Sep-2026 |
| 6 |  | 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 |
| 7 | | Sallinger, Sarah Sophie ; Graussam, Lukas ; Weissenbacher, Georg ; Zuleger, Florian ; Ignatiev, Alexey | Consistency-Based Software Diagnosis: Accuracy, Scalability, and Limitations | Inproceedings Konferenzbeitrag | 24-Jul-2026 |
| 8 |  | Hajdu, Márton ; Hozzová, Petra ; Kovács, Laura ; Wagner, Eva Maria | Completeness of Synthesis Under Realizability Assumptions Using Superposition | Inproceedings Konferenzbeitrag | 24-Jul-2026 |
| 9 | | Bocevska, Ivana ; Tsukada, Takeshi ; Unno, Hiroshi ; Padon, Oded ; Shoham, Sharon | Lagrangian-Based Duality for Quantified SMT Algorithms | Inproceedings Konferenzbeitrag | 24-Jul-2026 |
| 10 | | Eiter, Thomas ; Nießen, Tobias ; Soldà, Davide | SAT Modulo Well-Founded Semantics | Inproceedings Konferenzbeitrag | 16-Jul-2026 |
| 11 | | Nießen, Tobias ; Paverd, Andrew | Trusted and Transparent Time-Stamping Through TEEs and Network Time Security | Inproceedings Konferenzbeitrag | 26-Apr-2026 |
| 12 | | Schreiber, Dominik ; Fleury, Mathias ; Fazekas, Katalin ; Biere, Armin | Real-time Proof Checking for Distributed Incremental SAT Solving | Inproceedings Konferenzbeitrag | 16-Apr-2026 |
| 13 | | Chen, Chen ; Kaufmann, Daniela ; Deng, Chenhui ; Song, Zhan ; Zhang, Hongce ; Yu, Cunxi | ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers | Inproceedings Konferenzbeitrag | 15-Apr-2026 |
| 14 |  | Sextl, Florian | Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust | Presentation Vortrag | 13-Apr-2026 |
| 15 | | King, Daragh ; Koutavas, Vasileios ; Kovacs, Laura | LLMs and fuzzing in tandem: a new approach to automatically generating weakest preconditions | Article Artikel | 12-Mar-2026 |
| 16 | | El Manssour, Rida Ait ; Kenison, George ; Shirmohammadi, Mahsa ; Varonka, Anton ; Worrell, James B | Determination Problems for Orbit Closures and Matrix Groups | Inproceedings Konferenzbeitrag | 8-Jan-2026 |
| 17 | | Kolluri, Aashish ; Sharma, Rishi ; Costa, Manuel ; Köpf, Boris ; Nießen, Tobias ; Russinovich, Mark ; Tople, Shruti ; Zanella Béguelin, Santiago | Optimizing Agent Planning for Security and Autonomy | Inproceedings Konferenzbeitrag | 2026 |
| 18 | | Moeini Jam, Mehran ; Kalantari, Hamed ; Khamespanah, Ehsan ; Sirjani, Marjan ; Movaghar, Ali | Compositional Verification of Timed Automata via Violation Assumptions | Inproceedings Konferenzbeitrag | 2026 |
| 19 | | Coutelier, Robin ; Hader, Thomas ; Kovacs, Laura | Generalizing CDCL with Graph Backtracking | Inproceedings Konferenzbeitrag | 2026 |
| 20 | | Eisenhofer, Clemens ; Seiser, Theodor ; Bjørner, Nikolaj ; Kovács, Laura | On Solving String Equations via Powers and Parikh Images | Inproceedings Konferenzbeitrag | 2026 |
| 21 | | Rawson, Michael ; Eisenhofer, Clemens ; Kovács, Laura | Constraint Learning for Non-confluent Proof Search | Inproceedings Konferenzbeitrag | 2026 |
| 22 |  | Correnson, Arthur ; Nießen, Tobias ; Finkbeiner, Bernd ; Weissenbacher, Georg | Symbolic execution for refuting ∀∃ hyperproperties | Article Artikel | Dec-2025 |
| 23 | | Rain, Sophie ; Petković Komel, Anja ; Rawson, Michael ; Kovacs, Laura | Game Modeling of Blockchain Protocols | Inproceedings Konferenzbeitrag | 15-Nov-2025 |
| 24 | | Winkler, Lorenz ; Kovács, Laura | Positive Almost-Sure Termination of Polynomial Random Walks | Inproceedings Konferenzbeitrag | 2-Oct-2025 |
| 25 | | Bocevska, Ivana ; Petković Komel, Anja ; Kovacs, Laura ; Rain, Sophie ; Rawson, Michael | Divide and Conquer: A Compositional Approach to Game-Theoretic Security | Article Artikel | Oct-2025 |
| 26 | | Bozga, Marius ; Iosif, Radu ; Zuleger, Florian | Regular Grammars for Sets of Graphs of Tree-Width 2 | Inproceedings Konferenzbeitrag | Oct-2025 |
| 27 | | Kaufmann, Daniela | Verifying Arithmetic Circuits with Polynomials | Presentation Vortrag | 24-Sep-2025 |
| 28 | | Bártek, Filip ; Bhayat, Ahmed ; Coutelier, Robin ; Hajdu, Márton ; Hetzenberger, Matthias ; Hozzová, Petra ; Kovács, Laura ; Rath, Jakob ; Rawson, Michael ; Reger, Giles ; Suda, Martin ; Schoisswohl, Johannes ; Voronkov, Andrei | The Vampire Diary | Inproceedings Konferenzbeitrag | 24-Sep-2025 |
| 29 | | Hajdu, Marton ; Kovács, Laura ; Voronkov, Andrei | Partial Redundancy in Saturation | Inproceedings Konferenzbeitrag | 24-Sep-2025 |
| 30 | | Pluska, Alexander ; Malhotra, Sagar | On Local Limits of Sparse Random Graphs: Color Convergence and the Refined Configuration Model | Inproceedings Konferenzbeitrag | 18-Sep-2025 |
| 31 | | Varonka, Anton ; Watanabe, Kazuki | On Piecewise Affine Reachability with Bellman Operators | Inproceedings Konferenzbeitrag | 20-Aug-2025 |
| 32 | | Hofstadler, Clemens ; Kaufmann, Daniela | Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification | Inproceedings Konferenzbeitrag | 8-Aug-2025 |
| 33 |  | Codel, Cayden ; Fazekas, Katalin ; Heule, Marijn J. H. ; Iser, Markus | Proceedings of SAT Competition 2025 : Solver and Benchmark Descriptions | Proceedings Tagungsband | Aug-2025 |
| 34 | | Hajdu, Marton ; Coutelier, Robin ; Kovacs, Laura ; Voronkov, Andrei | Term Ordering Diagrams | Inproceedings Konferenzbeitrag | 30-Jul-2025 |
| 35 | | Aminof, Benjamin ; Rubin, Sasha ; Spegni, Francesco ; Zuleger, Florian | Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems | Article Artikel | 24-Jun-2025 |
| 36 | | King, Daragh ; Koutavas, Vasileios ; Kovacs, Laura | LLM-based Generation of Weakest Preconditions and Precise Array Invariants | Inproceedings Konferenzbeitrag | 12-Jun-2025 |
| 37 |  | Kovacs, Laura | Automated Reasoning | Presentation Vortrag | Jun-2025 |
| 38 | | Rath, Jakob ; Eisenhofer, Clemens ; Kaufmann, Daniela ; Bjørner, Nikolaj ; Kovacs, Laura | PolySAT: Word-level Bit-vector Reasoning in Z3 | Inproceedings Konferenzbeitrag | 3-May-2025 |
| 39 | | Sextl, Florian ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration | Inproceedings Konferenzbeitrag | 1-May-2025 |
| 40 | | Kaufmann, Daniela ; Berthomieu, Jérémy | Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs | Inproceedings Konferenzbeitrag | 1-May-2025 |
| 41 | | Sextl, Florian ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract) | Presentation Vortrag | 21-Jan-2025 |
| 42 | | Moosbrugger, Marcel ; Müllner, Julian ; Bartocci, Ezio ; Kovacs, Laura | Polar: An Algebraic Analyzer for (Probabilistic) Loops | Book Contribution Buchbeitrag | 2025 |
| 43 | | Ait El Manssour, Rida ; Kenison, George ; Shirmohammadi, Mahsa ; Varonka, Anton | Simple Linear Loops: Algebraic Invariants and Applications | Inproceedings Konferenzbeitrag | 2025 |
| 44 | | Kaufmann, Daniela ; Hofstadler, Clemens | Recycling Algebraic Proof Certificates | Inproceedings Konferenzbeitrag | 2025 |
| 45 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Incremental Inprocessing Rules beyond Resolution | Inproceedings Konferenzbeitrag | 2025 |
| 46 | | Simader, Marcel ; Rebola-Pardo, Adrian ; Seidl, Martina | FERAT: A New Expansion-Based Certification Framework for Quantified Boolean Formulas | Inproceedings Konferenzbeitrag | 2025 |
| 47 |  | Irfan, Ahmed ; Kaufmann, Daniela | Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design – FMCAD 2025 | Proceedings Tagungsband | 2025 |
| 48 | | Bozga, Marius ; Iosif, Radu ; Zuleger, Florian | Iterating Non-Aggregative Structure Compositions | Inproceedings Konferenzbeitrag | 2025 |
| 49 | | Hajdu, Márton ; Hozzová, Petra ; Kovács, Laura ; Voronkov, Andrei ; Wagner, Eva Maria ; Žilinčík, Richard Steven | Synthesis Benchmarks for Automated Reasoning | Inproceedings Konferenzbeitrag | 2025 |
| 50 | | Fazekas, Katalin ; Niemetz, Aina ; Preiner, Mathias ; Kirchweger, Markus ; Szeider, Stefan ; Biere, Armin | Satisfiability Modulo User Propagators | Article Artikel | 27-Dec-2024 |
| 51 | | Pani, Thomas ; Weissenbacher, Georg ; Zuleger, Florian | Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification | Article Artikel | Dec-2024 |
| 52 |  | Brechelmacher, Otto ; Ničković, Dejan ; Nießen, Tobias ; Sallinger, Sarah Sophie ; Weissenbacher, Georg | Differential Property Monitoring for Backdoor Detection | Inproceedings Konferenzbeitrag | 29-Nov-2024 |
| 53 | | Loitzl, Alexander ; Zuleger, Florian | Modeling Register Pairs in CompCert | Inproceedings Konferenzbeitrag | 13-Nov-2024 |
| 54 |  | Coutelier, Robin ; Rath, Jakob ; Rawson, Michael ; Biere, Armin ; Kovacs, Laura | SAT solving for variants of first-order subsumption | Article Artikel | 11-Nov-2024 |
| 55 | | Aminof, Benjamin ; De Giacomo, Guiseppe ; Rubin, Sasha ; Zuleger, Florian | Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis | Inproceedings Konferenzbeitrag | Nov-2024 |
| 56 | | Fazekas, Katalin | SAT modulo IPASIR-UP | Presentation Vortrag | 14-Oct-2024 |
| 57 | | Rath, Jakob ; Eisenhofer, Clemens ; Kaufmann, Daniela ; Bjørner, Nikolaj ; Kovacs, Laura | PolySAT: Word-level Bit-vector Reasoning in Z3 | Presentation Vortrag | 14-Oct-2024 |
| 58 | | Correnson, Arthur ; Nießen, Tobias ; Finkbeiner, Bernd ; Weissenbacher, Georg | Finding ∀∃ Hyperbugs using Symbolic Execution | Article Artikel | 8-Oct-2024 |
| 59 | | Barrett, Clark ; Chen, Pei-Wei ; Cook, Byron ; Dutertre, Bruno ; Jones, Robert B. ; Le, Nham ; Reynolds, Andrew ; Sheth, Kunal ; Stephens, Christopher ; Whalen, Michael W. | SMT-D: New Strategies for Portfolio-Based SMT Solving | Inproceedings Konferenzbeitrag | Oct-2024 |
| 60 | | Priya, Siddharth ; Gurfinkel, Arie | Ownership in low-level intermediate representation | Inproceedings Konferenzbeitrag | Oct-2024 |
| 61 | | Kopinsky, Max ; Pientka, Brigitte ; Si, Xujie | Modernizing SMT-Based Type Error Localization | Inproceedings Konferenzbeitrag | Oct-2024 |
| 62 | | Dardik, Ian ; Porter, April ; Kang, Eunsuk | Recomposition: A New Technique for Efficient Compositional Verification | Inproceedings Konferenzbeitrag | Oct-2024 |
| 63 | | Biere, Armin ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils | Clausal Equivalence Sweeping | Inproceedings Konferenzbeitrag | Oct-2024 |
| 64 | | Zhou, Yi ; Bosamiya, Jay ; Li, Jessica G. ; Heule, Marijn J. H. ; Parno, Bryan | Context Pruning for More Robust SMT-based Program Verification | Inproceedings Konferenzbeitrag | Oct-2024 |
| 65 | | Blicha, Martin ; Tsiskaridze, Nestan | The FMCAD 2024 Student Forum | Inproceedings Konferenzbeitrag | Oct-2024 |
| 66 | | Codel, Cayden ; Avigad, Jeremy ; Heule, Marijn J. H. | Verified Substitution Redundancy Checking | Inproceedings Konferenzbeitrag | Oct-2024 |
| 67 | | Bonnot, Paul ; Boyer, Benoît ; Faissole, Florian ; Marché, Claude ; Rieu-Helft, Raphaël | Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function | Inproceedings Konferenzbeitrag | Oct-2024 |
| 68 | | Kamath, Adharsh ; Mohammed, Nausheen ; Senthilnathan, Aditya ; Chakraborty, Saikat ; Deligiannis, Pantazis ; Lahiri, Shuvendu K. ; Lal, Akash ; Rastogi, Aseem ; Roy, Subhajit ; Sharma, Rahul | Leveraging LLMs for Program Verification | Inproceedings Konferenzbeitrag | Oct-2024 |
| 69 | | Cleaveland, Rachel ; Trippel, Caroline | Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware | Inproceedings Konferenzbeitrag | Oct-2024 |
| 70 | | Redondi, Gianluca ; Cimatti, Alessandro ; Griggio, Alberto | Towards Verification Modulo Theories of asynchronous systems via abstraction refinement | Inproceedings Konferenzbeitrag | Oct-2024 |
| 71 | | Lahiri, Shuvendu K. | Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages | Inproceedings Konferenzbeitrag | Oct-2024 |
| 72 | | Ait El Manssour, Rida ; Kenison, George James ; Shirmohammadi, Mahsa ; Varonka, Anton | Simple Linear Loops: Algebraic Invariants and Synthesis | Presentation Vortrag | 19-Sep-2024 |
| 73 | | Sextl, Florian | With Biabduction towards Memory Safety across the Rust-C-FFI | Presentation Vortrag | 17-Sep-2024 |
| 74 | | Biere, Armin ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils | Clausal Congruence Closure | Inproceedings Konferenzbeitrag | 19-Aug-2024 |
| 75 | | Coutelier, Robin ; Fleury, Mathias ; Kovacs, Laura | Lazy Reimplication in Chronological Backtracking | Inproceedings Konferenzbeitrag | 19-Aug-2024 |
| 76 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Certifying Incremental SAT Solving | Presentation Vortrag | 23-Jul-2024 |
| 77 |  | Kofnov, Andrey ; Moosbrugger, Marcel ; Stankovic, Miroslav ; Bartocci, Ezio ; Bura, Efstathia | Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments | Article Artikel | 10-Jul-2024 |
| 78 | | Hader, Thomas ; Kaufmann, Daniela ; Irfan, Ahmed ; Graham-Lengrand, Stéphane ; Kovács, Laura | MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper) | Inproceedings Konferenzbeitrag | 1-Jul-2024 |
| 79 | | Indri, Patrick ; Blohm, Peter ; Athavale, Anagha ; Bartocci, Ezio ; Weissenbacher, Georg ; Maffei, Matteo ; Nickovic, Dejan ; Gärtner, Thomas ; Malhotra, Sagar | Distillation based Robustness Verification with PAC Guarantees | Inproceedings Konferenzbeitrag | 28-Jun-2024 |
| 80 | | Fazekas, Katalin | Incremental SAT Solvers in Practice | Presentation Vortrag | 26-Jun-2024 |
| 81 |  | Pluska, Alexander ; Welke, Pascal ; Gärtner, Thomas ; Malhotra, Sagar | Logical Distillation of Graph Neural Networks | Inproceedings Konferenzbeitrag | 24-Jun-2024 |
| 82 | | Nastran, Martin ; Peschek, Paul ; Walendzik, Izabela ; Rath, Jakob ; Fickl, Bernhard ; Schubert, Jasmin Sophia ; Szabo, Gabriel ; Wilhelm, Richard Arthur ; Schmidt, Jochen ; Eder, Dominik ; Bayer-Skoff, Bernhard | High-yield liquid phase exfoliation of graphene utilizing low boiling co-solvent solutions and ammonia | Presentation Vortrag | 24-Jun-2024 |
| 83 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Incremental Proofs for Bounded Model Checking | Inproceedings Konferenzbeitrag | 19-Jun-2024 |
| 84 | | Amrollahi, Daneshvar ; Bartocci, Ezio ; Kenison, George James ; Kovacs, Laura ; Moosbrugger, Marcel ; Stankovic, Miroslav | (Un)Solvable loop analysis | Article Artikel | 11-Jun-2024 |
| 85 |  | AL-Zu'bi, Mai ; Weissenbacher, Georg | Statistical Profiling of Micro-Architectural Traces and Machine Learning for Spectre Detection: A Systematic Evaluation | Inproceedings Konferenzbeitrag | 10-Jun-2024 |
| 86 | | Chimes, Mark Jonathan ; Iosif, Radu ; Zuleger, Florian | Tree-Verifiable Graph Grammars | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 87 |  | Georgiou, Pamina ; Hajdu, Marton ; Kovacs, Laura | Saturating Sorting without Sorts | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 88 |  | Hajdu, Marton ; Kovács, Laura ; Rawson, Michael | Rewriting and Inductive Reasoning | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 89 |  | Schoisswohl, Johannes ; Kovács, Laura ; Korovin, Konstantin | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 90 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Certifying Incremental SAT Solving | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 91 | | Dacík, Tomáš ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian | Deciding Boolean Separation Logic via Small Models | Inproceedings Konferenzbeitrag | 4-Apr-2024 |
| 92 | | Hitarth, S. ; Kenison, George James ; Kovacs, Laura ; Varonka, Anton | Linear Loop Synthesis for Quadratic Invariants | Inproceedings Konferenzbeitrag | 11-Mar-2024 |
| 93 | | Georgiou, Pamina ; Hajdu, Márton ; Kovács, Laura | Saturating Sorting without Sorts | Preprint Preprint | 6-Mar-2024 |
| 94 | | Sochor, Hannes ; Ferrarotti, Flavio ; Kaufmann, Daniela | Fuzzing-based grammar learning from a minimal set of seed inputs | Article Artikel | Mar-2024 |
| 95 |  | Nießen, Tobias ; Weissenbacher, Georg | Finding counterexamples to ∀∃ hyperproperties | Presentation Vortrag | 16-Jan-2024 |
| 96 | | Müllner, Julian ; Moosbrugger, Marcel ; Kovács, Laura | Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs | Article Artikel | 5-Jan-2024 |
| 97 |  | Eisenhofer, Clemens ; Kovács, Laura ; Rawson, Michael | Embedding the Connection Calculus in Satisfiability Modulo Theories | Inproceedings Konferenzbeitrag | Jan-2024 |
| 98 | | Jeanteur, Simon ; Kovács, Laura ; Maffei, Matteo ; Rawson, Michael | CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model | Inproceedings Konferenzbeitrag | 2024 |
| 99 | | Ciabattoni, Agata ; Eisenhofer, Clemens ; Rozplokhas, Dmitry | Strongly Analytic Calculi for KLM Logics with SMT-Based Prover | Inproceedings Konferenzbeitrag | 2024 |
| 100 |  | Pluska, Alexander ; Welke, Pascal ; Gärtner, Thomas ; Malhotra, Sagar | Logical Distillation of Graph Neural Networks | Inproceedings Konferenzbeitrag | 2024 |
