Laura Kovács

Anton Varonka

Proceedings of the Relational and Algebraic Methods in Computer Science, 2023

2022

The probabilistic termination tool amber.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., August, 2022

This is the Moment for Probabilistic Loops - Artifact (Polar).

[BibT_eX]

[DOI]

Dataset, July, 2022

This is the Moment for Probabilistic Loops - Artifact (Polar).

[BibT_eX]

[DOI]

Dataset, July, 2022

This is the Moment for Probabilistic Loops - Artifact (Polar).

[BibT_eX]

[DOI]

Dataset, July, 2022

This is the Moment for Probabilistic Loops - Artifact (Polar).

[BibT_eX]

[DOI]

Dataset, July, 2022

Moment-based analysis of Bayesian network properties.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2022

This is the moment for probabilistic loops.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Algebra-Based Reasoning for Loop Synthesis.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2022

An SMT Approach for Solving Polynomials over Finite Fields.

[BibT_eX]

[DOI]

Thomas Hader

Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

User-Propagators for Custom Theories in SMT Solving.

[BibT_eX]

[DOI]

Clemens Eisenhofer

Solving Invariant Generation for Unsolvable Loops.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 29th International Symposium, 2022

Distribution Estimation for Probabilistic Loops.

[BibT_eX]

[DOI]

Proceedings of the Quantitative Evaluation of Systems - 19th International Conference, 2022

The Vampire Approach to Induction (short paper).

[BibT_eX]

[DOI]

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

Lemmaless Induction in Trace Logic.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 15th International Conference, 2022

First-Order Subsumption via SAT Solving.

[BibT_eX]

[DOI]

Jakob Rath

Armin Biere

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

The Rapid Software Verification Framework.

[BibT_eX]

[DOI]

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Getting Saturated with Induction.

[BibT_eX]

[DOI]

Proceedings of the Principles of Systems Design, 2022

2021

Automating Induction by Reflection.

[BibT_eX]

[DOI]

Johannes Schoisswohl

Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2021

Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Automated Generation of Exam Sheets for Automated Deduction.

[BibT_eX]

[DOI]

Petra Hozzová

Jakob Rath

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Inductive Benchmarks for Automated Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Induction with Recursive Definitions in Superposition.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer Aided Design, 2021

Automated Termination Analysis of Polynomial Probabilistic Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2021

Summing up Smart Transitions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Integer Induction in Saturation.

[BibT_eX]

[DOI]

Petra Hozzová

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Algebra-based Loop Synthesis.

[BibT_eX]

[DOI]

CoRR, 2020

Mora - Automatic Generation of Moment-Based Invariants.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Formalizing Graph Trail Properties in Isabelle/HOL.

[BibT_eX]

[DOI]

Hanna Lachnitt

Stefan Szeider

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

Induction with Generalization in Superposition Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

Algebra-Based Loop Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 16th International Conference, 2020

Analysis of Bayesian Networks via Prob-Solvable Loops.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30, 2020

Trace Logic for Inductive Loop Reasoning.

[BibT_eX]

[DOI]

Pamina Georgiou

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Subsumption Demodulation in First-Order Theorem Proving.

[BibT_eX]

[DOI]

Jakob Rath

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Foreword.

[BibT_eX]

[DOI]

James H. Davenport

Daniela Zaharie

Math. Comput. Sci., 2019

Foreword - Formalization of geometry, automated and interactive geometric reasoning.

[BibT_eX]

[DOI]

Pascal Schreck

Tetsuo Ida

Ann. Math. Artif. Intell., 2019

Portfolio SAT and SMT Solving of Cardinality Constraints in Sensor Network Optimization.

[BibT_eX]

[DOI]

Gergely Kovásznai

Krisztián Gajdár

Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2019

Superposition Reasoning about Quantified Bitvector Formulas.

[BibT_eX]

[DOI]

David Damestani

Martin Suda

Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2019

Interactive Visualization of Saturation Attempts in Vampire.

[BibT_eX]

[DOI]

Lena Schnedlitz

Proceedings of the Integrated Formal Methods - 15th International Conference, 2019

Verifying Relational Properties using Trace Logic.

[BibT_eX]

[DOI]

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2019

2018

Invariant Generation for Multi-Path Loops with Polynomial Assignments.

[BibT_eX]

[DOI]

Maximilian Jaroschek

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Aligator.jl - A Julia Package for Loop Invariant Generation.

[BibT_eX]

[DOI]

Maximilian Jaroschek

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Loop Analysis by Quantification over Iterations.

[BibT_eX]

[DOI]

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

A FOOLish Encoding of the Next State Relations of Imperative Programs.

[BibT_eX]

[DOI]

Evgenii Kotelnikov

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution.

[BibT_eX]

[DOI]

J. Symb. Comput., 2017

Coming to terms with quantified reasoning.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

First-Order Interpolation and Interpolating Proof Systems.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences.

[BibT_eX]

[DOI]

Maximilian Jaroschek

Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation, 2017

A Supervisory Control Algorithm Based on Property-Directed Reachability.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2017

First-Order Interpolation and Grey Areas of Proofs (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, 2017

Splitting Proofs for Interpolation.

[BibT_eX]

[DOI]

Martin Suda

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Symbolic Computation and Automated Reasoning for Program Analysis.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

A Clausal Normal Form Translation for FOOL.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

The vampire and the FOOL.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Theory-Specific Reasoning about Loops with Arrays using Vampire.

[BibT_eX]

[DOI]

Yuting Chen

Proceedings of the Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, 2016

2015

Special issue on symbolic computation in software science.

[BibT_eX]

[DOI]

J. Symb. Comput., 2015

A First Class Boolean Sort in First-Order Theorem Proving and TPTP.

[BibT_eX]

[DOI]

Evgenii Kotelnikov

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Reasoning About Loops Using Vampire in KeY.

[BibT_eX]

[DOI]

Wolfgang Ahrendt

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Segment Abstraction for Worst-Case Execution Time Analysis.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2015

Reasoning About Loops Using Vampire.

[BibT_eX]

[DOI]

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2015

2014

Symbol Elimination for Automated Generation of Program Properties.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014

Experimenting with SAT Solvers in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Human-Inspired Computing and Its Applications, 2014

Supervisory Control of Discrete-Event Systems via IC3.

[BibT_eX]

[DOI]

Mohammad Reza Shoaei

Bengt Lennartson

Proceedings of the Hardware and Software: Verification and Testing, 2014

Lingva: Generating and Proving Program Properties Using Symbol Elimination.

[BibT_eX]

[DOI]

Ioan Dragan

Proceedings of the Perspectives of System Informatics, 2014

SAT solving experiments in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

Extensional Crisis and Proving Identity.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Special issue on Automated Specification and Verification of Web Systems.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2013

The Auspicious Couple: Symbolic Execution and WCET Analysis.

[BibT_eX]

[DOI]

Proceedings of the 13th International Workshop on Worst-Case Execution Time Analysis, 2013

Bound Propagation for Arithmetic Reasoning in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Real-Time Networks and Systems, 2013

A Parametric Interpolation Framework for First-Order Theories.

[BibT_eX]

[DOI]

Simone Fulvio Rollini

Natasha Sharygina

Proceedings of the Advances in Artificial Intelligence and Its Applications, 2013

The Inverse Method for Many-Valued Logics.

[BibT_eX]

[DOI]

Andrei Mantsivoda

Proceedings of the Advances in Artificial Intelligence and Its Applications, 2013

Tree Interpolation in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

First-Order Theorem Proving and Vampire.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

SmacC: A Retargetable Symbolic Execution Engine.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Foreword.

[BibT_eX]

[DOI]

J. Symb. Comput., 2012

Special issue on Automated Specification and Verification of Web Systems.

[BibT_eX]

[DOI]

Temur Kutsia

J. Appl. Log., 2012

Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461).

[BibT_eX]

[DOI]

Krishnendu Chatterjee

Rupak Majumdar

Dagstuhl Reports, 2012

Solving Robust Glucose-Insulin Control by Dixon Resultant Computations.

[BibT_eX]

[DOI]

Béla Paláncz

Levente Kovács

Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2012

FFX: a portable WCET annotation language.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Real-Time and Network Systems, 2012

Playing in the grey area of proofs.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

r-TuBound: Loop Bounds for WCET Analysis (Tool Paper).

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Vinter: A Vampire-Based Tool for Interpolation.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Invariant Generation in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Symbol Elimination in Program Analysis.

[BibT_eX]

[DOI]

Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2011

Case Studies on Invariant Generation Using a Saturation Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Advances in Artificial Intelligence, 2011

Symbolic Loop Bound Computation for WCET Analysis.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2011

On Transfinite Knuth-Bendix Orders.

[BibT_eX]

[DOI]

Georg Moser

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Introduction.

[BibT_eX]

[DOI]

Martin Giese

Andrew Ireland

J. Symb. Comput., 2010

Invariant and Type Inference for Matrices.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Aligators for Arrays (Tool Paper).

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

ABC: Algebraic Bound Computation for Loops.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Interpolation and Symbol Elimination in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2009

A Complete Invariant Generation Approach for P-solvable Loops.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2009

Interpolation and Symbol Elimination.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Reasoning Algebraically About P-Solvable Loops.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Valigator: A Verification Tool with Bound and Invariant Generation.

[BibT_eX]

[DOI]

Thomas A. Henzinger

Thibaud Hottelier

Proceedings of the Logic for Programming, 2008

Invariant Generation for P-Solvable Loops with Assignments.

[BibT_eX]

[DOI]

Proceedings of the Computer Science, 2008

Aligator: A Mathematica Package for Invariant Generation (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2006

Theorema: Towards computer-aided mathematical theory exploration.

[BibT_eX]

[DOI]

J. Appl. Log., 2006

Combining Logic and Algebraic Techniques for Program Verification in Theorema.

[BibT_eX]

[DOI]

Nikolaj Popov

Tudor Jebelean

Proceedings of the Leveraging Applications of Formal Methods, 2006

2005

An Algorithm for Automated Generation of Invariants for Loops with Conditionals.

[BibT_eX]

[DOI]

Laura Ildikó Kovács

Tudor Jebelean

Proceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2005), 2005

2004

Experimental Program Verification in the Theorema System.

[BibT_eX]

Tudor Jebelean