|
| | Preview | Authors / Editors | Title | Type | Issue Date |
| 1 |  | Sextl, Florian | Brushing off the Rust: Towards Compositional Memory Safety Verification for unsafe Rust | Presentation Vortrag   | 13-Apr-2026 |
| 2 | | King, Daragh ; Koutavas, Vasileios ; Kovacs, Laura | LLMs and fuzzing in tandem: a new approach to automatically generating weakest preconditions | Article Artikel  | 12-Mar-2026 |
| 3 | | 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 |
| 4 | | Rawson, Michael ; Eisenhofer, Clemens ; Kovács, Laura | Constraint Learning for Non-confluent Proof Search | Inproceedings Konferenzbeitrag | 2026 |
| 5 | | Eisenhofer, Clemens ; Seiser, Theodor ; Bjørner, Nikolaj ; Kovács, Laura | On Solving String Equations via Powers and Parikh Images | Inproceedings Konferenzbeitrag | 2026 |
| 6 |  | Correnson, Arthur ; Nießen, Tobias ; Finkbeiner, Bernd ; Weissenbacher, Georg | Symbolic execution for refuting ∀∃ hyperproperties | Article Artikel | Dec-2025 |
| 7 | | Rain, Sophie ; Petković Komel, Anja ; Rawson, Michael ; Kovacs, Laura | Game Modeling of Blockchain Protocols | Inproceedings Konferenzbeitrag | 15-Nov-2025 |
| 8 | | Hajdu, Márton ; Hozzová, Petra ; Kovacs, Laura ; Voronkov, Andrei ; Wagner, Eva Maria ; Žilinčík, Richard Steven | Synthesis Benchmarks for Automated Reasoning | Inproceedings Konferenzbeitrag | 8-Oct-2025 |
| 9 | | Winkler, Lorenz ; Kovács, Laura | Positive Almost-Sure Termination of Polynomial Random Walks | Inproceedings Konferenzbeitrag | 2-Oct-2025 |
| 10 | | 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 |
| 11 | | Bozga, Marius ; Iosif, Radu ; Zuleger, Florian | Regular Grammars for Sets of Graphs of Tree-Width 2 | Inproceedings Konferenzbeitrag | Oct-2025 |
| 12 | | Hajdu, Marton ; Kovács, Laura ; Voronkov, Andrei | Partial Redundancy in Saturation | Inproceedings Konferenzbeitrag | 24-Sep-2025 |
| 13 | | Kaufmann, Daniela | Verifying Arithmetic Circuits with Polynomials | Presentation Vortrag | 24-Sep-2025 |
| 14 | | 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 |
| 15 | | Pluska, Alexander ; Malhotra, Sagar | On Local Limits of Sparse Random Graphs: Color Convergence and the Refined Configuration Model | Inproceedings Konferenzbeitrag | 18-Sep-2025 |
| 16 | | Varonka, Anton ; Watanabe, Kazuki | On Piecewise Affine Reachability with Bellman Operators | Inproceedings Konferenzbeitrag | 20-Aug-2025 |
| 17 | | Hofstadler, Clemens ; Kaufmann, Daniela | Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification | Inproceedings Konferenzbeitrag | 8-Aug-2025 |
| 18 |  | Codel, Cayden ; Fazekas, Katalin ; Heule, Marijn J. H. ; Iser, Markus | Proceedings of SAT Competition 2025 : Solver and Benchmark Descriptions | Proceedings Tagungsband | Aug-2025 |
| 19 | | Hajdu, Marton ; Coutelier, Robin ; Kovacs, Laura ; Voronkov, Andrei | Term Ordering Diagrams | Inproceedings Konferenzbeitrag | 30-Jul-2025 |
| 20 | | Aminof, Benjamin ; Rubin, Sasha ; Spegni, Francesco ; Zuleger, Florian | Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems | Article Artikel | 24-Jun-2025 |
| 21 | | King, Daragh ; Koutavas, Vasileios ; Kovacs, Laura | LLM-based Generation of Weakest Preconditions and Precise Array Invariants | Inproceedings Konferenzbeitrag | 12-Jun-2025 |
| 22 |  | Kovacs, Laura | Automated Reasoning | Presentation Vortrag | Jun-2025 |
| 23 | | Rath, Jakob ; Eisenhofer, Clemens ; Kaufmann, Daniela ; Bjørner, Nikolaj ; Kovacs, Laura | PolySAT: Word-level Bit-vector Reasoning in Z3 | Inproceedings Konferenzbeitrag | 3-May-2025 |
| 24 | | Sextl, Florian ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian | Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration | Inproceedings Konferenzbeitrag | 1-May-2025 |
| 25 | | 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 |
| 26 | | 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 |
| 27 | | Moosbrugger, Marcel ; Müllner, Julian ; Bartocci, Ezio ; Kovacs, Laura | Polar: An Algebraic Analyzer for (Probabilistic) Loops | Book Contribution Buchbeitrag | 2025 |
| 28 | | Ait El Manssour, Rida ; Kenison, George ; Shirmohammadi, Mahsa ; Varonka, Anton | Simple Linear Loops: Algebraic Invariants and Applications | Inproceedings Konferenzbeitrag | 2025 |
| 29 | | Irfan, Ahmed ; Kaufmann, Daniela | Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design – FMCAD 2025 | Proceedings Tagungsband | 2025 |
| 30 | | Kaufmann, Daniela ; Hofstadler, Clemens | Recycling Algebraic Proof Certificates | Inproceedings Konferenzbeitrag | 2025 |
| 31 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Incremental Inprocessing Rules beyond Resolution | Inproceedings Konferenzbeitrag | 2025 |
| 32 | | Bozga, Marius ; Iosif, Radu ; Zuleger, Florian | Iterating Non-Aggregative Structure Compositions | Inproceedings Konferenzbeitrag | 2025 |
| 33 | | Simader, Marcel ; Rebola-Pardo, Adrian ; Seidl, Martina | FERAT: A New Expansion-Based Certification Framework for Quantified Boolean Formulas | Inproceedings Konferenzbeitrag | 2025 |
| 34 | | Fazekas, Katalin ; Niemetz, Aina ; Preiner, Mathias ; Kirchweger, Markus ; Szeider, Stefan ; Biere, Armin | Satisfiability Modulo User Propagators | Article Artikel | 27-Dec-2024 |
| 35 | | 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 |
| 36 |  | Brechelmacher, Otto ; Ničković, Dejan ; Nießen, Tobias ; Sallinger, Sarah Sophie ; Weissenbacher, Georg | Differential Property Monitoring for Backdoor Detection | Inproceedings Konferenzbeitrag | 29-Nov-2024 |
| 37 | | Loitzl, Alexander ; Zuleger, Florian | Modeling Register Pairs in CompCert | Inproceedings Konferenzbeitrag | 13-Nov-2024 |
| 38 |  | Coutelier, Robin ; Rath, Jakob ; Rawson, Michael ; Biere, Armin ; Kovacs, Laura | SAT solving for variants of first-order subsumption | Article Artikel | 11-Nov-2024 |
| 39 | | 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 |
| 40 | | Fazekas, Katalin | SAT modulo IPASIR-UP | Presentation Vortrag | 14-Oct-2024 |
| 41 | | Rath, Jakob ; Eisenhofer, Clemens ; Kaufmann, Daniela ; Bjørner, Nikolaj ; Kovacs, Laura | PolySAT: Word-level Bit-vector Reasoning in Z3 | Presentation Vortrag | 14-Oct-2024 |
| 42 | | Correnson, Arthur ; Nießen, Tobias ; Finkbeiner, Bernd ; Weissenbacher, Georg | Finding ∀∃ Hyperbugs using Symbolic Execution | Article Artikel | 8-Oct-2024 |
| 43 | | Biere, Armin ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils | Clausal Equivalence Sweeping | Inproceedings Konferenzbeitrag | Oct-2024 |
| 44 | | Ait El Manssour, Rida ; Kenison, George James ; Shirmohammadi, Mahsa ; Varonka, Anton | Simple Linear Loops: Algebraic Invariants and Synthesis | Presentation Vortrag | 19-Sep-2024 |
| 45 | | Sextl, Florian | With Biabduction towards Memory Safety across the Rust-C-FFI | Presentation Vortrag | 17-Sep-2024 |
| 46 | | Biere, Armin ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils | Clausal Congruence Closure | Inproceedings Konferenzbeitrag | 19-Aug-2024 |
| 47 | | Coutelier, Robin ; Fleury, Mathias ; Kovacs, Laura | Lazy Reimplication in Chronological Backtracking | Inproceedings Konferenzbeitrag | 19-Aug-2024 |
| 48 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Certifying Incremental SAT Solving | Presentation Vortrag | 23-Jul-2024 |
| 49 |  | 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 |
| 50 | | 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 |
| 51 | | 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 |
| 52 | | Fazekas, Katalin | Incremental SAT Solvers in Practice | Presentation Vortrag | 26-Jun-2024 |
| 53 | | 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 |
| 54 |  | Pluska, Alexander ; Welke, Pascal ; Gärtner, Thomas ; Malhotra, Sagar | Logical Distillation of Graph Neural Networks | Inproceedings Konferenzbeitrag | 24-Jun-2024 |
| 55 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Incremental Proofs for Bounded Model Checking | Inproceedings Konferenzbeitrag | 19-Jun-2024 |
| 56 | | Amrollahi, Daneshvar ; Bartocci, Ezio ; Kenison, George James ; Kovacs, Laura ; Moosbrugger, Marcel ; Stankovic, Miroslav | (Un)Solvable loop analysis | Article Artikel | 11-Jun-2024 |
| 57 |  | 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 |
| 58 | | Chimes, Mark Jonathan ; Iosif, Radu ; Zuleger, Florian | Tree-Verifiable Graph Grammars | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 59 |  | Georgiou, Pamina ; Hajdu, Marton ; Kovacs, Laura | Saturating Sorting without Sorts | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 60 |  | Hajdu, Marton ; Kovács, Laura ; Rawson, Michael | Rewriting and Inductive Reasoning | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 61 |  | Schoisswohl, Johannes ; Kovács, Laura ; Korovin, Konstantin | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 62 | | Fazekas, Katalin ; Pollitt, Florian ; Fleury, Mathias ; Biere, Armin | Certifying Incremental SAT Solving | Inproceedings Konferenzbeitrag | 26-May-2024 |
| 63 | | Dacík, Tomáš ; Rogalewicz, Adam ; Vojnar, Tomáš ; Zuleger, Florian | Deciding Boolean Separation Logic via Small Models | Inproceedings Konferenzbeitrag | 4-Apr-2024 |
| 64 | | Hitarth, S. ; Kenison, George James ; Kovacs, Laura ; Varonka, Anton | Linear Loop Synthesis for Quadratic Invariants | Inproceedings Konferenzbeitrag | 11-Mar-2024 |
| 65 | | Georgiou, Pamina ; Hajdu, Márton ; Kovács, Laura | Saturating Sorting without Sorts | Preprint Preprint | 6-Mar-2024 |
| 66 | | Sochor, Hannes ; Ferrarotti, Flavio ; Kaufmann, Daniela | Fuzzing-based grammar learning from a minimal set of seed inputs | Article Artikel | Mar-2024 |
| 67 |  | Nießen, Tobias ; Weissenbacher, Georg | Finding counterexamples to ∀∃ hyperproperties | Presentation Vortrag | 16-Jan-2024 |
| 68 | | 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 |
| 69 |  | Eisenhofer, Clemens ; Kovács, Laura ; Rawson, Michael | Embedding the Connection Calculus in Satisfiability Modulo Theories | Inproceedings Konferenzbeitrag | Jan-2024 |
| 70 | | Jeanteur, Simon ; Kovács, Laura ; Maffei, Matteo ; Rawson, Michael | CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model | Inproceedings Konferenzbeitrag | 2024 |
| 71 | | Ciabattoni, Agata ; Eisenhofer, Clemens ; Rozplokhas, Dmitry | Strongly Analytic Calculi for KLM Logics with SMT-Based Prover | Inproceedings Konferenzbeitrag | 2024 |
| 72 |  | Pluska, Alexander ; Welke, Pascal ; Gärtner, Thomas ; Malhotra, Sagar | Logical Distillation of Graph Neural Networks | Inproceedings Konferenzbeitrag | 2024 |
| 73 | | Aminof, Benjamin ; Cooper, Linus ; Rubin, Sasha ; Vardi, Moshe Y. ; Zuleger, Florian | Probabilistic Synthesis and Verification for LTL on Finite Traces | Inproceedings Konferenzbeitrag | 2024 |
| 74 |  | Kovács, Laura ; Hozzová, Petra ; Hajdu, Márton ; Voronkov, Andrei | Induction in Saturation | Inproceedings Konferenzbeitrag | 2024 |
| 75 | | Hozzová, Petra ; Amrollahi, Daneshvar ; Hajdu, Márton ; Kovács, Laura ; Voronkov, Andrei ; Wagner, Eva Maria | Synthesis of Recursive Programs in Saturation | Inproceedings Konferenzbeitrag | 2024 |
| 76 | | Biere, Armin ; Faller, Tobias ; Fazekas, Katalin ; Fleury, Mathias ; Froleyks, Nils ; Pollitt, Florian | CaDiCaL 2.0 | Inproceedings Konferenzbeitrag | 2024 |
| 77 |  | Hajdu, Márton ; Kovács, Laura ; Rawson, Michael ; Voronkov, Andrei | Reducibility Constraints in Superposition | Inproceedings Konferenzbeitrag | 2024 |
| 78 |  | Heisinger, Simone ; Heisinger, Maximilian ; Rebola-Pardo, Adrian ; Seidl, Martina | Quantifier Shifting for Quantified Boolean Formulas Revisited | Inproceedings Konferenzbeitrag | 2024 |
| 79 | | Athavale, Anagha ; Bartocci, Ezio ; Christakis, Maria ; Maffei, Matteo ; Ničković, Dejan ; Weissenbacher, Georg | Verifying Global Two-Safety Properties in Neural Networks with Confidence | Inproceedings Konferenzbeitrag | 2024 |
| 80 | | Rain, Sophie ; Brugger, Lea Salome ; Petković Komel, Anja ; Kovács, Laura ; Rawson, Michael | Scaling CheckMate for Game-Theoretic Security | Inproceedings Konferenzbeitrag | 2024 |
| 81 | | Hader, Thomas ; Ozdemir, Alex | An SMT-LIB Theory of Finite Fields | Inproceedings Konferenzbeitrag | 2024 |
| 82 | | Amrollahi, Daneshvar ; Bartocci, Ezio ; Kenison, George ; Kovacs, Laura ; Moosbrugger, Marcel ; Stankovič, Miroslav | Correction: (Un)Solvable loop analysis | Article Artikel | 2024 |
| 83 |  | Brugger, Lea Salome ; Kovács, Laura ; Petkovic Komel, Anja ; Rain, Sophie ; Rawson, Michael | CheckMate: Automated Game-Theoretic Security Reasoning | Inproceedings Konferenzbeitrag | 21-Nov-2023 |
| 84 | | Moosbrugger, Marcel ; Müllner, Julian ; Kovács, Laura | Automated Sensitivity Analysis for Probabilistic Loops | Inproceedings Konferenzbeitrag | 6-Nov-2023 |
| 85 |  | Sallinger, Sarah ; Weissenbacher, Georg ; Zuleger, Florian | A Formalization of Heisenbugs and Their Causes | Inproceedings Konferenzbeitrag | 31-Oct-2023 |
| 86 |  | Landman, Martina ; Rain, Sophie ; Kovács, Laura ; Gerald Futschek | Reshaping Unplugged Computer Science Workshops for Primary School Education | Inproceedings Konferenzbeitrag | 1-Oct-2023 |
| 87 |  | Fazekas, Katalin ; Aman, Goel ; Sakallah, Karem | SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols | Inproceedings Konferenzbeitrag | Oct-2023 |
| 88 |  | Rozier, Kristin Yvonne ; Shankar, Natarajan ; Tinelli, Cesare ; Vardi, Moshe | Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community | Inproceedings Konferenzbeitrag | Oct-2023 |
| 89 | | Andriushchenko, Roman ; Bartocci, Ezio ; Češka, Milan ; Pontiggia, Francesco ; Sallinger, Sarah Sophie | Deductive Controller Synthesis for Probabilistic Hyperproperties | Inproceedings Konferenzbeitrag | 15-Sep-2023 |
| 90 | | Rawson, Michael ; Wernhard, Christoph ; Zombori, Zsolt ; Bibel, Wolfgang | Lemmas: Generation, Selection, Application | Inproceedings Konferenzbeitrag | 14-Sep-2023 |
| 91 |  | Eisenhofer, Clemens ; Alassaf, Ruba ; Rawson, Michael ; Kovács, Laura | Non-Classical Logics in Satisfiability Modulo Theories | Inproceedings Konferenzbeitrag | 14-Sep-2023 |
| 92 | | Bjørner, Nikolaj ; Fazekas, Katalin | On Incremental Pre-processing for SMT | Inproceedings Konferenzbeitrag | 2-Sep-2023 |
| 93 | | Coutelier, Robin ; Kovács, Laura ; Rawson, Michael ; Rath, Jakob | SAT-Based Subsumption Resolution | Inproceedings Konferenzbeitrag | 2-Sep-2023 |
| 94 |  | Hozzová, Petra ; Kovács, Laura ; Norman, Chase ; Voronkov, Andrei | Program Synthesis in Saturation | Inproceedings Konferenzbeitrag | 2-Sep-2023 |
| 95 | | Bhayat, Ahmed ; Schoisswohl, Johannes ; Rawson, Michael | Superposition with Delayed Unification | Inproceedings Konferenzbeitrag | 2-Sep-2023 |
| 96 | | Ayala, Pablo ; Naghdi, Shaghayegh ; Nandan, Sreejith P. ; Myakala, Stephen Nagaraju ; Rath, Jakob ; Saito, Hikaru ; Guggenberger, Patrick ; Lakhanlal, Lakhanlal ; Kleitz, Freddy ; Toroker, Maytal Caspary ; Cherevan, Alexey ; Eder, Dominik | The Emergence of 2D Building Units in Metal‐Organic Frameworks for Photocatalytic Hydrogen Evolution: A Case Study with COK‐47 | Article Artikel | 18-Aug-2023 |
| 97 |  | Fazekas, Katalin ; Niemetz, Aina ; Preiner, Mathias ; Kirchweger, Markus ; Szeider, Stefan ; Biere, Armin | IPASIR-UP: User Propagators for CDCL | Inproceedings Konferenzbeitrag | 9-Aug-2023 |
| 98 | | Kenison, George ; Nosan, Klara ; Shirmohammadi, Mahsa ; Worrell, James | The Membership Problem for Hypergeometric Sequences with Quadratic Parameters | Inproceedings Konferenzbeitrag | 24-Jul-2023 |
| 99 | | Kenison, George ; Nieuwveld, Joris ; Ouaknine, Joël ; Worrell, James | Positivity Problems for Reversible Linear Recurrence Sequences | Inproceedings Konferenzbeitrag | 5-Jul-2023 |
| 100 | | Kenison, George James ; Kovacs, Laura ; Varonka, Anton | From Polynomial Invariants to Linear Loops | Inproceedings Konferenzbeitrag | Jul-2023 |
