| Automated Termination Analysis of Polynomial Probabilistic Programs | 0 | 0.34 | 2021 |
| Integer Induction In Saturation | 0 | 0.34 | 2021 |
| Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper). | 0 | 0.34 | 2021 |
| Analysis of Bayesian Networks via Prob-Solvable Loops | 2 | 0.36 | 2020 |
| Induction with Generalization in Superposition Reasoning. | 0 | 0.34 | 2020 |
| Trace Logic for Inductive Loop Reasoning | 0 | 0.34 | 2020 |
| Algebra-Based Loop Synthesis. | 0 | 0.34 | 2020 |
| Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. | 2 | 0.36 | 2019 |
| Superposition Reasoning about Quantified Bitvector Formulas | 0 | 0.34 | 2019 |
| Interactive Visualization Of Saturation Attempts In Vampire | 1 | 0.35 | 2019 |
| Foreword - Formalization of geometry, automated and interactive geometric reasoning. | 0 | 0.34 | 2019 |
| A FOOLish Encoding of the Next State Relations of Imperative Programs. | 0 | 0.34 | 2018 |
| Aligator.Jl - A Julia Package For Loop Invariant Generation | 0 | 0.34 | 2018 |
| Loop Analysis by Quantification over Iterations. | 0 | 0.34 | 2018 |
| First-Order Interpolation and Interpolating Proof Systems. | 1 | 0.36 | 2017 |
| Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. | 2 | 0.36 | 2017 |
| A Supervisory Control Algorithm Based on Property-Directed Reachability. | 0 | 0.34 | 2017 |
| First-Order Interpolation and Grey Areas of Proofs (Invited Talk). | 0 | 0.34 | 2017 |
| Splitting Proofs for Interpolation. | 0 | 0.34 | 2017 |
| Coming to Terms with Quantified Reasoning. | 2 | 0.38 | 2017 |
| A Clausal Normal Form Translation for FOOL. | 0 | 0.34 | 2016 |
| Theory-Specific Reasoning about Loops with Arrays using Vampire. | 0 | 0.34 | 2016 |
| Reasoning About Loops Using Vampire. | 0 | 0.34 | 2015 |
| The Vampire and the FOOL | 4 | 0.42 | 2015 |
| A First Class Boolean Sort in First-Order Theorem Proving and TPTP | 5 | 0.48 | 2015 |
| Reasoning About Loops Using Vampire in KeY | 0 | 0.34 | 2015 |
| Segment Abstraction for Worst-Case Execution Time Analysis. | 8 | 0.46 | 2015 |
| Special issue on symbolic computation in software science. | 0 | 0.34 | 2015 |
| Extensional Crisis and Proving Identity. | 1 | 0.36 | 2014 |
| Supervisory Control of Discrete-Event Systems via IC3. | 4 | 0.41 | 2014 |
| Lingva: Generating And Proving Program Properties Using Symbol Elimination | 4 | 0.44 | 2014 |
| Special issue on Automated Specification and Verification of Web Systems | 0 | 0.34 | 2013 |
| SmacC: A Retargetable Symbolic Execution Engine. | 2 | 0.39 | 2013 |
| First-Order theorem proving and vampire | 95 | 3.16 | 2013 |
| A Parametric Interpolation Framework for First-Order Theories. | 0 | 0.34 | 2013 |
| Tree Interpolation in Vampire. | 4 | 0.39 | 2013 |
| The Auspicious Couple: Symbolic Execution and WCET Analysis. | 4 | 0.41 | 2013 |
| Bound Propagation for Arithmetic Reasoning in Vampire | 1 | 0.37 | 2013 |
| WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds | 14 | 0.60 | 2013 |
| The Inverse Method for Many-Valued Logics. | 1 | 0.36 | 2013 |
| FFX: a portable WCET annotation language | 6 | 0.47 | 2012 |
| r-TuBound: loop bounds for WCET analysis (tool paper) | 9 | 0.57 | 2012 |
| Playing in the grey area of proofs | 18 | 0.74 | 2012 |
| Vinter: A Vampire-Based Tool for Interpolation. | 2 | 0.38 | 2012 |
| Solving Robust Glucose-Insulin Control by Dixon Resultant Computations | 0 | 0.34 | 2012 |
| Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). | 0 | 0.34 | 2012 |
| On transfinite Knuth-Bendix orders | 6 | 0.52 | 2011 |
| Symbol Elimination in Program Analysis | 0 | 0.34 | 2011 |
| Case studies on invariant generation using a saturation theorem prover | 7 | 0.66 | 2011 |
| Symbolic loop bound computation for WCET analysis | 10 | 0.59 | 2011 |
